Source indexedtheorem · leanprover/lean4:v4.32.0

Complex.Hadamard.divisorCanonicalProduct_ne_zero_of_forall_ne

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Divisor · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/Divisor.lean:239 to 265

Source documentation

Away from the indexed divisor, the divisor canonical product is nonzero.

Exact Lean statement

theorem divisorCanonicalProduct_ne_zero_of_forall_ne
    (m : ℕ) (f : ℂ → ℂ)
    (h_sum : Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>
      ‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1)))
    {z : ℂ} (hz : ∀ p : divisorZeroIndex₀ f (Set.univ : Set ℂ), z ≠ divisorZeroIndex₀_val p) :
    divisorCanonicalProduct m f (Set.univ : Set ℂ) z ≠ 0

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem divisorCanonicalProduct_ne_zero_of_forall_ne    (m : ℕ) (f : ℂ → ℂ)    (h_sum : Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>      ‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1)))    {z : ℂ} (hz : ∀ p : divisorZeroIndex₀ f (Set.univ : Set ℂ), z ≠ divisorZeroIndex₀_val p) :    divisorCanonicalProduct m f (Set.univ : Set ℂ) z ≠ 0 := by  let F : ℂ → ℂ := divisorCanonicalProduct m f (Set.univ : Set ℂ)  have hfiber_empty : divisorZeroIndex₀_fiberFinset (f := f) z = ∅ := by    ext p    constructor    · intro hp      exact False.elim (hz p ((mem_divisorZeroIndex₀_fiberFinset (f := f) (z₀ := z) p).1 hp).symm)    · intro hp      simp at hp  have horder :      analyticOrderAt F z = (0 : ℕ∞) := by    have h :=      analyticOrderAt_divisorCanonicalProduct_eq_fiber_card        (m := m) (f := f) (h_sum := h_sum) (z₀ := z)    simpa [F, hfiber_empty] using h  have han : AnalyticAt ℂ F z := by    refine (Complex.analyticAt_iff_eventually_differentiableAt).2 ?_    refine Filter.Eventually.of_forall ?_    intro w    exact (((differentiableOn_divisorCanonicalProduct_univ m f h_sum) w      (by simp)).differentiableAt (by simp))  exact (han.analyticOrderAt_eq_zero).1 horder