Source indexedlemma · leanprover/lean4:v4.32.0

Complex.Hadamard.analyticOrderAt_ne_top_of_exists_ne_zero

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Divisor · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/Divisor.lean:62 to 76

Mathematical statement

Exact Lean statement

lemma analyticOrderAt_ne_top_of_exists_ne_zero {f : ℂ → ℂ} (hf : Differentiable ℂ f)
    (hnot : ∃ z : ℂ, f z ≠ 0) :
    ∀ z : ℂ, analyticOrderAt f z ≠ ⊤

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma analyticOrderAt_ne_top_of_exists_ne_zero {f : ℂ → ℂ} (hf : Differentiable ℂ f)    (hnot : ∃ z : ℂ, f z ≠ 0) :    ∀ z : ℂ, analyticOrderAt f z ≠ ⊤ := by  rcases hnot with ⟨z1, hz1⟩  have hf_an : AnalyticOnNhd ℂ f (Set.univ : Set ℂ) := by    intro z hz    exact (Differentiable.analyticAt (f := f) hf z)  have hz1_not_top : analyticOrderAt f z1 ≠ ⊤ := by    have : analyticOrderAt f z1 = 0 :=      (hf.analyticAt z1).analyticOrderAt_eq_zero.2 hz1    simp [this]  intro z  exact AnalyticOnNhd.analyticOrderAt_ne_top_of_isPreconnected (hf := hf_an)    (U := (Set.univ : Set ℂ)) (x := z1) (y := z) (by simpa using isPreconnected_univ)    (by simp) (by simp) hz1_not_top