Source indexedtheorem · leanprover/lean4:v4.32.0

Complex.Hadamard.hadamard_factorization_of_order_centered_reindex

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Order · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/HadamardFactorization/Order.lean:283 to 302

Source documentation

Reindexed centered finite-order Hadamard factorization, for any index type equivalent to the centered nonzero divisor indices.

Exact Lean statement

theorem hadamard_factorization_of_order_centered_reindex {ι : Type*} {f : ℂ → ℂ} {ρ : ℝ}
    (hρ : 0 ≤ ρ) (c : ℂ) (hnot : ∃ z : ℂ, f z ≠ 0)
    (horder : EntireOfOrderAtMost ρ f)
    (e : ι ≃ divisorZeroIndex₀ (fun w : ℂ => f (w + c)) (Set.univ : Set ℂ)) :
    ∃ (P : Polynomial ℂ),
      P.degree ≤ Nat.floor ρ ∧
      ∀ z : ℂ,
        f z =
          Complex.exp (Polynomial.eval (z - c) P) *
            (z - c) ^ (analyticOrderNatAt f c) *
            (∏' i : ι, weierstrassFactor (Nat.floor ρ)
              ((z - c) / divisorZeroIndex₀_val (e i)))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem hadamard_factorization_of_order_centered_reindex {ι : Type*} {f : ℂ → ℂ} {ρ : ℝ}    (hρ : 0 ≤ ρ) (c : ℂ) (hnot : ∃ z : ℂ, f z ≠ 0)    (horder : EntireOfOrderAtMost ρ f)    (e : ι ≃ divisorZeroIndex₀ (fun w : ℂ => f (w + c)) (Set.univ : Set ℂ)) :    ∃ (P : Polynomial ℂ),      P.degree ≤ Nat.floor ρ ∧      ∀ z : ℂ,        f z =          Complex.exp (Polynomial.eval (z - c) P) *            (z - c) ^ (analyticOrderNatAt f c) *            (∏' i : ι, weierstrassFactor (Nat.floor ρ)              ((z - c) / divisorZeroIndex₀_val (e i))) := by  classical  rcases hadamard_factorization_of_order_centered      (f := f) (ρ := ρ) hρ c hnot horder with    ⟨P, hdeg, hfac⟩  refine ⟨P, hdeg, ?_⟩  intro z  simpa [divisorCanonicalProduct_eq_tprod_of_equiv (m := Nat.floor ρ)      (f := fun w : ℂ => f (w + c)) (U := Set.univ) e (z - c)] using hfac z