Source indexedtheorem · leanprover/lean4:v4.32.0

Complex.Hadamard.eventually_exists_ball_eq_punctured_quotient_of_factorization

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorQuotientConvergence · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/DivisorQuotientConvergence.lean:511 to 526

Mathematical statement

Exact Lean statement

theorem eventually_exists_ball_eq_punctured_quotient_of_factorization
    (m : ℕ) (f : ℂ → ℂ) (z₀ : ℂ) :
    ∀ᶠ s : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ)) in (Filter.atTop : Filter _),
      ∃ ε > 0, ∃ g : ℂ → ℂ, AnalyticAt ℂ g z₀ ∧
        ∀ z : ℂ, z ∈ Metric.ball z₀ ε → z ≠ z₀ → (divisorPartialProduct m f s z) /
              (z - z₀) ^ (divisorZeroIndex₀_fiberFinset (f := f) z₀).card
            = g z

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem eventually_exists_ball_eq_punctured_quotient_of_factorization    (m : ℕ) (f : ℂ → ℂ) (z₀ : ℂ) :    ∀ᶠ s : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ)) in (Filter.atTop : Filter _),      ∃ ε > 0, ∃ g : ℂ → ℂ, AnalyticAt ℂ g z₀ ∧        ∀ z : ℂ, z ∈ Metric.ball z₀ ε → z ≠ z₀ → (divisorPartialProduct m f s z) /              (z - z₀) ^ (divisorZeroIndex₀_fiberFinset (f := f) z₀).card            = g z := by  refine (eventually_eq_punctured_quotient_of_factorization (m := m) (f := f) z₀).mono ?_  intro s hs  rcases hs with ⟨g, hg, hEq⟩  rcases (Metric.nhdsWithin_basis_ball (x := z₀) (s := {z : ℂ | z ≠ z₀})).mem_iff.1 hEq with    ⟨ε, hε, hball⟩  refine ⟨ε, hε, g, hg, ?_⟩  intro z hz hz0  have hz' : z ∈ Metric.ball z₀ ε ∩ {z : ℂ | z ≠ z₀} := ⟨hz, hz0⟩  exact hball hz'