Source indexedtheorem · leanprover/lean4:v4.32.0

Real.exists_norm_le_exp_mul_pow_of_rpow_bound

PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.ExpGrowth · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Log/ExpGrowth.lean:115 to 127

Source documentation

A pointwise exponential bound with real exponent can be weakened to a natural exponent.

Exact Lean statement

theorem exists_norm_le_exp_mul_pow_of_rpow_bound
    {f : α → E} {r : α → ℝ} {τ : ℝ} {n : ℕ} (hr : ∀ x, 1 ≤ r x) (hτn : τ < (n : ℝ))
    (hbound : ∃ C > 0, ∀ x, ‖f x‖ ≤ Real.exp (C * (r x) ^ τ)) :
    ∃ C > 0, ∀ x, ‖f x‖ ≤ Real.exp (C * (r x) ^ n)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem exists_norm_le_exp_mul_pow_of_rpow_bound    {f : α → E} {r : α → ℝ} {τ : ℝ} {n : ℕ} (hr : ∀ x, 1 ≤ r x) (hτn : τ < (n : ℝ))    (hbound : ∃ C > 0, ∀ x, ‖f x‖ ≤ Real.exp (C * (r x) ^ τ)) :    ∃ C > 0, ∀ x, ‖f x‖ ≤ Real.exp (C * (r x) ^ n) := by  rcases hbound with ⟨C, hCpos, hC⟩  have hweak :      ∀ x, ‖f x‖ ≤ Real.exp (C * (r x) ^ (n : ℝ)) :=    norm_le_exp_mul_rpow_of_exponent_le      (f := f) (r := r) hCpos.le hr (le_of_lt hτn) hC  refine ⟨C, hCpos, ?_⟩  intro x  have hpow : (r x) ^ (n : ℝ) = (r x) ^ n := Real.rpow_natCast (r x) n  simpa [hpow] using hweak x