Theorem: eventually_deriv_div_self_eq (RMT4/cindex.lean)

State before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
⊢ let g := (swap dslope z₀)^[FormalMultilinearSeries.order p] f;
  ∀ᶠ (z : ℂ) in 𝓝 z₀, z ≠ z₀ → deriv f z / f z = ↑(FormalMultilinearSeries.order p) / (z - z₀) + deriv g z / g z
Tactic:
intro g
State after:
f g✝ : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
g : ℂ → ℂ := (swap dslope z₀)^[FormalMultilinearSeries.order p] f
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, z ≠ z₀ → deriv f z / f z = ↑(FormalMultilinearSeries.order p) / (z - z₀) + deriv g z / g z

State before:
f g✝ : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
g : ℂ → ℂ := (swap dslope z₀)^[FormalMultilinearSeries.order p] f
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, z ≠ z₀ → deriv f z / f z = ↑(FormalMultilinearSeries.order p) / (z - z₀) + deriv g z / g z
Tactic:
obtain ⟨r, h2⟩ := hp.has_fpower_series_iterate_dslope_fslope p.order
State after:
case intro
f g✝ : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
g : ℂ → ℂ := (swap dslope z₀)^[FormalMultilinearSeries.order p] f
r : ENNReal
h2 :
  HasFPowerSeriesOnBall ((swap dslope z₀)^[FormalMultilinearSeries.order p] f)
    (FormalMultilinearSeries.fslope^[FormalMultilinearSeries.order p] p) z₀ r
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, z ≠ z₀ → deriv f z / f z = ↑(FormalMultilinearSeries.order p) / (z - z₀) + deriv g z / g z

State before:
case intro
f g✝ : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
g : ℂ → ℂ := (swap dslope z₀)^[FormalMultilinearSeries.order p] f
r : ENNReal
h2 :
  HasFPowerSeriesOnBall ((swap dslope z₀)^[FormalMultilinearSeries.order p] f)
    (FormalMultilinearSeries.fslope^[FormalMultilinearSeries.order p] p) z₀ r
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, z ≠ z₀ → deriv f z / f z = ↑(FormalMultilinearSeries.order p) / (z - z₀) + deriv g z / g z
Tactic:
have lh1 := h2.differentiableOn.eventually_differentiableAt (EMetric.ball_mem_nhds _ h2.r_pos)
State after:
case intro
f g✝ : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
g : ℂ → ℂ := (swap dslope z₀)^[FormalMultilinearSeries.order p] f
r : ENNReal
h2 :
  HasFPowerSeriesOnBall ((swap dslope z₀)^[FormalMultilinearSeries.order p] f)
    (FormalMultilinearSeries.fslope^[FormalMultilinearSeries.order p] p) z₀ r
lh1 : ∀ᶠ (y : ℂ) in 𝓝 z₀, DifferentiableAt ℂ ((swap dslope z₀)^[FormalMultilinearSeries.order p] f) y
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, z ≠ z₀ → deriv f z / f z = ↑(FormalMultilinearSeries.order p) / (z - z₀) + deriv g z / g z

State before:
case intro
f g✝ : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
g : ℂ → ℂ := (swap dslope z₀)^[FormalMultilinearSeries.order p] f
r : ENNReal
h2 :
  HasFPowerSeriesOnBall ((swap dslope z₀)^[FormalMultilinearSeries.order p] f)
    (FormalMultilinearSeries.fslope^[FormalMultilinearSeries.order p] p) z₀ r
lh1 : ∀ᶠ (y : ℂ) in 𝓝 z₀, DifferentiableAt ℂ ((swap dslope z₀)^[FormalMultilinearSeries.order p] f) y
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, z ≠ z₀ → deriv f z / f z = ↑(FormalMultilinearSeries.order p) / (z - z₀) + deriv g z / g z
Tactic:
have lh2 := hp.dslope_order_eventually_ne_zero h
State after:
case intro
f g✝ : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
g : ℂ → ℂ := (swap dslope z₀)^[FormalMultilinearSeries.order p] f
r : ENNReal
h2 :
  HasFPowerSeriesOnBall ((swap dslope z₀)^[FormalMultilinearSeries.order p] f)
    (FormalMultilinearSeries.fslope^[FormalMultilinearSeries.order p] p) z₀ r
lh1 : ∀ᶠ (y : ℂ) in 𝓝 z₀, DifferentiableAt ℂ ((swap dslope z₀)^[FormalMultilinearSeries.order p] f) y
lh2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, (swap dslope z₀)^[FormalMultilinearSeries.order p] f z ≠ 0
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, z ≠ z₀ → deriv f z / f z = ↑(FormalMultilinearSeries.order p) / (z - z₀) + deriv g z / g z

State before:
case intro
f g✝ : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
g : ℂ → ℂ := (swap dslope z₀)^[FormalMultilinearSeries.order p] f
r : ENNReal
h2 :
  HasFPowerSeriesOnBall ((swap dslope z₀)^[FormalMultilinearSeries.order p] f)
    (FormalMultilinearSeries.fslope^[FormalMultilinearSeries.order p] p) z₀ r
lh1 : ∀ᶠ (y : ℂ) in 𝓝 z₀, DifferentiableAt ℂ ((swap dslope z₀)^[FormalMultilinearSeries.order p] f) y
lh2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, (swap dslope z₀)^[FormalMultilinearSeries.order p] f z ≠ 0
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, z ≠ z₀ → deriv f z / f z = ↑(FormalMultilinearSeries.order p) / (z - z₀) + deriv g z / g z
Tactic:
have lh3 := eventually_eventually_nhds.mpr hp.eq_pow_order_mul_iterate_dslope
State after:
case intro
f g✝ : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
g : ℂ → ℂ := (swap dslope z₀)^[FormalMultilinearSeries.order p] f
r : ENNReal
h2 :
  HasFPowerSeriesOnBall ((swap dslope z₀)^[FormalMultilinearSeries.order p] f)
    (FormalMultilinearSeries.fslope^[FormalMultilinearSeries.order p] p) z₀ r
lh1 : ∀ᶠ (y : ℂ) in 𝓝 z₀, DifferentiableAt ℂ ((swap dslope z₀)^[FormalMultilinearSeries.order p] f) y
lh2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, (swap dslope z₀)^[FormalMultilinearSeries.order p] f z ≠ 0
lh3 :
  ∀ᶠ (y : ℂ) in 𝓝 z₀,
    ∀ᶠ (x : ℂ) in 𝓝 y,
      f x = (x - z₀) ^ FormalMultilinearSeries.order p • (swap dslope z₀)^[FormalMultilinearSeries.order p] f x
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, z ≠ z₀ → deriv f z / f z = ↑(FormalMultilinearSeries.order p) / (z - z₀) + deriv g z / g z

State before:
case intro
f g✝ : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
g : ℂ → ℂ := (swap dslope z₀)^[FormalMultilinearSeries.order p] f
r : ENNReal
h2 :
  HasFPowerSeriesOnBall ((swap dslope z₀)^[FormalMultilinearSeries.order p] f)
    (FormalMultilinearSeries.fslope^[FormalMultilinearSeries.order p] p) z₀ r
lh1 : ∀ᶠ (y : ℂ) in 𝓝 z₀, DifferentiableAt ℂ ((swap dslope z₀)^[FormalMultilinearSeries.order p] f) y
lh2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, (swap dslope z₀)^[FormalMultilinearSeries.order p] f z ≠ 0
lh3 :
  ∀ᶠ (y : ℂ) in 𝓝 z₀,
    ∀ᶠ (x : ℂ) in 𝓝 y,
      f x = (x - z₀) ^ FormalMultilinearSeries.order p • (swap dslope z₀)^[FormalMultilinearSeries.order p] f x
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, z ≠ z₀ → deriv f z / f z = ↑(FormalMultilinearSeries.order p) / (z - z₀) + deriv g z / g z
Tactic:
filter_upwards [lh1, lh2, lh3] with z using deriv_div_self_eq_div_add_deriv_div_self
State after:
no goals