Source indexedlemma · leanprover/lean4:v4.32.0

ENNReal.rpow_le_rpow_of_exponent_le_base_ge

Carleson.ToMathlib.RealInterpolation.InterpolatedExponents · Carleson/ToMathlib/RealInterpolation/InterpolatedExponents.lean:229 to 245

Mathematical statement

Exact Lean statement

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

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma rpow_le_rpow_of_exponent_le_base_ge {a b t γ : ℝ} (hγ : 0 < γ) (htγ : γ ≤ t) (hab : a ≤ b) :    ENNReal.ofReal (t ^ a) ≤ ENNReal.ofReal (t ^ b) * ENNReal.ofReal (γ ^ (a - b)) := by  rw [mul_comm]  have t_pos : 0 < t := lt_of_le_of_lt' htγ hγ  rw [Real.rpow_sub hγ]  refine (ENNReal.mul_le_mul_iff_right (a := ENNReal.ofReal (γ ^ (-a) )) ?_ coe_ne_top).mp ?_  · exact (ofReal_pos.mpr (Real.rpow_pos_of_pos hγ (-a))).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 (Real.rpow_le_rpow_of_exponent_le ((one_le_div hγ).mpr htγ) hab)