feat(measure_theory/integral): weaker assumptions on Ioi integrability (

#11090)

To show a function is integrable given an `ae_cover` it suffices to show boundedness along a filter, not necessarily convergence. This PR adds these generalisations, and uses them to show the older convergence versions.

src/measure_theory/integral/integral_eq_improper.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2021 Anatole Dedecker. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Anatole Dedecker
+Authors: Anatole Dedecker, Bhavik Mehta
 -/
 import measure_theory.integral.interval_integral
 import order.filter.at_top_bot
@@ -280,52 +280,82 @@ section integrable
 variables {α ι E : Type*} [measurable_space α] {μ : measure α} {l : filter ι}
   [normed_group E] [measurable_space E] [opens_measurable_space E]
 
+lemma ae_cover.integrable_of_lintegral_nnnorm_bounded [l.ne_bot] [l.is_countably_generated]
+  {φ : ι → set α} (hφ : ae_cover μ l φ) {f : α → E} (I : ℝ) (hfm : ae_measurable f μ)
+  (hbounded : ∀ᶠ i in l, ∫⁻ x in φ i, ∥f x∥₊ ∂μ ≤ ennreal.of_real I) :
+  integrable f μ :=
+begin
+  refine ⟨hfm, (le_of_tendsto _ hbounded).trans_lt ennreal.of_real_lt_top⟩,
+  exact hφ.lintegral_tendsto_of_countably_generated
+    (measurable_nnnorm.comp_ae_measurable hfm).coe_nnreal_ennreal,
+end
+
 lemma ae_cover.integrable_of_lintegral_nnnorm_tendsto [l.ne_bot] [l.is_countably_generated]
   {φ : ι → set α} (hφ : ae_cover μ l φ) {f : α → E} (I : ℝ)
   (hfm : ae_measurable f μ)
-  (htendsto : tendsto (λ i, ∫⁻ x in φ i, nnnorm (f x) ∂μ) l (𝓝 $ ennreal.of_real I)) :
+  (htendsto : tendsto (λ i, ∫⁻ x in φ i, ∥f x∥₊ ∂μ) l (𝓝 $ ennreal.of_real I)) :
   integrable f μ :=
 begin
-  refine ⟨hfm, _⟩,
-  unfold has_finite_integral,
-  rw hφ.lintegral_eq_of_tendsto _ (measurable_nnnorm.comp_ae_measurable hfm).coe_nnreal_ennreal
-    htendsto,
-  exact ennreal.of_real_lt_top
+  refine hφ.integrable_of_lintegral_nnnorm_bounded (max 1 (I + 1)) hfm _,
+  refine htendsto.eventually (ge_mem_nhds _),
+  refine (ennreal.of_real_lt_of_real_iff (lt_max_of_lt_left zero_lt_one)).2 _,
+  exact lt_max_of_lt_right (lt_add_one I),
 end
 
+lemma ae_cover.integrable_of_lintegral_nnnorm_bounded' [l.ne_bot] [l.is_countably_generated]
+  {φ : ι → set α} (hφ : ae_cover μ l φ) {f : α → E} (I : ℝ≥0) (hfm : ae_measurable f μ)
+  (hbounded : ∀ᶠ i in l, ∫⁻ x in φ i, ∥f x∥₊ ∂μ ≤ I) :
+  integrable f μ :=
+hφ.integrable_of_lintegral_nnnorm_bounded I hfm
+  (by simpa only [ennreal.of_real_coe_nnreal] using hbounded)
+
 lemma ae_cover.integrable_of_lintegral_nnnorm_tendsto' [l.ne_bot] [l.is_countably_generated]
   {φ : ι → set α} (hφ : ae_cover μ l φ) {f : α → E} (I : ℝ≥0)
   (hfm : ae_measurable f μ)
-  (htendsto : tendsto (λ i, ∫⁻ x in φ i, nnnorm (f x) ∂μ) l (𝓝 $ ennreal.of_real I)) :
+  (htendsto : tendsto (λ i, ∫⁻ x in φ i, ∥f x∥₊ ∂μ) l (𝓝 I)) :
   integrable f μ :=
-hφ.integrable_of_lintegral_nnnorm_tendsto I hfm htendsto
+hφ.integrable_of_lintegral_nnnorm_tendsto I hfm
+  (by simpa only [ennreal.of_real_coe_nnreal] using htendsto)
 
-lemma ae_cover.integrable_of_integral_norm_tendsto [l.ne_bot] [l.is_countably_generated]
+lemma ae_cover.integrable_of_integral_norm_bounded [l.ne_bot] [l.is_countably_generated]
   {φ : ι → set α} (hφ : ae_cover μ l φ) {f : α → E}
   (I : ℝ) (hfi : ∀ i, integrable_on f (φ i) μ)
-  (htendsto : tendsto (λ i, ∫ x in φ i, ∥f x∥ ∂μ) l (𝓝 I)) :
+  (hbounded : ∀ᶠ i in l, ∫ x in φ i, ∥f x∥ ∂μ ≤ 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 _ _)
+  refine hφ.integrable_of_lintegral_nnnorm_bounded I hfm _,
+  conv at hbounded in (integral _ _)
   { rw integral_eq_lintegral_of_nonneg_ae (ae_of_all _ (λ x, @norm_nonneg E _ (f x)))
     hfm.norm.restrict },
-  conv at htendsto in (ennreal.of_real _) { dsimp, rw ← coe_nnnorm, rw ennreal.of_real_coe_nnreal },
-  convert ennreal.tendsto_of_real htendsto,
-  ext i : 1,
-  rw ennreal.of_real_to_real _,
-  exact ne_top_of_lt (hfi i).2
+  conv at hbounded in (ennreal.of_real _) { dsimp, rw ← coe_nnnorm, rw ennreal.of_real_coe_nnreal },
+  refine hbounded.mono (λ i hi, _),
+  rw ←ennreal.of_real_to_real (ne_top_of_lt (hfi i).2),
+  apply ennreal.of_real_le_of_real hi,
 end
 
+lemma ae_cover.integrable_of_integral_norm_tendsto [l.ne_bot] [l.is_countably_generated]
+  {φ : ι → set α} (hφ : ae_cover μ l φ) {f : α → E}
+  (I : ℝ) (hfi : ∀ i, integrable_on f (φ i) μ)
+  (htendsto : tendsto (λ i, ∫ x in φ i, ∥f x∥ ∂μ) l (𝓝 I)) :
+  integrable f μ :=
+let ⟨I', hI'⟩ := htendsto.is_bounded_under_le in hφ.integrable_of_integral_norm_bounded I' hfi hI'
+
+lemma ae_cover.integrable_of_integral_bounded_of_nonneg_ae [l.ne_bot] [l.is_countably_generated]
+  {φ : ι → set α} (hφ : ae_cover μ l φ) {f : α → ℝ} (I : ℝ)
+  (hfi : ∀ i, integrable_on f (φ i) μ) (hnng : ∀ᵐ x ∂μ, 0 ≤ f x)
+  (hbounded : ∀ᶠ i in l, ∫ x in φ i, f x ∂μ ≤ I) :
+  integrable f μ :=
+hφ.integrable_of_integral_norm_bounded I hfi $ hbounded.mono $ λ i hi,
+  (integral_congr_ae $ ae_restrict_of_ae $ hnng.mono $ λ x, real.norm_of_nonneg).le.trans hi
+
 lemma ae_cover.integrable_of_integral_tendsto_of_nonneg_ae [l.ne_bot] [l.is_countably_generated]
   {φ : ι → set α} (hφ : ae_cover μ l φ) {f : α → ℝ} (I : ℝ)
   (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 hfi
-  (htendsto.congr $ λ i, integral_congr_ae $ ae_restrict_of_ae $ hnng.mono $
-    λ x hx, (real.norm_of_nonneg hx).symm)
+let ⟨I', hI'⟩ := htendsto.is_bounded_under_le in
+  hφ.integrable_of_integral_bounded_of_nonneg_ae I' hfi hnng hI'
 
 end integrable
 
@@ -374,58 +404,77 @@ variables {α ι E : Type*}
           [measurable_space E] [normed_group E] [borel_space E]
           {a b : ι → α} {f : α → E}
 
-lemma integrable_of_interval_integral_norm_tendsto [no_min_order α] [nonempty α]
+lemma integrable_of_interval_integral_norm_bounded [no_min_order α] [nonempty α]
   (I : ℝ) (hfi : ∀ i, integrable_on f (Ioc (a i) (b i)) μ)
   (ha : tendsto a l at_bot) (hb : tendsto b l at_top)
-  (h : tendsto (λ i, ∫ x in a i .. b i, ∥f x∥ ∂μ) l (𝓝 $ I)) :
+  (h : ∀ᶠ i in l, ∫ x in a i .. b i, ∥f x∥ ∂μ ≤ I) :
   integrable f μ :=
 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 _ hfi (h.congr' _),
+  have hφ : ae_cover μ l _ := ae_cover_Ioc ha hb,
+  refine hφ.integrable_of_integral_norm_bounded I hfi (h.mp _),
   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)
+  intros i hai hbi ht,
+  rwa ←interval_integral.integral_of_le (hai.trans hbi)
 end
 
-lemma integrable_on_Iic_of_interval_integral_norm_tendsto [no_min_order α] (I : ℝ) (b : α)
+lemma integrable_of_interval_integral_norm_tendsto [no_min_order α] [nonempty α]
+  (I : ℝ) (hfi : ∀ i, integrable_on f (Ioc (a i) (b i)) μ)
+  (ha : tendsto a l at_bot) (hb : tendsto b l at_top)
+  (h : tendsto (λ i, ∫ x in a i .. b i, ∥f x∥ ∂μ) l (𝓝 I)) :
+  integrable f μ :=
+let ⟨I', hI'⟩ := h.is_bounded_under_le in
+  integrable_of_interval_integral_norm_bounded I' hfi ha hb hI'
+
+lemma integrable_on_Iic_of_interval_integral_norm_bounded [no_min_order α] (I : ℝ) (b : α)
   (hfi : ∀ i, integrable_on f (Ioc (a i) b) μ) (ha : tendsto a l at_bot)
-  (h : tendsto (λ i, ∫ x in a i .. b, ∥f x∥ ∂μ) l (𝓝 $ I)) :
+  (h : ∀ᶠ i in l, (∫ x in a i .. b, ∥f x∥ ∂μ) ≤ I) :
   integrable_on f (Iic b) μ :=
 begin
-  let φ := λ i, Ioi (a i),
-  have hφ : ae_cover (μ.restrict $ Iic b) l φ := ae_cover_Ioi ha,
-  have hfi : ∀ i, integrable_on f (φ i) (μ.restrict $ Iic b),
+  have hφ : ae_cover (μ.restrict $ Iic b) l _ := ae_cover_Ioi ha,
+  have hfi : ∀ i, integrable_on f (Ioi (a i)) (μ.restrict $ Iic b),
   { intro i,
     rw [integrable_on, measure.restrict_restrict (hφ.measurable i)],
     exact hfi i },
-  refine hφ.integrable_of_integral_norm_tendsto _ hfi (h.congr' _),
+  refine hφ.integrable_of_integral_norm_bounded I hfi (h.mp _),
   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)],
-  refl
+  exact id
 end
 
-lemma integrable_on_Ioi_of_interval_integral_norm_tendsto (I : ℝ) (a : α)
+lemma integrable_on_Iic_of_interval_integral_norm_tendsto [no_min_order α] (I : ℝ) (b : α)
+  (hfi : ∀ i, integrable_on f (Ioc (a i) b) μ) (ha : tendsto a l at_bot)
+  (h : tendsto (λ i, ∫ x in a i .. b, ∥f x∥ ∂μ) l (𝓝 I)) :
+  integrable_on f (Iic b) μ :=
+let ⟨I', hI'⟩ := h.is_bounded_under_le in
+  integrable_on_Iic_of_interval_integral_norm_bounded I' b hfi ha hI'
+
+lemma integrable_on_Ioi_of_interval_integral_norm_bounded (I : ℝ) (a : α)
   (hfi : ∀ i, integrable_on f (Ioc a (b i)) μ) (hb : tendsto b l at_top)
-  (h : tendsto (λ i, ∫ x in a .. b i, ∥f x∥ ∂μ) l (𝓝 $ I)) :
+  (h : ∀ᶠ i in l, (∫ x in a .. b i, ∥f x∥ ∂μ) ≤ I) :
   integrable_on f (Ioi a) μ :=
 begin
-  let φ := λ i, Iic (b i),
-  have hφ : ae_cover (μ.restrict $ Ioi a) l φ := ae_cover_Iic hb,
-  have hfi : ∀ i, integrable_on f (φ i) (μ.restrict $ Ioi a),
+  have hφ : ae_cover (μ.restrict $ Ioi a) l _ := ae_cover_Iic hb,
+  have hfi : ∀ i, integrable_on f (Iic (b i)) (μ.restrict $ Ioi a),
   { intro i,
     rw [integrable_on, measure.restrict_restrict (hφ.measurable i), inter_comm],
     exact hfi i },
-  refine hφ.integrable_of_integral_norm_tendsto _ hfi (h.congr' _),
-  filter_upwards [hb.eventually (eventually_ge_at_top $ a)],
+  refine hφ.integrable_of_integral_norm_bounded I hfi (h.mp _),
+  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),
       inter_comm],
-  refl
+  exact id
 end
 
+lemma integrable_on_Ioi_of_interval_integral_norm_tendsto (I : ℝ) (a : α)
+  (hfi : ∀ i, integrable_on f (Ioc a (b i)) μ) (hb : tendsto b l at_top)
+  (h : tendsto (λ i, ∫ x in a .. b i, ∥f x∥ ∂μ) l (𝓝 $ I)) :
+  integrable_on f (Ioi a) μ :=
+let ⟨I', hI'⟩ := h.is_bounded_under_le in
+  integrable_on_Ioi_of_interval_integral_norm_bounded I' a hfi hb hI'
+
 end integrable_of_interval_integral
 
 section integral_of_interval_integral