Source indexedtheorem · leanprover/lean4:v4.32.0

Complex.Hadamard.analyticOrderAt_prod_fiberFinset

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Divisor · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/Divisor.lean:177 to 189

Mathematical statement

Exact Lean statement

theorem analyticOrderAt_prod_fiberFinset
    (m : ℕ) (f : ℂ → ℂ) (z₀ : ℂ) :
    analyticOrderAt (fun z : ℂ => ∏ p ∈ divisorZeroIndex₀_fiberFinset (f := f) z₀,
            weierstrassFactor m (z / divisorZeroIndex₀_val p))
      z₀ = ((divisorZeroIndex₀_fiberFinset (f := f) z₀).card : ℕ∞)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem analyticOrderAt_prod_fiberFinset    (m : ℕ) (f : ℂ → ℂ) (z₀ : ℂ) :    analyticOrderAt (fun z : ℂ => ∏ p ∈ divisorZeroIndex₀_fiberFinset (f := f) z₀,            weierstrassFactor m (z / divisorZeroIndex₀_val p))      z₀ = ((divisorZeroIndex₀_fiberFinset (f := f) z₀).card : ℕ∞) := by  have h :=    analyticOrderAt_finset_prod_weierstrassFactor_divisorZeroIndex₀      (m := m) (f := f) (s := divisorZeroIndex₀_fiberFinset (f := f) z₀) (z₀ := z₀)  have hfilter :      (divisorZeroIndex₀_fiberFinset (f := f) z₀).filter (fun p => divisorZeroIndex₀_val p = z₀) =        divisorZeroIndex₀_fiberFinset (f := f) z₀ := by    ext p; simp  simpa [hfilter] using h