Source indexedlemma · leanprover/lean4:v4.32.0

ENNReal.rpow_le_rpow_of_exponent_le_base_ge_enorm

Carleson.ToMathlib.RealInterpolation.InterpolatedExponents · Carleson/ToMathlib/RealInterpolation/InterpolatedExponents.lean:247 to 275

Mathematical statement

Exact Lean statement

lemma rpow_le_rpow_of_exponent_le_base_ge_enorm {a b : ℝ} {t γ : ℝ≥0∞} (hγ : 0 < γ) (hγ' : γ ≠ ∞) (htγ : γ ≤ t) (hab : a ≤ b) :
    t ^ a ≤ (t ^ b) * (γ ^ (a - b))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma rpow_le_rpow_of_exponent_le_base_ge_enorm {a b : ℝ} {t γ : ℝ≥0∞} (hγ : 0 < γ) (hγ' : γ ≠ ∞) (htγ : γ ≤ t) (hab : a ≤ b) :    t ^ a ≤ (t ^ b) * (γ ^ (a - b)) := by  by_cases ht' : t = ∞  · simp_all only [le_top, top_rpow_def, ite_mul, sub_zero, one_mul, zero_mul]    split_ifs with ha hb hb' ha'    · simp_all    · exact False.elim (by linarith [hb, hb'])    · exact False.elim (by linarith [hb, hb'])    · simp_all    · simp_all    · simpa using by order    · rw [ENNReal.top_mul]      · exact zero_le      simp_all    · positivity    · simp  have t_pos : 0 < t := lt_of_le_of_lt' htγ hγ  rw [mul_comm, ← ENNReal.inv_mul_le_iff, ← ENNReal.rpow_neg, mul_comm, ENNReal.mul_le_iff_le_inv,    ← ENNReal.rpow_neg, ← ENNReal.rpow_add, neg_sub, add_comm, sub_eq_add_neg]  · gcongr    linarith  · positivity  · assumption  · simp_all only [ne_eq, ENNReal.rpow_eq_zero_iff, false_and, or_false, not_and, not_lt]    contrapose    exact fun _ ↦ t_pos.ne'  · simpa [ht'] using fun hfalse ↦ by simp_all  · simp_all  · simpa using ⟨fun h ↦ by simp_all, fun h ↦ by simp_all⟩