MeasureTheory.eLorentzNorm_add_le''

theorem eLorentzNorm_add_le'' :    eLorentzNorm (f + g) p q μ ≤ 2 ^ p.toReal⁻¹ * LpAddConst q * (eLorentzNorm f p q μ + eLorentzNorm g p q μ) := by  unfold eLorentzNorm  split_ifs with p_zero p_top q_zero q_top  · simp  · simp  · unfold LpAddConst    simp only [p_top, toReal_top, _root_.inv_zero, rpow_zero, q_top, Set.mem_Ioo, zero_lt_top,      not_top_lt, and_false, ↓reduceIte, mul_one, one_mul]    exact eLpNormEssSup_add_le  · simp only [p_top, toReal_top, _root_.inv_zero, rpow_zero, one_mul]    rw [← mul_add, ← mul_assoc, ENNReal.mul_top]    · gcongr      exact eLpNormEssSup_add_le    unfold LpAddConst    split_ifs <;> simp  rw [eLorentzNorm'_eq p_zero p_top]  calc _    _ ≤ eLpNorm (fun (t : ℝ≥0) ↦ ↑t ^ p⁻¹.toReal * (rearrangement f (t / 2) μ + rearrangement g (t / 2) μ))          q (volume.withDensity (fun (t : ℝ≥0) ↦ t⁻¹)) := by      apply eLpNorm_mono_enorm      intro t      simp only [ENNReal.toReal_inv, enorm_eq_self]      gcongr      convert! rearrangement_add_le      simp    _ ≤ LpAddConst q * (eLpNorm (fun (t : ℝ≥0) ↦ ↑t ^ p⁻¹.toReal * rearrangement f (t / 2) μ) q (volume.withDensity (fun (t : ℝ≥0) ↦ t⁻¹))        + eLpNorm (fun (t : ℝ≥0) ↦ ↑t ^ p⁻¹.toReal * rearrangement g (t / 2) μ) q (volume.withDensity (fun (t : ℝ≥0) ↦ t⁻¹))) := by      simp_rw [mul_add ( _ ^ _)]      apply eLpNorm_add_le' (by fun_prop) (by fun_prop)    _ = LpAddConst q * 2 ^ p.toReal⁻¹ * (eLpNorm (fun (t : ℝ≥0) ↦ ↑t ^ p⁻¹.toReal * rearrangement f t μ) q (volume.withDensity (fun (t : ℝ≥0) ↦ t⁻¹))        + eLpNorm (fun (t : ℝ≥0) ↦ ↑t ^ p⁻¹.toReal * rearrangement g t μ) q (volume.withDensity (fun (t : ℝ≥0) ↦ t⁻¹))) := by      rw [mul_assoc]      congr      rw [← eLpNorm_withDensity_scale_constant' (a := 2) (by fun_prop) (by norm_num)]      nth_rw 2 [← eLpNorm_withDensity_scale_constant' (a := 2) (by fun_prop) (by norm_num)]      simp only [coe_mul, coe_ofNat]      conv in (2 * _) ^ p⁻¹.toReal => rw [ENNReal.mul_rpow_of_nonneg _ _ (by simp)]      conv in (2 * _) ^ p⁻¹.toReal => rw [ENNReal.mul_rpow_of_nonneg _ _ (by simp)]      have : ∀ {f : α → ε}, (fun (t : ℝ≥0) ↦ 2 ^ p⁻¹.toReal * t ^ p⁻¹.toReal * rearrangement f (2 * t / 2) μ)          = (2 : ℝ≥0∞) ^ p⁻¹.toReal • fun (t : ℝ≥0) ↦ t ^ p⁻¹.toReal * rearrangement f (2 * t / 2) μ := by        intro f        ext t        simp only [toReal_inv, Pi.smul_apply, smul_eq_mul]        ring      rw [this, this, eLpNorm_const_smul'' (by simp), eLpNorm_const_smul'' (by simp), ← mul_add]      congr      · simp      all_goals      · ext t        congr        rw [mul_div_assoc]        apply ENNReal.mul_div_cancel          <;> norm_num    _ = 2 ^ p.toReal⁻¹ * LpAddConst q * (eLorentzNorm' f p q μ + eLorentzNorm' g p q μ) := by      rw [mul_comm (LpAddConst q)]      symm; congr <;>      · exact eLorentzNorm'_eq p_zero p_top