MeasureTheory.lintegral_rearrangement_eq

lemma lintegral_rearrangement_eq {ε} [TopologicalSpace ε] [ContinuousENorm ε] [NoAtoms' μ] {f : α → ε}  (hf : AEStronglyMeasurable f μ) {t : ℝ≥0∞} :    ∫⁻ s in Set.Iio t, rearrangement f s μ      = ⨆ (E : Set α) (_ : NullMeasurableSet E μ) (_ : μ E ≤ t), ∫⁻ x in E, ‖f x‖ₑ ∂μ := by  rw [lintegral_rearrangement_eq']  apply le_antisymm  · by_cases h_zero : rearrangement f t μ = 0    · rw [← ENNReal.bot_eq_zero, ← le_bot_iff, rearrangement_le_iff_distribution_le, ENNReal.bot_eq_zero] at h_zero      apply le_iSup_of_le (superlevelSet f 0)      apply le_iSup_of_le (nullMeasurableSet_superlevelSet hf)      apply le_iSup_of_le h_zero      rw [setLIntegral_enorm_eq hf (nullMeasurableSet_superlevelSet hf), superlevelSet]      gcongr with s      apply min_le_of_left_le      unfold distribution      gcongr      intro x      simp only [Set.mem_setOf_eq, Set.mem_inter_iff]      intro hs      simp only [hs, and_true]      apply hs.trans_le'      simp    rw [← ENNReal.bot_eq_zero, ← le_bot_iff, not_le, ENNReal.bot_eq_zero] at h_zero    have : ∀ a < rearrangement f t μ,      ∫⁻ s in (Set.Ioo a (rearrangement f t μ))ᶜ, min (distribution f s μ) t        ≤ ⨆ E, ⨆ (_ : NullMeasurableSet E μ), ⨆ (_ : μ E ≤ t), ∫⁻ (x : α) in E, ‖f x‖ₑ ∂μ := by      intro a ha      have : ∃ E, NullMeasurableSet E μ∧ superlevelSet f (rearrangement f t μ) ⊆ E ∧ E ⊆ superlevelSet f a ∧ μ E = t := by        have lb := distribution_rearrangement_le (f := f) (μ := μ) (x := t)        rw [distribution_eq_measure_superlevelSet] at lb        have ub : t ≤ μ (superlevelSet f a) := by          rw [lt_rearrangement_iff_lt_distribution] at ha          exact ha.le        apply NoAtoms'.exists_nullmeasurable_between_measure_eq (nullMeasurableSet_superlevelSet hf)          (nullMeasurableSet_superlevelSet hf) (superlevelSet_antitone ha.le) lb ub      rcases this with ⟨E, measE, hE, hE', hμE⟩      apply le_iSup_of_le E      apply le_iSup_of_le measE      apply le_iSup_of_le hμE.le      rw [setLIntegral_enorm_eq hf measE, ← lintegral_indicator measurableSet_Ioo.compl]      gcongr with s      unfold Set.indicator      simp only [Set.mem_compl_iff, Set.mem_Ioo, not_and, not_lt]      split_ifs with h      rotate_left      · simp      by_cases! h' : distribution f s μ ≤ t      · rw [min_eq_left h']        rw [← rearrangement_le_iff_distribution_le] at h'        unfold distribution        gcongr        rw [Set.inter_eq_right.mpr]        apply hE.trans'        intro x hx        simp only [Set.mem_setOf_eq] at *        exact hx.trans_le' h'      · have has : s ≤ a := by          rw [rearrangement_le_iff_distribution_le] at h          contrapose! h          exact ⟨h, h'⟩        rw [min_eq_right h'.le, ← hμE]        gcongr        rw [Set.inter_eq_left.mpr]        apply hE'.trans        simp only [Set.setOf_subset_setOf, superlevelSet]        exact fun a_2 a_3 ↦ Std.lt_of_le_of_lt has a_3    rcases exists_seq_strictMono_tendsto' h_zero with ⟨a, mono_a, ha, a_tendsto⟩    calc _      _ = ⨆ n, ∫⁻ (s : ℝ≥0∞), (Set.Ioo (a n) (rearrangement f t μ))ᶜ.indicator (fun s ↦ min (distribution f s μ) t) s := by        rw [← lintegral_iSup]        rotate_left        · intro n          measurability        · intro n m hmn          simp only          gcongr          exact mono_a.monotone hmn        congr with s        rw [← iSup_apply, Set.iSup_indicator ENNReal.bot_eq_zero monotone_const]        rotate_left        · intro n m hmn          simp only [compl_le_compl_iff_le]          gcongr          exact mono_a.monotone hmn        have : Set.univ = ⋃ n, (Set.Ioo (a n) (rearrangement f t μ))ᶜ := by          ext x          simp only [Set.mem_univ, Set.mem_iUnion, Set.mem_compl_iff, Set.mem_Ioo, not_and, not_lt,            true_iff]          rw [tendsto_order] at a_tendsto          have a_tendsto := a_tendsto.1          contrapose! a_tendsto          use x, (a_tendsto 0).2          apply Filter.Frequently.of_forall          exact fun n ↦ (a_tendsto n).1.le        rw [← this]        simp      _ ≤ _ := by        apply iSup_le        intro n        rw [lintegral_indicator measurableSet_Ioo.compl]        exact this (a n) (ha n).2  · simp only [iSup_le_iff]    intro E measE hμE    rw [setLIntegral_enorm_eq hf measE]    gcongr with s    apply le_min    · unfold distribution      gcongr      exact Set.inter_subset_right    · apply hμE.trans'      gcongr      exact Set.inter_subset_left