MeasureTheory.wnorm'_eq_iSup_rpow_mul_rearrangement

theorem wnorm'_eq_iSup_rpow_mul_rearrangement {p : ℝ} (hp : 0 < p) {f : α → ε} {μ : Measure α} :    wnorm' f p μ = ⨆ t : ℝ≥0, t ^ p⁻¹ * rearrangement f t μ := by  have hp' : 0 < p⁻¹ := by simpa  unfold wnorm'  calc _    _ = ⨆ t, t * distribution f t μ ^ p⁻¹ := by      rw [ENNReal.iSup_ennreal]      simp only [distibution_top, left_eq_sup]      rw [ENNReal.zero_rpow_of_pos hp', mul_zero]      exact zero_le  symm  calc _    _ = ⨆ t, t ^ p⁻¹ * rearrangement f t μ := by      rw [ENNReal.iSup_ennreal]      simp  symm  apply le_antisymm  · apply iSup_le    intro t    apply le_of_forall_lt    intro a ha    by_cases! a_ne_zero : a = 0    · rw [a_ne_zero]      rw [a_ne_zero] at ha      rw [lt_iSup_iff]      contrapose! ha      simp only [nonpos_iff_eq_zero, mul_eq_zero] at *      simp_rw [ENNReal.rpow_eq_zero_iff_of_pos hp'] at *      by_cases ht : t = 0      · left        assumption      · right        rw [← nonpos_iff_eq_zero]        apply _root_.le_of_forall_pos_le_add        intro ε hε        rw [zero_add, ← rearrangement_le_iff_distribution_le]        rcases ha ε with h | h        · order        rw [h]        exact zero_le    have a_ne_top : a ≠ ∞ := ha.ne_top    rw [lt_iSup_iff]    use (a / t) ^ p    rw [ENNReal.rpow_rpow_inv hp.ne']    rw [ENNReal.mul_comm_div]    nth_rw 1 [← mul_one a]    gcongr    rw [ENNReal.lt_div_iff_mul_lt (by simp) (by simp), one_mul, lt_rearrangement_iff_lt_distribution]    apply (ENNReal.lt_rpow_inv_iff hp).mp    rwa [ENNReal.div_lt_iff (by right; assumption) (by right; assumption), mul_comm]  · apply iSup_le    intro t    apply le_of_forall_lt    intro a ha    by_cases! a_ne_zero : a = 0    · rw [a_ne_zero]      rw [a_ne_zero] at ha      rw [lt_iSup_iff]      contrapose! ha      simp only [nonpos_iff_eq_zero, mul_eq_zero] at *      simp_rw [ENNReal.rpow_eq_zero_iff_of_pos hp'] at *      by_cases ht : t = 0      · left        assumption      · right        rw [← nonpos_iff_eq_zero]        apply _root_.le_of_forall_pos_le_add        intro ε hε        rw [zero_add, rearrangement_le_iff_distribution_le]        rcases ha ε with h | h        · order        rw [h]        exact zero_le    have a_ne_top : a ≠ ∞ := ha.ne_top    rw [lt_iSup_iff]    use a / t ^ p⁻¹    rw [ENNReal.mul_comm_div]    nth_rw 1 [← mul_one a]    gcongr    rw [ENNReal.lt_div_iff_mul_lt (by simp) (by simp), one_mul]    gcongr    rw [← lt_rearrangement_iff_lt_distribution]    rwa [ENNReal.div_lt_iff (by right; assumption) (by right; assumption), mul_comm]