Source indexedtheorem · leanprover/lean4:v4.32.0

Real.norm_le_exp_mul_rpow_of_log_growth

PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.ExpGrowth · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Log/ExpGrowth.lean:86 to 94

Source documentation

A logarithmic growth bound gives a pointwise exponential norm bound after weakening the exponent.

Exact Lean statement

theorem norm_le_exp_mul_rpow_of_log_growth
    {f : α → E} {r : α → ℝ} {C ρ τ : ℝ} (hC : 0 ≤ C) (hr : ∀ x, 1 ≤ r x) (hρτ : ρ ≤ τ)
    (hlog : ∀ x, Real.log (1 + ‖f x‖) ≤ C * (r x) ^ ρ) : ∀ x, ‖f x‖ ≤ Real.exp (C * (r x) ^ τ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem norm_le_exp_mul_rpow_of_log_growth    {f : α → E} {r : α → ℝ} {C ρ τ : ℝ} (hC : 0 ≤ C) (hr : ∀ x, 1 ≤ r x) (hρτ : ρ ≤ τ)    (hlog : ∀ x, Real.log (1 + ‖f x‖) ≤ C * (r x) ^ ρ) : ∀ x, ‖f x‖ ≤ Real.exp (C * (r x) ^ τ) := by  intro x  have hpow : (r x) ^ ρ ≤ (r x) ^ τ :=    Real.rpow_le_rpow_of_exponent_le (hr x) hρτ  have hlogτ : Real.log (1 + ‖f x‖) ≤ C * (r x) ^ τ :=    (hlog x).trans (mul_le_mul_of_nonneg_left hpow hC)  exact Real.le_exp_of_log_one_add_le (norm_nonneg (f x)) hlogτ