feat(measure_theory/[integrable_on, set_integral]): integrals on two …

…ae-eq sets are equal (#8440)

src/measure_theory/integrable_on.lean

@@ -107,6 +107,10 @@ lemma integrable_on.mono_set_ae (h : integrable_on f t μ) (hst : s ≤ᵐ[μ] t
   integrable_on f s μ :=
 h.integrable.mono_measure $ restrict_mono_ae hst
 
+lemma integrable_on.congr_set_ae (h : integrable_on f t μ) (hst : s =ᵐ[μ] t) :
+  integrable_on f s μ :=
+h.mono_set_ae hst.le
+
 lemma integrable.integrable_on (h : integrable f μ) : integrable_on f s μ :=
 h.mono_measure $ measure.restrict_le_self
 

src/measure_theory/measure_space.lean

@@ -2552,7 +2552,7 @@ lemma metric.bounded.finite_measure [metric_space α] [proper_space α]
 
 section piecewise
 
-variables [measurable_space α] {μ : measure α} {s : set α} {f g : α → β}
+variables [measurable_space α] {μ : measure α} {s t : set α} {f g : α → β}
 
 lemma piecewise_ae_eq_restrict (hs : measurable_set s) : piecewise s f g =ᵐ[μ.restrict s] f :=
 begin
@@ -2567,11 +2567,19 @@ begin
   exact (piecewise_eq_on_compl s f g).eventually_eq.filter_mono inf_le_right
 end
 
+lemma piecewise_ae_eq_of_ae_eq_set (hst : s =ᵐ[μ] t) : s.piecewise f g =ᵐ[μ] t.piecewise f g :=
+begin
+  filter_upwards [hst],
+  intros x hx,
+  replace hx : x ∈ s ↔ x ∈ t := iff_of_eq hx,
+  by_cases h : x ∈ s; have h' := h; rw hx at h'; simp [h, h']
+end
+
 end piecewise
 
 section indicator_function
 
-variables [measurable_space α] {μ : measure α} {s : set α} {f : α → β}
+variables [measurable_space α] {μ : measure α} {s t : set α} {f : α → β}
 
 lemma ae_measurable.restrict [measurable_space β] (hfm : ae_measurable f μ) {s} :
   ae_measurable f (μ.restrict s) :=
@@ -2585,6 +2593,9 @@ piecewise_ae_eq_restrict hs
 lemma indicator_ae_eq_restrict_compl (hs : measurable_set s) : indicator s f =ᵐ[μ.restrict sᶜ] 0 :=
 piecewise_ae_eq_restrict_compl hs
 
+lemma indicator_ae_eq_of_ae_eq_set (hst : s =ᵐ[μ] t) : s.indicator f =ᵐ[μ] t.indicator f :=
+piecewise_ae_eq_of_ae_eq_set hst
+
 variables [measurable_space β]
 
 lemma ae_measurable_indicator_iff {s} (hs : measurable_set s) :

src/measure_theory/set_integral.lean

@@ -65,7 +65,6 @@ variables [normed_group E] [measurable_space E] {f g : α → E} {s t : set α}
 
 variables [complete_space E] [normed_space ℝ E]
 
-
 lemma set_integral_congr_ae (hs : measurable_set s) (h : ∀ᵐ x ∂μ, x ∈ s → f x = g x) :
   ∫ x in s, f x ∂μ = ∫ x in s, g x ∂μ :=
 integral_congr_ae ((ae_restrict_iff' hs).2 h)
@@ -108,6 +107,10 @@ begin
   ... = ∫ x in s, f x ∂μ : by simp
 end
 
+lemma set_integral_congr_set_ae (hst : s =ᵐ[μ] t) :
+  ∫ x in s, f x ∂μ = ∫ x in t, f x ∂μ :=
+by rw restrict_congr_set hst
+
 lemma set_integral_const (c : E) : ∫ x in s, c ∂μ = (μ s).to_real • c :=
 by rw [integral_const, measure.restrict_apply_univ]