Theorem: HasFPowerSeriesAt.dslope_order_eventually_ne_zero (RMT4/cindex.lean)

State before:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
z₀ c : ℂ
n : ℕ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, (swap dslope z₀)^[FormalMultilinearSeries.order p] f z ≠ 0
Tactic:
refine ContinuousAt.eventually_ne ?h (hp.iterate_dslope_fslope_ne_zero h)
State after:
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
z₀ c : ℂ
n : ℕ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
⊢ ContinuousAt (fun z => (swap dslope z₀)^[FormalMultilinearSeries.order p] f z) z₀

State before:
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
z₀ c : ℂ
n : ℕ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
⊢ ContinuousAt (fun z => (swap dslope z₀)^[FormalMultilinearSeries.order p] f z) z₀
Tactic:
obtain ⟨r, hf⟩ := hp
State after:
case h.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
z₀ c : ℂ
n : ℕ
h : p ≠ 0
r : ENNReal
hf : HasFPowerSeriesOnBall f p z₀ r
⊢ ContinuousAt (fun z => (swap dslope z₀)^[FormalMultilinearSeries.order p] f z) z₀

State before:
case h.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
z₀ c : ℂ
n : ℕ
h : p ≠ 0
r : ENNReal
hf : HasFPowerSeriesOnBall f p z₀ r
⊢ ContinuousAt (fun z => (swap dslope z₀)^[FormalMultilinearSeries.order p] f z) z₀
Tactic:
have hr : 0 < r := hf.r_pos
State after:
case h.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
z₀ c : ℂ
n : ℕ
h : p ≠ 0
r : ENNReal
hf : HasFPowerSeriesOnBall f p z₀ r
hr : 0 < r
⊢ ContinuousAt (fun z => (swap dslope z₀)^[FormalMultilinearSeries.order p] f z) z₀

State before:
case h.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
z₀ c : ℂ
n : ℕ
h : p ≠ 0
r : ENNReal
hf : HasFPowerSeriesOnBall f p z₀ r
hr : 0 < r
⊢ ContinuousAt (fun z => (swap dslope z₀)^[FormalMultilinearSeries.order p] f z) z₀
Tactic:
refine ContinuousOn.continuousAt ?h1 (EMetric.ball_mem_nhds _ hr)
State after:
case h1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
z₀ c : ℂ
n : ℕ
h : p ≠ 0
r : ENNReal
hf : HasFPowerSeriesOnBall f p z₀ r
hr : 0 < r
⊢ ContinuousOn (fun z => (swap dslope z₀)^[FormalMultilinearSeries.order p] f z) (EMetric.ball z₀ r)

State before:
case h1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
z₀ c : ℂ
n : ℕ
h : p ≠ 0
r : ENNReal
hf : HasFPowerSeriesOnBall f p z₀ r
hr : 0 < r
⊢ ContinuousOn (fun z => (swap dslope z₀)^[FormalMultilinearSeries.order p] f z) (EMetric.ball z₀ r)
Tactic:
have hh : DifferentiableOn ℂ (iterate (swap dslope z₀) p.order f) (EMetric.ball z₀ r) :=
  DifferentiableOn.iterate_dslope hf.differentiableOn EMetric.isOpen_ball (EMetric.mem_ball_self hr)
State after:
case h1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
z₀ c : ℂ
n : ℕ
h : p ≠ 0
r : ENNReal
hf : HasFPowerSeriesOnBall f p z₀ r
hr : 0 < r
hh : DifferentiableOn ℂ ((swap dslope z₀)^[FormalMultilinearSeries.order p] f) (EMetric.ball z₀ r)
⊢ ContinuousOn (fun z => (swap dslope z₀)^[FormalMultilinearSeries.order p] f z) (EMetric.ball z₀ r)

State before:
case h1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
z₀ c : ℂ
n : ℕ
h : p ≠ 0
r : ENNReal
hf : HasFPowerSeriesOnBall f p z₀ r
hr : 0 < r
hh : DifferentiableOn ℂ ((swap dslope z₀)^[FormalMultilinearSeries.order p] f) (EMetric.ball z₀ r)
⊢ ContinuousOn (fun z => (swap dslope z₀)^[FormalMultilinearSeries.order p] f z) (EMetric.ball z₀ r)
Tactic:
exact hh.continuousOn
State after:
no goals