Source indexedtheorem · leanprover/lean4:v4.32.0

Complex.Hadamard.natDegree_le_floor_of_exp_eval_norm_bound

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ExpPoly.Growth · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/ExpPoly/Growth.lean:371 to 384

Source documentation

A norm bound for exp (P z) gives the corresponding polynomial degree bound.

Exact Lean statement

theorem natDegree_le_floor_of_exp_eval_norm_bound {τ : ℝ} (hτ : 0 ≤ τ) (P : Polynomial ℂ)
    (hbound :
      ∃ C > 0, ∀ z : ℂ,
        ‖Complex.exp (Polynomial.eval z P)‖ ≤ Real.exp (C * (1 + ‖z‖) ^ τ)) :
    P.natDegree ≤ Nat.floor τ

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem natDegree_le_floor_of_exp_eval_norm_bound {τ : ℝ} (hτ : 0 ≤ τ) (P : Polynomial ℂ)    (hbound :      ∃ C > 0, ∀ z : ℂ,        ‖Complex.exp (Polynomial.eval z P)‖ ≤ Real.exp (C * (1 + ‖z‖) ^ τ)) :    P.natDegree ≤ Nat.floor τ := by  rcases hbound with ⟨C, hCpos, hC⟩  have hlog_growth :      ∃ C > 0, ∀ z : ℂ,        Real.log (1 + ‖Complex.exp (Polynomial.eval z P)‖) ≤ C * (1 + ‖z‖) ^ τ :=    Real.log_growth_of_norm_le_exp_mul_rpow      (f := fun z : ℂ => Complex.exp (Polynomial.eval z P))      (r := fun z : ℂ => 1 + ‖z‖) hCpos hτ      (fun z => by linarith [norm_nonneg z]) hC  exact natDegree_le_floor_of_growth_exp_eval (ρ := τ) hτ P hlog_growth