Source indexedtheorem · leanprover/lean4:v4.32.0

Complex.Hadamard.analyticOrderAt_divisorCanonicalProduct_at_index

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Divisor · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/Divisor.lean:282 to 297

Source documentation

At a nonzero divisor index, the canonical product has the same multiplicity as the original function.

Exact Lean statement

theorem analyticOrderAt_divisorCanonicalProduct_at_index
    (m : ℕ) {f : ℂ → ℂ} (hf : Differentiable ℂ f)
    (h_sum : Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>
      ‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1)))
    (p : divisorZeroIndex₀ f (Set.univ : Set ℂ)) :
    analyticOrderAt (divisorCanonicalProduct m f (Set.univ : Set ℂ)) (divisorZeroIndex₀_val p) =
      (analyticOrderNatAt f (divisorZeroIndex₀_val p) : ℕ∞)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem analyticOrderAt_divisorCanonicalProduct_at_index    (m : ℕ) {f : ℂ → ℂ} (hf : Differentiable ℂ f)    (h_sum : Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>      ‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1)))    (p : divisorZeroIndex₀ f (Set.univ : Set ℂ)) :    analyticOrderAt (divisorCanonicalProduct m f (Set.univ : Set ℂ)) (divisorZeroIndex₀_val p) =      (analyticOrderNatAt f (divisorZeroIndex₀_val p) : ℕ∞) := by  have horder :=    analyticOrderAt_divisorCanonicalProduct_eq_fiber_card      (m := m) (f := f) (h_sum := h_sum) (z₀ := divisorZeroIndex₀_val p)  have hfiber :      (divisorZeroIndex₀_fiberFinset (f := f) (divisorZeroIndex₀_val p)).card =        analyticOrderNatAt f (divisorZeroIndex₀_val p) :=    divisorZeroIndex₀_fiberFinset_card_eq_analyticOrderNatAt      (hf := hf) (z₀ := divisorZeroIndex₀_val p) p.property  simpa [hfiber] using horder