Source indexedtheorem · leanprover/lean4:v4.32.0

Real.exp_mul_rpow_le_exp_mul_rpow_of_le_mul

PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.ExpGrowth · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Log/ExpGrowth.lean:166 to 173

Source documentation

A multiplicative radius comparison gives the corresponding exponential rpow comparison.

Exact Lean statement

theorem exp_mul_rpow_le_exp_mul_rpow_of_le_mul
    {A B x y τ : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (hx : 0 ≤ x) (hy : 0 ≤ y)
    (hτ : 0 ≤ τ) (hxy : x ≤ B * y) : Real.exp (A * x ^ τ) ≤ Real.exp ((A * B ^ τ) * y ^ τ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem exp_mul_rpow_le_exp_mul_rpow_of_le_mul    {A B x y τ : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (hx : 0 ≤ x) (hy : 0 ≤ y)    (hτ : 0 ≤ τ) (hxy : x ≤ B * y) : Real.exp (A * x ^ τ) ≤ Real.exp ((A * B ^ τ) * y ^ τ) := by  refine Real.exp_le_exp.2 ?_  have hpow : x ^ τ ≤ (B * y) ^ τ := Real.rpow_le_rpow hx hxy hτ  have hsplit : (B * y) ^ τ = B ^ τ * y ^ τ := by    simpa using (Real.mul_rpow (x := B) (y := y) (z := τ) hB hy)  simpa [mul_assoc] using mul_le_mul_of_nonneg_left (hpow.trans_eq hsplit) hA