Source indexedlemma · leanprover/lean4:v4.32.0

ENNReal.rpow_le_rpow_of_exponent_le_base_le

Carleson.ToMathlib.RealInterpolation.InterpolatedExponents · Carleson/ToMathlib/RealInterpolation/InterpolatedExponents.lean:201 to 217

Mathematical statement

Exact Lean statement

lemma rpow_le_rpow_of_exponent_le_base_le {a b t γ : ℝ} (ht : 0 < t) (htγ : t ≤ γ) (hab : a ≤ b) :
    ENNReal.ofReal (t ^ b) ≤ ENNReal.ofReal (t ^ a) * ENNReal.ofReal (γ ^ (b - a))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma rpow_le_rpow_of_exponent_le_base_le {a b t γ : ℝ} (ht : 0 < t) (htγ : t ≤ γ) (hab : a ≤ b) :    ENNReal.ofReal (t ^ b) ≤ ENNReal.ofReal (t ^ a) * ENNReal.ofReal (γ ^ (b - a)) := by  rw [mul_comm]  have γ_pos : 0 < γ := lt_of_lt_of_le ht htγ  rw [Real.rpow_sub γ_pos]  refine (ENNReal.mul_le_mul_iff_right (a := ENNReal.ofReal (γ ^ (-b) )) ?_ coe_ne_top).mp ?_  · exact (ofReal_pos.mpr (Real.rpow_pos_of_pos γ_pos (-b))).ne'  · rw [← ofReal_mul, ← mul_assoc, ← ofReal_mul, ← mul_div_assoc, ← Real.rpow_add, neg_add_cancel,        Real.rpow_zero, ← ofReal_mul, mul_comm] <;> try positivity    nth_rw 2 [mul_comm]    rw [← neg_one_mul, Real.rpow_mul, Real.rpow_neg_one, ← Real.mul_rpow] <;> try positivity    rw [one_div]    nth_rw 2 [← Real.rpow_neg_one]    rw [← Real.rpow_mul (by positivity)]    nth_rw 3 [mul_comm]    rw [Real.rpow_mul, Real.rpow_neg_one, ← Real.mul_rpow, ← div_eq_mul_inv] <;> try positivity    exact ofReal_le_ofReal (power_estimate' ht htγ hab)