Source indexedtheorem · leanprover/lean4:v4.32.0

MeasureTheory.antitone_rpow_inv_sub_inv

Carleson.ToMathlib.MeasureTheory.Function.LorentzSeminorm.TriangleInequality · Carleson/ToMathlib/MeasureTheory/Function/LorentzSeminorm/TriangleInequality.lean:148 to 164

Mathematical statement

Exact Lean statement

theorem antitone_rpow_inv_sub_inv (q_le_p : q ≤ p) (q_zero : q ≠ 0) :
    Antitone fun (x : ℝ≥0) ↦ (ENNReal.ofNNReal x) ^ (p.toReal⁻¹ - q.toReal⁻¹)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem antitone_rpow_inv_sub_inv (q_le_p : q ≤ p) (q_zero : q ≠ 0) :    Antitone fun (x : ℝ≥0) ↦ (ENNReal.ofNNReal x) ^ (p.toReal⁻¹ - q.toReal⁻¹) := by  have p_zero : p ≠ 0 := by    aesop  intro x y h  simp only  apply ENNReal.rpow_le_rpow_of_nonpos _ (by simpa)  simp only [tsub_le_iff_right, zero_add]  by_cases p_top : p = ⊤  · rw [p_top]    simp  have q_top : q ≠ ⊤ := by    aesop  rw [inv_le_inv₀]  · rwa [ENNReal.toReal_le_toReal q_top p_top]  · exact ENNReal.toReal_pos p_zero p_top  · exact ENNReal.toReal_pos q_zero q_top