Source indexedtheorem · leanprover/lean4:v4.32.0

Complex.Hadamard.hadamard_factorization_of_order_centered

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Order · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/HadamardFactorization/Order.lean:253 to 279

Source documentation

Centered finite-order Hadamard factorization. This is derived from the origin-centered theorem by translating f by c; the product indexes zeros away from the center in centered coordinates.

Exact Lean statement

theorem hadamard_factorization_of_order_centered {f : ℂ → ℂ} {ρ : ℝ} (hρ : 0 ≤ ρ)
    (c : ℂ) (hnot : ∃ z : ℂ, f z ≠ 0)
    (horder : EntireOfOrderAtMost ρ f) :
    ∃ (P : Polynomial ℂ),
      P.degree ≤ Nat.floor ρ ∧
      ∀ z : ℂ,
        f z =
          Complex.exp (Polynomial.eval (z - c) P) *
            (z - c) ^ (analyticOrderNatAt f c) *
            divisorCanonicalProduct (Nat.floor ρ) (fun w : ℂ => f (w + c))
              (Set.univ : Set ℂ) (z - c)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem hadamard_factorization_of_order_centered {f : ℂ → ℂ} {ρ : ℝ} (hρ : 0 ≤ ρ)    (c : ℂ) (hnot : ∃ z : ℂ, f z ≠ 0)    (horder : EntireOfOrderAtMost ρ f) :    ∃ (P : Polynomial ℂ),      P.degree ≤ Nat.floor ρ ∧      ∀ z : ℂ,        f z =          Complex.exp (Polynomial.eval (z - c) P) *            (z - c) ^ (analyticOrderNatAt f c) *            divisorCanonicalProduct (Nat.floor ρ) (fun w : ℂ => f (w + c))              (Set.univ : Set ℂ) (z - c) := by  classical  let g : ℂ → ℂ := fun w : ℂ => f (w + c)  have hnot_g : ∃ w : ℂ, g w ≠ 0 := by    rcases hnot with ⟨z, hz⟩    refine ⟨z - c, ?_⟩    simpa [g] using hz  have horder_g : EntireOfOrderAtMost ρ g :=    horder.comp_add_const hρ c  rcases hadamard_factorization_of_order (f := g) (ρ := ρ) hρ hnot_g horder_g with    ⟨P, hdeg, hfac⟩  refine ⟨P, hdeg, ?_⟩  intro z  have h := hfac (z - c)  have horder0 : analyticOrderNatAt g 0 = analyticOrderNatAt f c := by    simpa [g] using analyticOrderNatAt_comp_add_const f c  simpa [g, horder0] using h