feat(measure_theory): add a few integration-related lemmas (#7821)

These are lemmas I proved while working on #7164. Some of them are actually not used anymore in that PR because I'm refactoring it, but I thought they would be useful anyway, so here there are.

Author: ADedecker

src/measure_theory/integration.lean

@@ -903,6 +903,16 @@ begin
   exact h a,
 end
 
+lemma lintegral_mono_set ⦃μ : measure α⦄
+  {s t : set α} {f : α → ℝ≥0∞} (hst : s ⊆ t) :
+  ∫⁻ x in s, f x ∂μ ≤ ∫⁻ x in t, f x ∂μ :=
+lintegral_mono' (measure.restrict_mono hst (le_refl μ)) (le_refl f)
+
+lemma lintegral_mono_set' ⦃μ : measure α⦄
+  {s t : set α} {f : α → ℝ≥0∞} (hst : s ≤ᵐ[μ] t) :
+  ∫⁻ x in s, f x ∂μ ≤ ∫⁻ x in t, f x ∂μ :=
+lintegral_mono' (measure.restrict_mono' hst (le_refl μ)) (le_refl f)
+
 lemma monotone_lintegral (μ : measure α) : monotone (lintegral μ) :=
 lintegral_mono
 

src/measure_theory/measure_space.lean

@@ -974,6 +974,10 @@ by { rw [restrict, restrictₗ], convert le_lift_linear_apply _ t, simp }
   (μ.restrict t).restrict s = μ.restrict (s ∩ t) :=
 ext $ λ u hu, by simp [*, set.inter_assoc]
 
+lemma restrict_comm (hs : measurable_set s) (ht : measurable_set t) :
+  (μ.restrict t).restrict s = (μ.restrict s).restrict t :=
+by rw [restrict_restrict hs, restrict_restrict ht, inter_comm]
+
 lemma restrict_apply_eq_zero (ht : measurable_set t) : μ.restrict s t = 0 ↔ μ (t ∩ s) = 0 :=
 by rw [restrict_apply ht]
 
@@ -1070,14 +1074,19 @@ by rw [restrictₗ_apply, restrict_apply ht, linear_map.comp_apply,
     (measurable_subtype_coe ht), subtype.image_preimage_coe]
 
 /-- Restriction of a measure to a subset is monotone both in set and in measure. -/
-@[mono] lemma restrict_mono ⦃s s' : set α⦄ (hs : s ⊆ s') ⦃μ ν : measure α⦄ (hμν : μ ≤ ν) :
+lemma restrict_mono' ⦃s s' : set α⦄ ⦃μ ν : measure α⦄ (hs : s ≤ᵐ[μ] s') (hμν : μ ≤ ν) :
   μ.restrict s ≤ ν.restrict s' :=
 assume t ht,
 calc μ.restrict s t = μ (t ∩ s) : restrict_apply ht
-... ≤ μ (t ∩ s') : measure_mono $ inter_subset_inter_right _ hs
+... ≤ μ (t ∩ s') : measure_mono_ae $ hs.mono $ λ x hx ⟨hxt, hxs⟩, ⟨hxt, hx hxs⟩
 ... ≤ ν (t ∩ s') : le_iff'.1 hμν (t ∩ s')
 ... = ν.restrict s' t : (restrict_apply ht).symm
 
+/-- Restriction of a measure to a subset is monotone both in set and in measure. -/
+@[mono] lemma restrict_mono ⦃s s' : set α⦄ (hs : s ⊆ s') ⦃μ ν : measure α⦄ (hμν : μ ≤ ν) :
+  μ.restrict s ≤ ν.restrict s' :=
+restrict_mono' (ae_of_all _ hs) hμν
+
 lemma restrict_le_self : μ.restrict s ≤ μ :=
 assume t ht,
 calc μ.restrict s t = μ (t ∩ s) : restrict_apply ht

src/measure_theory/set_integral.lean

@@ -179,6 +179,10 @@ h.mono_measure $ measure.restrict_le_self
 lemma integrable.integrable_on' (h : integrable f (μ.restrict s)) : integrable_on f s μ :=
 h
 
+lemma integrable_on.restrict (h : integrable_on f s μ) (hs : measurable_set s) :
+  integrable_on f s (μ.restrict t) :=
+by { rw [integrable_on, measure.restrict_restrict hs], exact h.mono_set (inter_subset_left _ _) }
+
 lemma integrable_on.left_of_union (h : integrable_on f (s ∪ t) μ) : integrable_on f s μ :=
 h.mono_set $ subset_union_left _ _
 
@@ -537,6 +541,18 @@ set_integral_nonneg_of_ae_restrict ((ae_restrict_iff' hs).mpr (ae_of_all μ hf))
 
 end nonneg
 
+lemma set_integral_mono_set {α : Type*} [measurable_space α] {μ : measure α}
+  {s t : set α} {f : α → ℝ} (hfi : integrable f μ) (hf : 0 ≤ᵐ[μ] f) (hst : s ≤ᵐ[μ] t) :
+  ∫ x in s, f x ∂μ ≤ ∫ x in t, f x ∂μ :=
+begin
+  repeat { rw integral_eq_lintegral_of_nonneg_ae (ae_restrict_of_ae hf)
+            (hfi.1.mono_measure measure.restrict_le_self) },
+  rw ennreal.to_real_le_to_real
+    (ne_of_lt $ (has_finite_integral_iff_of_real (ae_restrict_of_ae hf)).mp hfi.integrable_on.2)
+    (ne_of_lt $ (has_finite_integral_iff_of_real (ae_restrict_of_ae hf)).mp hfi.integrable_on.2),
+  exact (lintegral_mono_set' hst),
+end
+
 end measure_theory
 
 open measure_theory asymptotics metric