Source indexedtheorem · leanprover/lean4:v4.32.0

Real.log_growth_of_norm_le_exp_mul_rpow

PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.ExpGrowth · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Log/ExpGrowth.lean:97 to 112

Source documentation

Convert a pointwise exponential norm bound into a logarithmic growth bound.

Exact Lean statement

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

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem log_growth_of_norm_le_exp_mul_rpow    {f : α → E} {r : α → ℝ} {C τ : ℝ} (hC : 0 < C) (hτ : 0 ≤ τ)    (hr : ∀ x, 1 ≤ r x) (hbound : ∀ x, ‖f x‖ ≤ Real.exp (C * (r x) ^ τ)) :    ∃ C' > 0, ∀ x, Real.log (1 + ‖f x‖) ≤ C' * (r x) ^ τ := by  refine ⟨C + Real.log 2, by    have hlog2 : 0 ≤ Real.log 2 := Real.log_nonneg (by norm_num)    linarith, ?_⟩  intro x  have hX : (1 : ℝ) ≤ (r x) ^ τ := Real.one_le_rpow (hr x) hτ  have hB : 0 ≤ C * (r x) ^ τ :=    mul_nonneg hC.le (Real.rpow_nonneg (le_trans zero_le_one (hr x)) _)  have hlog :      Real.log (1 + ‖f x‖) ≤ C * (r x) ^ τ + Real.log 2 :=    Real.log_one_add_le_add_log_two_of_le_exp (norm_nonneg _) hB (hbound x)  have hlog2_nonneg : 0 ≤ Real.log 2 := Real.log_nonneg (by norm_num)  nlinarith [hlog, hX, hlog2_nonneg]