Source indexedtheorem · leanprover/lean4:v4.32.0

Complex.Hadamard.exists_analyticAt_eq_pow_smul_of_partialProduct_contains_fiber

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorPartialProductFactor · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/DivisorPartialProductFactor.lean:176 to 196

Mathematical statement

Exact Lean statement

theorem exists_analyticAt_eq_pow_smul_of_partialProduct_contains_fiber
    (m : ℕ) (f : ℂ → ℂ) (z₀ : ℂ)
    (s : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ)))
    (hs : divisorZeroIndex₀_fiberFinset (f := f) z₀ ⊆ s) :
    ∃ g : ℂ → ℂ,
      AnalyticAt ℂ g z₀ ∧ g z₀ ≠ 0 ∧
        (fun z : ℂ => ∏ p ∈ s, weierstrassFactor m (z / divisorZeroIndex₀_val p))
          =ᶠ[𝓝 z₀]
          fun z : ℂ => (z - z₀) ^ (divisorZeroIndex₀_fiberFinset (f := f) z₀).card • g z

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem exists_analyticAt_eq_pow_smul_of_partialProduct_contains_fiber    (m : ℕ) (f : ℂ → ℂ) (z₀ : ℂ)    (s : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ)))    (hs : divisorZeroIndex₀_fiberFinset (f := f) z₀ ⊆ s) :    ∃ g : ℂ → ℂ,      AnalyticAt ℂ g z₀ ∧ g z₀ ≠ 0 ∧        (fun z : ℂ => ∏ p ∈ s, weierstrassFactor m (z / divisorZeroIndex₀_val p))          =ᶠ[𝓝 z₀]          fun z : ℂ => (z - z₀) ^ (divisorZeroIndex₀_fiberFinset (f := f) z₀).card • g z := by  let F : ℂ → ℂ := fun z : ℂ => ∏ p ∈ s, weierstrassFactor m (z / divisorZeroIndex₀_val p)  have hF_ana : AnalyticAt ℂ F z₀ := by    simpa [F, divisorPartialProduct] using! analyticAt_divisorPartialProduct m f s z₀  have hOrder :      analyticOrderAt F z₀ =        ((divisorZeroIndex₀_fiberFinset (f := f) z₀).card : ℕ∞) := by    simpa [F] using      (analyticOrderAt_partialProduct_eq_fiberCard_of_subset (m := m)      (f := f) (z₀ := z₀) (s := s) hs)  refine (hF_ana.analyticOrderAt_eq_natCast (n := (divisorZeroIndex₀_fiberFinset    (f := f) z₀).card)).1 ?_  simp [hOrder]