Source indexedlemma · leanprover/lean4:v4.32.0

Complex.Hadamard.divisorPartialProduct_ne_zero_on_ball_punctured

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Divisor · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/Divisor.lean:347 to 359

Mathematical statement

Exact Lean statement

lemma divisorPartialProduct_ne_zero_on_ball_punctured
    (m : ℕ) {f : ℂ → ℂ} {z₀ : ℂ} {ε : ℝ}
    (hball :
      Metric.ball z₀ ε ∩ (MeromorphicOn.divisor f (Set.univ : Set ℂ)).support = {z₀})
    (s : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ))) :
    ∀ z ∈ Metric.ball z₀ ε, z ≠ z₀ → divisorPartialProduct m f s z ≠ 0

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma divisorPartialProduct_ne_zero_on_ball_punctured    (m : ℕ) {f : ℂ → ℂ} {z₀ : ℂ} {ε : ℝ}    (hball :      Metric.ball z₀ ε ∩ (MeromorphicOn.divisor f (Set.univ : Set ℂ)).support = {z₀})    (s : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ))) :    ∀ z ∈ Metric.ball z₀ ε, z ≠ z₀ → divisorPartialProduct m f s z ≠ 0 := by  intro z hz hz0  have hfac :      ∀ p ∈ s, weierstrassFactor m (z / divisorZeroIndex₀_val p) ≠ 0 := by    intro p hp    exact weierstrassFactor_div_ne_zero_on_ball_punctured      (m := m) (f := f) (z₀ := z₀) (ε := ε) hball z hz hz0 p  simpa [divisorPartialProduct, Finset.prod_ne_zero_iff] using hfac