MeasureTheory.Antitone.lintegral_withDensity_le

lemma Antitone.lintegral_withDensity_le {f d : ℝ≥0∞ → ℝ≥0∞} (hf : Antitone f)  (hf' : AEMeasurable f) (hd : d ≤ 1) (hd' : AEMeasurable d) :    ∫⁻ t, f t ∂volume.withDensity d ≤ ∫⁻ t in Set.Iio (∫⁻ t, d t), f t := by  set T := ∫⁻ t, d t with T_def  by_cases d_int : T = ⊤  · rw [d_int, lintegral_withDensity_eq_lintegral_mul₀' hd' (by fun_prop)]    simp only [Pi.mul_apply]    calc _      _ = ∫⁻ t in Set.univ, d t * f t := by simp      _ = (∫⁻ t in Set.Iio ⊤, d t * f t) + ∫⁻ t in {⊤}, d t * f t := by        rw [← lintegral_union (measurableSet_singleton _) (by simp)]        simp      _ ≤ ∫⁻ (t : ℝ≥0∞) in Set.Iio ⊤, f t := by        simp only [Measure.restrict_singleton, measure_singleton, zero_smul, lintegral_zero_measure,          add_zero]        apply setLIntegral_mono' measurableSet_Iio        intro x _        nth_rw 2 [← one_mul (f x)]        gcongr        exact hd x  have d_int' : ∫⁻ (s : ℝ≥0∞) in Set.Iio T, d s ≠ ⊤ := by    rw [← ne_eq] at d_int    rw [← lt_top_iff_ne_top] at *    apply d_int.trans_le'    nth_rw 2 [T_def]    apply setLIntegral_le_lintegral  by_cases f_int : ∫⁻ (s : ℝ≥0∞) in Set.Iio T, f s = ⊤  · rw [f_int]    simp  have f_int' : ∫⁻ (s : ℝ≥0∞) in Set.Iio T, (1 - d s) * f s ≠ ⊤ := by    rw [← ne_eq] at f_int    rw [← lt_top_iff_ne_top] at *    apply f_int.trans_le'    apply setLIntegral_mono' measurableSet_Iio    intro x hx    nth_rw 2 [← one_mul (f x)]    gcongr    simp  calc _    _ = ∫⁻ t in Set.Iio T, f t ∂volume.withDensity d + ∫⁻ t in Set.Ici T, f t ∂volume.withDensity d := by      rw [← lintegral_union measurableSet_Ici (Set.Iio_disjoint_Ici le_rfl)]      simp    _ = ((∫⁻ t in Set.Iio T, f t) - ∫⁻ t in Set.Iio T, (1 - d t) * f t)        + ∫⁻ t in Set.Ici T, f t ∂volume.withDensity d := by      congr 1      rw [setLIntegral_withDensity_eq_lintegral_mul₀' hd' (by fun_prop) measurableSet_Iio]      simp only [Pi.mul_apply]      calc _        _ = ∫⁻ t in Set.Iio T, (1 - (1 - d t)) * f t := by          congr with s          congr          symm          apply ENNReal.sub_sub_cancel ENNReal.one_ne_top (hd s)        _ = (∫⁻ t in Set.Iio T, f t) - ∫⁻ t in Set.Iio T, (1 - d t) * f t := by          rw [← lintegral_sub' (by fun_prop) f_int']          · apply setLIntegral_congr_fun_ae measurableSet_Iio            have : ∀ᵐ (s : ℝ≥0∞), s ≠ 0 := Measure.ae_ne volume 0            filter_upwards [this] with t t_ne_zero ht            rw [ENNReal.sub_mul, one_mul]            intros            contrapose! f_int            rw [eq_top_iff]            calc ⊤              _ = ∫⁻ (s : ℝ≥0∞) in Set.Iio t, ⊤ := by                simp only [lintegral_const, MeasurableSet.univ, Measure.restrict_apply,                  Set.univ_inter]                rw [ENNReal.volume_Iio, ENNReal.top_mul t_ne_zero]              _ = ∫⁻ (s : ℝ≥0∞) in Set.Iio t, f s := by                apply setLIntegral_congr_fun measurableSet_Iio                intro s hs                simp only                symm                rw [eq_top_iff, ← f_int]                apply hf hs.le              _ ≤ ∫⁻ (s : ℝ≥0∞) in Set.Iio T, f s := by                gcongr                exact ht.le          · filter_upwards []            intro s            nth_rw 2 [← one_mul (f s)]            apply mul_le_mul_left            simp    _ ≤ (∫⁻ t in Set.Iio T, f t)        + ((∫⁻ t in Set.Ici T, f t ∂volume.withDensity d)            - ∫⁻ t in Set.Iio T, (1 - d t) * f t) := by      rw [ENNReal.sub_add_eq_add_sub _ f_int']      · apply add_tsub_le_assoc      · apply setLIntegral_mono' measurableSet_Iio        intro x hx        nth_rw 2 [← one_mul (f x)]        gcongr        simp    _ ≤ (∫⁻ t in Set.Iio T, f t)        + ((∫⁻ t in Set.Ici T, f T ∂volume.withDensity d)            - ∫⁻ t in Set.Iio T, (1 - d t) * f T) := by      gcongr 2      · apply setLIntegral_mono' measurableSet_Ici        intro s hs        exact hf hs      · apply setLIntegral_mono' measurableSet_Iio        intro s hs        gcongr        exact hf hs.le    _ = (∫⁻ t in Set.Iio T, f t)        + ((∫⁻ t in Set.Ici T, 1 ∂volume.withDensity d) * f T            - ((∫⁻ t in Set.Iio T, 1) - ∫⁻ t in Set.Iio T, d t) * f T) := by      congr 2      · rw [← lintegral_mul_const'' _ (by fun_prop), one_mul]      · rw [lintegral_mul_const'' _ (by fun_prop), lintegral_sub' (by fun_prop) d_int']        filter_upwards []        exact hd    _ = (∫⁻ t in Set.Iio T, f t)        + ((∫⁻ t in Set.Ici T, d t) * f T            - (∫⁻ t in Set.Ici T, d t) * f T) := by      congr 2      · rw [setLIntegral_withDensity_eq_lintegral_mul₀' hd' (by fun_prop) measurableSet_Ici]        simp      · congr        rw [lintegral_const, one_mul, Measure.restrict_apply MeasurableSet.univ, Set.univ_inter,            ENNReal.volume_Iio]        nth_rw 1 [T_def]        have : ∫⁻ t, d t = (∫⁻ t in Set.Iio T, d t) + ∫⁻ t in Set.Ici T, d t := by          rw [← lintegral_union measurableSet_Ici] <;> simp        rw [this, ENNReal.add_sub_cancel_left d_int']    _ = ∫⁻ t in Set.Iio T, f t := by      simp