Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.eLorentzNorm'_eq_lintegral_lorentz_helper_mul

Carleson.ToMathlib.MeasureTheory.Function.LorentzSeminorm.TriangleInequality · Carleson/ToMathlib/MeasureTheory/Function/LorentzSeminorm/TriangleInequality.lean:183 to 222

Mathematical statement

Exact Lean statement

lemma eLorentzNorm'_eq_lintegral_lorentz_helper_mul (p_ne_zero : p ≠ 0) (p_ne_top : p ≠ ⊤)
  (hq : 1 ≤ q) (q_ne_top : q ≠ ⊤) (f_ne_top : eLorentzNorm' f p q μ ≠ ⊤) :
    eLorentzNorm' f p q μ
      = eLpNorm (lorentz_helper f p q μ * fun (t : ℝ≥0) ↦ t ^ (p⁻¹.toReal - q⁻¹.toReal) * rearrangement f t μ) 1

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma eLorentzNorm'_eq_lintegral_lorentz_helper_mul (p_ne_zero : p ≠ 0) (p_ne_top : p ≠ ⊤)  (hq : 1 ≤ q) (q_ne_top : q ≠ ⊤) (f_ne_top : eLorentzNorm' f p q μ ≠ ⊤) :    eLorentzNorm' f p q μ      = eLpNorm (lorentz_helper f p q μ * fun (t : ℝ≥0) ↦ t ^ (p⁻¹.toReal - q⁻¹.toReal) * rearrangement f t μ) 1 := by  unfold lorentz_helper  simp only [Algebra.smul_mul_assoc]  rw [eLpNorm_const_smul''' (by fun_prop), Pi.mul_def]  conv =>    rhs    congr    rfl    congr    intro t    rw [mul_comm]    congr    rw [← ENNReal.rpow_one (_ * rearrangement _ _ _)]  conv =>    rhs    congr    rfl    congr    intro t    rw [← ENNReal.rpow_add_of_nonneg, add_sub_cancel]    rfl    exact zero_le_one    tactic =>      simp only [sub_nonneg]      rw [← ENNReal.ofReal_le_iff_le_toReal q_ne_top]      simpa  conv =>    rhs    congr; rfl    congr    intro t    congr    rw [← enorm_eq_self (_ * _)]  rw [eLpNorm_enorm_rpow _ (ENNReal.toReal_pos (by aesop) q_ne_top)]  rw [one_mul, ENNReal.ofReal_toReal q_ne_top]  rw [← eLorentzNorm'_eq' p_ne_zero p_ne_top, ← ENNReal.rpow_add_of_add_pos f_ne_top _ _ (by simp)]  simp