MeasureTheory.eLorentzNorm_add_le

theorem eLorentzNorm_add_le [ContinuousAdd ε] (one_le_q : 1 ≤ q) (q_le_p : q ≤ p)     (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) :      eLorentzNorm (f + g) p 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  · exact eLpNormEssSup_add_le  · rw [← mul_add]    gcongr    exact eLpNormEssSup_add_le  have q_top : q ≠ ⊤ := by aesop  by_cases hfg : eLorentzNorm' (f + g) p q μ = 0  · rw [hfg]    simp  by_cases hfg' : eLorentzNorm' (f + g) p q μ = ⊤  · have := eLorentzNorm_add_le'' (p := p) (q := q) (f := f) (g := g) (μ := μ)    rw [eLorentzNorm_eq_eLorentzNorm' p_zero p_top,        eLorentzNorm_eq_eLorentzNorm' p_zero p_top,        eLorentzNorm_eq_eLorentzNorm' p_zero p_top, hfg'] at this    simp only [top_le_iff] at this    rw [mul_eq_top] at this    rcases this with ⟨_, h⟩ | ⟨h, _⟩    · rw [h]      simp    · contrapose! h      apply mul_ne_top (by simp) (LpAddConst_lt_top _).ne  rw [eLorentzNorm'_eq_lintegral_lorentz_helper_mul p_zero p_top one_le_q q_top hfg']  calc _    _ ≤ eLpNorm (lorentz_helper (f + g) p q μ * fun (t : ℝ≥0) ↦ t ^ (p⁻¹.toReal - q⁻¹.toReal) * (rearrangement f t μ + rearrangement g t μ)) 1 := by      rw [eLpNorm_one_eq_lintegral_enorm, eLpNorm_one_eq_lintegral_enorm]      simp only [toReal_inv, Pi.mul_apply, enorm_eq_self]      simp_rw [← mul_assoc]      apply lintegral_antitone_mul_le (by fun_prop) (by fun_prop)      · intro t        apply (le_lintegral_add _ _).trans'        have := lintegral_rearrangement_add_rearrangement_le_add_lintegral hf hg (t := t)        rw [setLIntegral_ennreal_eq_setLintegral_of_nnreal measurableSet_Iio,            setLIntegral_ennreal_eq_setLintegral_of_nnreal measurableSet_Iio,            setLIntegral_ennreal_eq_setLintegral_of_nnreal measurableSet_Iio] at this        convert this <;> aesop      · apply Antitone.mul' (antitone_lorentz_helper one_le_q q_le_p p_top) (antitone_rpow_inv_sub_inv q_le_p (zero_lt_one.trans_le one_le_q).ne')    _ ≤ eLpNorm (lorentz_helper (f + g) p q μ * fun (t : ℝ≥0) ↦ t ^ (p⁻¹.toReal - q⁻¹.toReal) * rearrangement f t μ) 1        + eLpNorm (lorentz_helper (f + g) p q μ * fun (t : ℝ≥0) ↦ t ^ (p⁻¹.toReal - q⁻¹.toReal) * rearrangement g t μ) 1 := by      apply (eLpNorm_add_le (by fun_prop) (by fun_prop) le_rfl).trans'      apply le_of_eq      congr      rw [← mul_add]      congr with t      simp      ring    _ ≤ eLpNorm (lorentz_helper (f + g) p q μ) q.conjExponent * eLpNorm (fun (t : ℝ≥0) ↦ t ^ (p⁻¹.toReal - q⁻¹.toReal) * rearrangement f t μ) q        + eLpNorm (lorentz_helper (f + g) p q μ) q.conjExponent * eLpNorm (fun (t : ℝ≥0) ↦ t ^ (p⁻¹.toReal - q⁻¹.toReal) * rearrangement g t μ) q := by      gcongr <;>      · apply eLpNorm_le_eLpNorm_mul_eLpNorm_of_enorm' (by fun_prop) (by fun_prop) (HolderConjugate.conjExponent one_le_q).symm    _ = eLorentzNorm' f p q μ + eLorentzNorm' g p q μ := by      rw [eLpNorm_lorentz_helper p_zero p_top one_le_q q_top hfg hfg', one_mul, one_mul,        ← eLorentzNorm'_eq' p_zero p_top, ← eLorentzNorm'_eq' p_zero p_top]