analyticOrderAt_eq_zero — Mathlib

English

A combined ENNReal-based radius formula comparing with ENNReal division to cover zero/nonzero regimes.

Русский

Комбинированная формула радиуса на основе ENNReal учитывает различные режимы нуля и ненуля.

LaTeX

$$$$(\text{Radius}) = r^{-1} \;\text{in ENNReal terms}, \text{ with cases as in } ofScalars_radius_eq_inv_of_tendsto_ENNReal.$$$$

Lean4

theorem analyticOrderAt_eq_zero : analyticOrderAt f z₀ = 0 ↔ ¬AnalyticAt 𝕜 f z₀ ∨ f z₀ ≠ 0 :=
  by
  by_cases hf : AnalyticAt 𝕜 f z₀
  · rw [← ENat.coe_zero, hf.analyticOrderAt_eq_natCast]
    constructor
    · intro ⟨g, _, _, hg⟩
      simpa [hf, hg.self_of_nhds]
    · exact fun hz ↦ ⟨f, hf, hz.resolve_left <| not_not_intro hf, by simp⟩
  · simp [hf]

Похожие утверждения