Source indexedtheorem · leanprover/lean4:v4.32.0

Complex.Hadamard.eventually_exists_analyticAt_eq_pow_smul_divisorPartialProduct

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorQuotientConvergence · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/DivisorQuotientConvergence.lean:463 to 476

Mathematical statement

Exact Lean statement

theorem eventually_exists_analyticAt_eq_pow_smul_divisorPartialProduct
    (m : ℕ) (f : ℂ → ℂ) (z₀ : ℂ) :
    ∀ᶠ s : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ)) in (Filter.atTop : Filter _),
      ∃ g : ℂ → ℂ, AnalyticAt ℂ g z₀ ∧ g z₀ ≠ 0 ∧ (fun z : ℂ => divisorPartialProduct m f s z)
        =ᶠ[𝓝 z₀] fun z : ℂ =>
          (z - z₀) ^ (divisorZeroIndex₀_fiberFinset (f := f) z₀).card • g z

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem eventually_exists_analyticAt_eq_pow_smul_divisorPartialProduct    (m : ℕ) (f : ℂ → ℂ) (z₀ : ℂ) :    ∀ᶠ s : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ)) in (Filter.atTop : Filter _),      ∃ g : ℂ → ℂ, AnalyticAt ℂ g z₀ ∧ g z₀ ≠ 0 ∧ (fun z : ℂ => divisorPartialProduct m f s z)        =ᶠ[𝓝 z₀] fun z : ℂ =>          (z - z₀) ^ (divisorZeroIndex₀_fiberFinset (f := f) z₀).card • g z := by  refine (eventually_atTop_subset_fiberFinset (f := f) z₀).mono ?_  intro s hs  rcases      exists_analyticAt_eq_pow_smul_of_partialProduct_contains_fiber        (m := m) (f := f) (z₀ := z₀) (s := s) hs with    ⟨g, hg, hg0, hEq⟩  refine ⟨g, hg, hg0, ?_⟩  simpa [divisorPartialProduct] using hEq