Source indexedtheorem · leanprover/lean4:v4.32.0

Complex.Hadamard.analyticOrderAt_divisorCanonicalProduct_eq_fiber_card

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Divisor · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/Divisor.lean:209 to 236

Source documentation

The analytic order of the divisor-indexed canonical product at z₀ is the number of divisor indices lying over z₀.

Exact Lean statement

theorem analyticOrderAt_divisorCanonicalProduct_eq_fiber_card
    (m : ℕ) (f : ℂ → ℂ)
    (h_sum : Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>
      ‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1)))
    (z₀ : ℂ) :
    analyticOrderAt (divisorCanonicalProduct m f (Set.univ : Set ℂ)) z₀ =
      ((divisorZeroIndex₀_fiberFinset (f := f) z₀).card : ℕ∞)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem analyticOrderAt_divisorCanonicalProduct_eq_fiber_card    (m : ℕ) (f : ℂ → ℂ)    (h_sum : Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>      ‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1)))    (z₀ : ℂ) :    analyticOrderAt (divisorCanonicalProduct m f (Set.univ : Set ℂ)) z₀ =      ((divisorZeroIndex₀_fiberFinset (f := f) z₀).card : ℕ∞) := by  let F : ℂ → ℂ := divisorCanonicalProduct m f (Set.univ : Set ℂ)  have hNat :      analyticOrderNatAt F z₀ = (divisorZeroIndex₀_fiberFinset (f := f) z₀).card := by    simpa [F] using      (analyticOrderNatAt_divisorCanonicalProduct_eq_fiber_card        (m := m) (f := f) (h_sum := h_sum) (z₀ := z₀))  have hdiffOn : DifferentiableOn ℂ F (Set.univ : Set ℂ) := by    simpa [F] using differentiableOn_divisorCanonicalProduct_univ (m := m) (f := f) h_sum  have hdiff : Differentiable ℂ F := by    intro z    exact (hdiffOn z (by simp)).differentiableAt (by simp)  have hnotTop : analyticOrderAt F z₀ ≠ ⊤ :=    analyticOrderAt_ne_top_of_exists_ne_zero (hf := hdiff)      ⟨0, by simp [F, divisorCanonicalProduct_zero]⟩ z₀  have hcast : (analyticOrderNatAt F z₀ : ℕ∞) = analyticOrderAt F z₀ :=    Nat.cast_analyticOrderNatAt (f := F) (z₀ := z₀) hnotTop  have hNatCast :      (analyticOrderNatAt F z₀ : ℕ∞) =        ((divisorZeroIndex₀_fiberFinset (f := f) z₀).card : ℕ∞) := by    simp [hNat]  simpa [F, hcast] using hNatCast