feat(measure_theory/integral/integral_eq_improper): weaken measurabil…

…ity assumptions (#10387)

As suggested by @fpvandoorn, this removes a.e. measurability assumptions which could be deduced from integrability assumptions. More of them could be removed assuming the codomain is a `borel_space` and not only an `open_measurable_space`, but I’m not sure wether or not it would be a good idea.

src/measure_theory/integral/integrable_on.lean

@@ -104,7 +104,7 @@ h.mono (subset.refl _) hμ
 
 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
+h.integrable.mono_measure $ measure.restrict_mono_ae hst
 
 lemma integrable_on.congr_set_ae (h : integrable_on f t μ) (hst : s =ᵐ[μ] t) :
   integrable_on f s μ :=

src/measure_theory/integral/integral_eq_improper.lean

@@ -171,11 +171,22 @@ ae_cover_restrict_of_ae_imp hs
   (λ i, (hφ.measurable i).inter hs)
 
 lemma ae_cover.ae_tendsto_indicator {β : Type*} [has_zero β] [topological_space β]
-  {f : α → β} {φ : ι → set α} (hφ : ae_cover μ l φ) :
+  (f : α → β) {φ : ι → set α} (hφ : ae_cover μ l φ) :
   ∀ᵐ x ∂μ, tendsto (λ i, (φ i).indicator f x) l (𝓝 $ f x) :=
 hφ.ae_eventually_mem.mono (λ x hx, tendsto_const_nhds.congr' $
   hx.mono $ λ n hn, (indicator_of_mem hn _).symm)
 
+lemma ae_cover.ae_measurable {β : Type*} [measurable_space β] [l.is_countably_generated] [l.ne_bot]
+  {f : α → β} {φ : ι → set α} (hφ : ae_cover μ l φ)
+  (hfm : ∀ i, ae_measurable f (μ.restrict $ φ i)) : ae_measurable f μ :=
+begin
+  obtain ⟨u, hu⟩ := l.exists_seq_tendsto,
+  have := ae_measurable_Union_iff.mpr (λ (n : ℕ), hfm (u n)),
+  rwa measure.restrict_eq_self_of_ae_mem at this,
+  filter_upwards [hφ.ae_eventually_mem]
+    (λ x hx, let ⟨i, hi⟩ := (hu.eventually hx).exists in mem_Union.mpr ⟨i, hi⟩)
+end
+
 end ae_cover
 
 lemma ae_cover.comp_tendsto {α ι ι' : Type*} [measurable_space α] {μ : measure α} {l : filter ι}
@@ -222,7 +233,7 @@ let F := λ n, (φ n).indicator f in
 have key₁ : ∀ n, ae_measurable (F n) μ, from λ n, hfm.indicator (hφ.measurable n),
 have key₂ : ∀ᵐ (x : α) ∂μ, monotone (λ n, F n x), from ae_of_all _
   (λ x i j hij, indicator_le_indicator_of_subset (hmono hij) (λ x, zero_le $ f x) x),
-have key₃ : ∀ᵐ (x : α) ∂μ, tendsto (λ n, F n x) at_top (𝓝 (f x)), from hφ.ae_tendsto_indicator,
+have key₃ : ∀ᵐ (x : α) ∂μ, tendsto (λ n, F n x) at_top (𝓝 (f x)), from hφ.ae_tendsto_indicator f,
 (lintegral_tendsto_of_tendsto_of_monotone key₁ key₂ key₃).congr
   (λ n, lintegral_indicator f (hφ.measurable n))
 
@@ -291,10 +302,11 @@ hφ.integrable_of_lintegral_nnnorm_tendsto I hfm htendsto
 
 lemma ae_cover.integrable_of_integral_norm_tendsto [l.ne_bot] [l.is_countably_generated]
   {φ : ι → set α} (hφ : ae_cover μ l φ) {f : α → E}
-  (I : ℝ) (hfm : ae_measurable f μ) (hfi : ∀ i, integrable_on f (φ i) μ)
+  (I : ℝ) (hfi : ∀ i, integrable_on f (φ i) μ)
   (htendsto : tendsto (λ i, ∫ x in φ i, ∥f x∥ ∂μ) l (𝓝 I)) :
   integrable f μ :=
 begin
+  have hfm : ae_measurable f μ := hφ.ae_measurable (λ i, (hfi i).ae_measurable),
   refine hφ.integrable_of_lintegral_nnnorm_tendsto I hfm _,
   conv at htendsto in (integral _ _)
   { rw integral_eq_lintegral_of_nonneg_ae (ae_of_all _ (λ x, @norm_nonneg E _ (f x)))
@@ -308,10 +320,10 @@ end
 
 lemma ae_cover.integrable_of_integral_tendsto_of_nonneg_ae [l.ne_bot] [l.is_countably_generated]
   {φ : ι → set α} (hφ : ae_cover μ l φ) {f : α → ℝ} (I : ℝ)
-  (hfm : ae_measurable f μ) (hfi : ∀ i, integrable_on f (φ i) μ) (hnng : ∀ᵐ x ∂μ, 0 ≤ f x)
+  (hfi : ∀ i, integrable_on f (φ i) μ) (hnng : ∀ᵐ x ∂μ, 0 ≤ f x)
   (htendsto : tendsto (λ i, ∫ x in φ i, f x ∂μ) l (𝓝 I)) :
   integrable f μ :=
-hφ.integrable_of_integral_norm_tendsto I hfm hfi
+hφ.integrable_of_integral_norm_tendsto I hfi
   (htendsto.congr $ λ i, integral_congr_ae $ ae_restrict_of_ae $ hnng.mono $
     λ x hx, (real.norm_of_nonneg hx).symm)
 
@@ -331,7 +343,7 @@ by { convert h, ext n, rw integral_indicator (hφ.measurable n) },
 tendsto_integral_filter_of_dominated_convergence (λ x, ∥f x∥)
   (eventually_of_forall $ λ i, hfi.ae_measurable.indicator $ hφ.measurable i)
   (eventually_of_forall $ λ i, ae_of_all _ $ λ x, norm_indicator_le_norm_self _ _)
-  hfi.norm hφ.ae_tendsto_indicator
+  hfi.norm (hφ.ae_tendsto_indicator f)
 
 /-- Slight reformulation of
     `measure_theory.ae_cover.integral_tendsto_of_countably_generated`. -/
@@ -344,11 +356,11 @@ tendsto_nhds_unique (hφ.integral_tendsto_of_countably_generated hfi) h
 
 lemma ae_cover.integral_eq_of_tendsto_of_nonneg_ae [l.ne_bot] [l.is_countably_generated]
   {φ : ι → set α} (hφ : ae_cover μ l φ) {f : α → ℝ} (I : ℝ)
-  (hnng : 0 ≤ᵐ[μ] f) (hfm : ae_measurable f μ) (hfi : ∀ n, integrable_on f (φ n) μ)
+  (hnng : 0 ≤ᵐ[μ] f) (hfi : ∀ n, integrable_on f (φ n) μ)
   (htendsto : tendsto (λ n, ∫ x in φ n, f x ∂μ) l (𝓝 I)) :
   ∫ x, f x ∂μ = I :=
 have hfi' : integrable f μ,
-  from hφ.integrable_of_integral_tendsto_of_nonneg_ae I hfm hfi hnng htendsto,
+  from hφ.integrable_of_integral_tendsto_of_nonneg_ae I hfi hnng htendsto,
 hφ.integral_eq_of_tendsto I hfi' htendsto
 
 end integral
@@ -360,9 +372,7 @@ variables {α ι E : Type*}
           [measurable_space α] [opens_measurable_space α] {μ : measure α}
           {l : filter ι} [filter.ne_bot l] [is_countably_generated l]
           [measurable_space E] [normed_group E] [borel_space E]
-          {a b : ι → α} {f : α → E} (hfm : ae_measurable f μ)
-
-include hfm
+          {a b : ι → α} {f : α → E}
 
 lemma integrable_of_interval_integral_norm_tendsto [no_bot_order α] [nonempty α]
   (I : ℝ) (hfi : ∀ i, integrable_on f (Ioc (a i) (b i)) μ)
@@ -373,7 +383,7 @@ begin
   let φ := λ n, Ioc (a n) (b n),
   let c : α := classical.choice ‹_›,
   have hφ : ae_cover μ l φ := ae_cover_Ioc ha hb,
-  refine hφ.integrable_of_integral_norm_tendsto _ hfm hfi (h.congr' _),
+  refine hφ.integrable_of_integral_norm_tendsto _ hfi (h.congr' _),
   filter_upwards [ha.eventually (eventually_le_at_bot c), hb.eventually (eventually_ge_at_top c)],
   intros i hai hbi,
   exact interval_integral.integral_of_le (hai.trans hbi)
@@ -390,7 +400,7 @@ begin
   { intro i,
     rw [integrable_on, measure.restrict_restrict (hφ.measurable i)],
     exact hfi i },
-  refine hφ.integrable_of_integral_norm_tendsto _ hfm.restrict hfi (h.congr' _),
+  refine hφ.integrable_of_integral_norm_tendsto _ hfi (h.congr' _),
   filter_upwards [ha.eventually (eventually_le_at_bot b)],
   intros i hai,
   rw [interval_integral.integral_of_le hai, measure.restrict_restrict (hφ.measurable i)],
@@ -408,7 +418,7 @@ begin
   { intro i,
     rw [integrable_on, measure.restrict_restrict (hφ.measurable i), inter_comm],
     exact hfi i },
-  refine hφ.integrable_of_integral_norm_tendsto _ hfm.restrict hfi (h.congr' _),
+  refine hφ.integrable_of_integral_norm_tendsto _ hfi (h.congr' _),
   filter_upwards [hb.eventually (eventually_ge_at_top $ a)],
   intros i hbi,
   rw [interval_integral.integral_of_le hbi, measure.restrict_restrict (hφ.measurable i),

src/measure_theory/integral/interval_integral.lean

@@ -617,7 +617,7 @@ begin
   simp_rw [integral_smul_measure, interval_integral, A.set_integral_map,
           ennreal.to_real_of_real (abs_nonneg c)],
   cases hc.lt_or_lt,
-  { simp [h, mul_div_cancel, hc, abs_of_neg, restrict_congr_set Ico_ae_eq_Ioc] },
+  { simp [h, mul_div_cancel, hc, abs_of_neg, measure.restrict_congr_set Ico_ae_eq_Ioc] },
   { simp [h, mul_div_cancel, hc, abs_of_pos] }
 end
 

src/measure_theory/integral/lebesgue.lean

@@ -1126,7 +1126,7 @@ by simp only [h]
 
 lemma set_lintegral_congr {f : α → ℝ≥0∞} {s t : set α} (h : s =ᵐ[μ] t) :
   ∫⁻ x in s, f x ∂μ = ∫⁻ x in t, f x ∂μ :=
-by rw [restrict_congr_set h]
+by rw [measure.restrict_congr_set h]
 
 lemma set_lintegral_congr_fun {f g : α → ℝ≥0∞} {s : set α} (hs : measurable_set s)
   (hfg : ∀ᵐ x ∂μ, x ∈ s → f x = g x) :

src/measure_theory/integral/set_integral.lean

@@ -70,7 +70,7 @@ set_integral_congr_ae hs $ eventually_of_forall h
 
 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
+by rw measure.restrict_congr_set hst
 
 lemma integral_union (hst : disjoint s t) (hs : measurable_set s) (ht : measurable_set t)
   (hfs : integrable_on f s μ) (hft : integrable_on f t μ) :

src/measure_theory/measure/measure_space.lean

@@ -969,6 +969,18 @@ assume t ht,
 calc μ.restrict s t = μ (t ∩ s) : restrict_apply ht
 ... ≤ μ t : measure_mono $ inter_subset_left t s
 
+lemma restrict_mono_ae (h : s ≤ᵐ[μ] t) : μ.restrict s ≤ μ.restrict t :=
+restrict_mono' h (le_refl μ)
+
+lemma restrict_congr_set (h : s =ᵐ[μ] t) : μ.restrict s = μ.restrict t :=
+le_antisymm (restrict_mono_ae h.le) (restrict_mono_ae h.symm.le)
+
+lemma restrict_eq_self_of_ae_mem {m0 : measurable_space α} ⦃s : set α⦄ ⦃μ : measure α⦄
+  (hs : ∀ᵐ x ∂μ, x ∈ s) :
+  μ.restrict s = μ :=
+calc μ.restrict s = μ.restrict univ : restrict_congr_set (eventually_eq_univ.mpr hs)
+... = μ : restrict_univ
+
 lemma restrict_congr_meas (hs : measurable_set s) :
   μ.restrict s = ν.restrict s ↔ ∀ t ⊆ s, measurable_set t → μ t = ν t :=
 ⟨λ H t hts ht,
@@ -1656,16 +1668,6 @@ by simp [filter.eventually_eq]
 
 end dirac
 
-lemma restrict_mono_ae (h : s ≤ᵐ[μ] t) : μ.restrict s ≤ μ.restrict t :=
-begin
-  intros u hu,
-  simp only [restrict_apply hu],
-  exact measure_mono_ae (h.mono $ λ x hx, and.imp id hx)
-end
-
-lemma restrict_congr_set (H : s =ᵐ[μ] t) : μ.restrict s = μ.restrict t :=
-le_antisymm (restrict_mono_ae H.le) (restrict_mono_ae H.symm.le)
-
 section is_finite_measure
 
 include m0