Source indexedtheorem · leanprover/lean4:v4.32.0

Complex.Hadamard.hadamard_factorization_of_order_reindex

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Order · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/HadamardFactorization/Order.lean:206 to 224

Source documentation

Reindexed form of hadamard_factorization_of_order, for any index type equivalent to the nonzero divisor indices.

Exact Lean statement

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

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

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