MeasureTheory.eLorentzNorm'_eq

lemma eLorentzNorm'_eq (p_nonzero : p ≠ 0) (p_ne_top : p ≠ ⊤) {f : α → ε} {μ : Measure α} :  eLorentzNorm' f p q μ    = eLpNorm (fun (t : ℝ≥0) ↦ t ^ p⁻¹.toReal * rearrangement f t μ) q        (volume.withDensity (fun (t : ℝ≥0) ↦ t⁻¹)) := by  by_cases q_zero : q = 0  · rw [q_zero]    simp  by_cases q_top : q = ⊤  · rw [q_top, eLorentzNorm'_eq_wnorm p_ne_top,      wnorm_eq_iSup_rpow_mul_rearrangement p_nonzero p_ne_top]    simp only [ENNReal.toReal_inv, eLpNorm_exponent_top]    symm    rw [eLpNormEssSup_withDensity (by fun_prop) (by simp)]    apply eLpNormEssSup_nnreal_eq_iSup_nnreal (f := fun t ↦ t ^ p.toReal⁻¹ * rearrangement f t μ)    intro a x ha    apply ContinuousWithinAt.ennreal_mul    · fun_prop    · apply continuousWithinAt_rearrangement.congr_mono (Set.eqOn_refl _ _)      · simp      · simp    · rw [or_iff_not_imp_left]      push Not      intro h      exfalso      rw [h] at ha      simp at ha    · right      simp  unfold eLorentzNorm'  rw [← eLpNorm_const_smul'' (by simp; aesop), eLpNorm_eq_lintegral_rpow_enorm_toReal q_zero q_top,      eLpNorm_eq_lintegral_rpow_enorm_toReal q_zero q_top,      lintegral_withDensity_eq_lintegral_mul₀ (by fun_prop) (by fun_prop),      lintegral_withDensity_eq_lintegral_mul₀ (by fun_prop) (by fun_prop)]  congr 1  simp only [ENNReal.toReal_inv, Pi.smul_apply, smul_eq_mul, enorm_eq_self]  conv =>    lhs    congr    rfl    intro t    simp    rw [ENNReal.mul_rpow_of_nonneg _ _ (by simp),        ENNReal.rpow_inv_rpow (ENNReal.toReal_ne_zero.mpr ⟨q_zero, q_top⟩),        ENNReal.mul_rpow_of_nonneg _ _ (by simp),        ← mul_assoc, ← mul_assoc, mul_comm _ p, mul_assoc p, ← ENNReal.rpow_neg_one]  conv =>    rhs    congr    rfl    intro t    simp    rw [ENNReal.mul_rpow_of_nonneg _ _ (by simp),        ← ENNReal.rpow_mul, ← ENNReal.rpow_neg_one, ← mul_assoc]  symm  calc _    _ = ∫⁻ t, t ^ ((q / p).toReal - 1) * rearrangement f t μ ^ q.toReal := by      rw [lintegral_nnreal_eq_lintegral_Ioi_ofReal            (f := fun t => t ^ (-1) * t ^ (p.toReal⁻¹ * q.toReal) * rearrangement f t μ ^ q.toReal),          lintegral_ennreal_eq_lintegral_Ioi_ofReal            (f := fun t => t ^ ((q / p).toReal - 1) * rearrangement f t μ ^ q.toReal)]      apply setLIntegral_congr_fun measurableSet_Ioi      intro t ht      simp only [ENNReal.toReal_div]      congr      rw [inv_mul_eq_div, ← ENNReal.toReal_div, ← ENNReal.rpow_add _ _ (by simpa) (by simp)]      ring_nf    _ = ∫⁻ t, t ^ ((q / p).toReal - 1)          * (∫⁻ l in Set.Iio (rearrangement f t μ), q * l ^ (q.toReal - 1)) := by      congr with t      congr      rw [lintegral_const_mul _ (by fun_prop)]      rw [setLIntegral_Iio_rpow, sub_add_cancel, ENNReal.ofReal_toReal q_top,        ENNReal.mul_div_cancel q_zero q_top]      simp only [neg_lt_sub_iff_lt_add, lt_add_iff_pos_right]      exact ENNReal.toReal_pos q_zero q_top    _ = ∫⁻ t, (∫⁻ l, t ^ ((q / p).toReal - 1)          * (Set.Iio (rearrangement f t μ)).indicator (fun l ↦ q * l ^ (q.toReal - 1)) l) := by      congr with t      rw [← lintegral_indicator measurableSet_Iio,          ← lintegral_const_mul _ (Measurable.indicator (by fun_prop) measurableSet_Iio)]    _ = ∫⁻ l, (∫⁻ t, t ^ ((q / p).toReal - 1)          * (Set.Iio (rearrangement f t μ)).indicator (fun l ↦ q * l ^ (q.toReal - 1)) l) := by      rw [lintegral_lintegral_swap]      apply Measurable.aemeasurable      apply Measurable.mul (by fun_prop)      apply Measurable.indicator (by fun_prop)      change MeasurableSet {(a : ℝ≥0∞ × ℝ≥0∞) | a.2 ∈ Set.Iio (rearrangement f a.1 μ)}      have : {(a : ℝ≥0∞ × ℝ≥0∞) | a.2 ∈ Set.Iio (rearrangement f a.1 μ)} = ((fun a ↦ (⟨rearrangement f a.1 μ, a.2⟩ : ℝ≥0∞ × ℝ≥0∞)) ⁻¹' ({t | t.2 < t.1})) := by        ext a        simp      rw [this]      measurability    _ = ∫⁻ l, (∫⁻ t, t ^ ((q / p).toReal - 1)          * (Set.Iio (distribution f l μ)).indicator 1 t * (q * l ^ (q.toReal - 1))) := by      congr with l      congr with t      rw [mul_assoc (_ ^ _)]      congr      rw [← Set.indicator_mul_const]      simp only [Pi.one_apply, one_mul]      apply Set.indicator_const_eq_indicator_const      simp only [Set.mem_Iio]      apply lt_rearrangement_iff_lt_distribution    _ = ∫⁻ l, (∫⁻ t in Set.Iio (distribution f l μ), t ^ ((q / p).toReal - 1)) * (q * l ^ (q.toReal - 1)) := by      congr with l      rw [← lintegral_mul_const _ (by fun_prop), ← lintegral_indicator measurableSet_Iio]      congr with t      rw [Set.indicator_mul_right, mul_assoc, ← Set.indicator_mul_const]      simp    _ = ∫⁻ l, (distribution f l μ ^ (q / p).toReal / (q / p)) * (q * l ^ (q.toReal - 1)) := by      congr with l      rw [setLIntegral_Iio_rpow, sub_add_cancel,        ENNReal.ofReal_toReal (ENNReal.div_ne_top q_top p_nonzero)]      simp only [ENNReal.toReal_div, neg_lt_sub_iff_lt_add, lt_add_iff_pos_right]      exact div_pos (ENNReal.toReal_pos q_zero q_top) (ENNReal.toReal_pos p_nonzero p_ne_top)    _ = ∫⁻ l, p * l ^ (q.toReal - 1) * distribution f l μ ^ (q / p).toReal := by      congr with l      rw [← ENNReal.div_mul _ (by left; assumption) (by left; assumption), ENNReal.div_eq_inv_mul,        mul_comm, mul_comm q, mul_assoc, ← mul_assoc q, ← mul_assoc q,        ENNReal.mul_inv_cancel q_zero q_top]      ring    _ = ∫⁻ (l : ℝ≥0), p * (↑l ^ (-1 : ℝ) * ↑l ^ q.toReal) * (distribution f (↑l) μ ^ p.toReal⁻¹) ^ q.toReal := by      rw [lintegral_ennreal_eq_lintegral_Ioi_ofReal            (f := fun l => p * l ^ (q.toReal - 1) * distribution f l μ ^ (q / p).toReal),          lintegral_nnreal_eq_lintegral_Ioi_ofReal            (f := fun l => p * (l ^ (-1 : ℝ) * l ^ q.toReal) * (distribution f l μ ^ p.toReal⁻¹) ^ q.toReal)]      apply setLIntegral_congr_fun measurableSet_Ioi      intro l hl      simp only [ENNReal.toReal_div]      rw [← ENNReal.rpow_mul, inv_mul_eq_div, ← ENNReal.rpow_add _ _ (by simpa) (by simp)]      ring_nf