Theorem: cindex_eventually_eq_order (RMT4/cindex.lean)

State before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hp : HasFPowerSeriesAt f p z₀
⊢ ∀ᶠ (r : ℝ) in 𝓝[>] 0, cindex z₀ r f = ↑(FormalMultilinearSeries.order p)
Tactic:
rw [eventually_nhdsWithin_iff, Metric.eventually_nhds_iff]
State after:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hp : HasFPowerSeriesAt f p z₀
⊢ ∃ ε > 0, ∀ ⦃y : ℝ⦄, dist y 0 < ε → y ∈ Set.Ioi 0 → cindex z₀ y f = ↑(FormalMultilinearSeries.order p)

State before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hp : HasFPowerSeriesAt f p z₀
⊢ ∃ ε > 0, ∀ ⦃y : ℝ⦄, dist y 0 < ε → y ∈ Set.Ioi 0 → cindex z₀ y f = ↑(FormalMultilinearSeries.order p)
Tactic:
obtain ⟨R, hR, hf⟩ := exists_cindex_eq_order hp
State after:
case intro.intro
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hp : HasFPowerSeriesAt f p z₀
R : ℝ
hR : R > 0
hf : ∀ r ∈ Set.Ioo 0 R, cindex z₀ r f = ↑(FormalMultilinearSeries.order p)
⊢ ∃ ε > 0, ∀ ⦃y : ℝ⦄, dist y 0 < ε → y ∈ Set.Ioi 0 → cindex z₀ y f = ↑(FormalMultilinearSeries.order p)

State before:
case intro.intro
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hp : HasFPowerSeriesAt f p z₀
R : ℝ
hR : R > 0
hf : ∀ r ∈ Set.Ioo 0 R, cindex z₀ r f = ↑(FormalMultilinearSeries.order p)
⊢ ∃ ε > 0, ∀ ⦃y : ℝ⦄, dist y 0 < ε → y ∈ Set.Ioi 0 → cindex z₀ y f = ↑(FormalMultilinearSeries.order p)
Tactic:
exact ⟨R, hR, λ r hr1 hr2 => hf r ⟨hr2, by simpa using lt_of_abs_lt hr1⟩⟩
State after:
no goals

State before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f p z₀
R : ℝ
hR : R > 0
hf : ∀ r ∈ Set.Ioo 0 R, cindex z₀ r f = ↑(FormalMultilinearSeries.order p)
r : ℝ
hr1 : dist r 0 < R
hr2 : r ∈ Set.Ioi 0
⊢ r < R
Tactic:
simpa using lt_of_abs_lt hr1
State after:
no goals