feat(probability/martingale/borel_cantelli): Lévy's generalized Borel…

…-Cantelli (#16358)

This PR proves the one sided martingale bound and uses it to prove the Lévy's generalized Borel-Cantelli lemma. With the generalized Borel-Cantelli, the still missing second Borel-Cantelli lemma follows by choosing an appropriate filtration.



Co-authored-by: RemyDegenne <Remydegenne@gmail.com>

src/measure_theory/function/conditional_expectation/real.lean

@@ -50,8 +50,8 @@ begin
       (signed_measure.measurable_rn_deriv _ _).strongly_measurable },
 end
 
-/-- TODO: this should be generalized and proved using Jensen's inequality
-for the conditional expectation (not in mathlib yet) .-/
+-- TODO: the following couple of lemmas should be generalized and proved using Jensen's inequality
+-- for the conditional expectation (not in mathlib yet) .
 lemma snorm_one_condexp_le_snorm (f : α → ℝ) :
   snorm (μ[f | m]) 1 μ ≤ snorm f 1 μ :=
 begin
@@ -90,6 +90,104 @@ begin
   end
 end
 
+lemma integral_abs_condexp_le (f : α → ℝ) :
+  ∫ x, |μ[f | m] x| ∂μ ≤ ∫ x, |f x| ∂μ :=
+begin
+  by_cases hm : m ≤ m0,
+  swap,
+  { simp_rw [condexp_of_not_le hm, pi.zero_apply, abs_zero, integral_zero],
+    exact integral_nonneg (λ x, abs_nonneg _) },
+  by_cases hfint : integrable f μ,
+  swap,
+  { simp only [condexp_undef hfint, pi.zero_apply, abs_zero, integral_const,
+      algebra.id.smul_eq_mul, mul_zero],
+    exact integral_nonneg (λ x, abs_nonneg _) },
+  rw [integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae],
+  { rw ennreal.to_real_le_to_real;
+    simp_rw [← real.norm_eq_abs, of_real_norm_eq_coe_nnnorm],
+    { rw [← snorm_one_eq_lintegral_nnnorm, ← snorm_one_eq_lintegral_nnnorm],
+      exact snorm_one_condexp_le_snorm _ },
+    { exact ne_of_lt integrable_condexp.2 },
+    { exact ne_of_lt hfint.2 } },
+  { exact eventually_of_forall (λ x, abs_nonneg _) },
+  { simp_rw ← real.norm_eq_abs,
+    exact hfint.1.norm },
+  { exact eventually_of_forall (λ x, abs_nonneg _) },
+  { simp_rw ← real.norm_eq_abs,
+    exact (strongly_measurable_condexp.mono hm).ae_strongly_measurable.norm }
+end
+
+lemma set_integral_abs_condexp_le {s : set α} (hs : measurable_set[m] s) (f : α → ℝ) :
+  ∫ x in s, |μ[f | m] x| ∂μ ≤ ∫ x in s, |f x| ∂μ :=
+begin
+  by_cases hnm : m ≤ m0,
+  swap,
+  { simp_rw [condexp_of_not_le hnm, pi.zero_apply, abs_zero, integral_zero],
+    exact integral_nonneg (λ x, abs_nonneg _) },
+  by_cases hfint : integrable f μ,
+  swap,
+  { simp only [condexp_undef hfint, pi.zero_apply, abs_zero, integral_const,
+      algebra.id.smul_eq_mul, mul_zero],
+    exact integral_nonneg (λ x, abs_nonneg _) },
+  have : ∫ x in s, |μ[f | m] x| ∂μ = ∫ x, |μ[s.indicator f | m] x| ∂μ,
+  { rw ← integral_indicator,
+    swap, { exact hnm _ hs },
+    refine integral_congr_ae _,
+    have : (λ x, |μ[s.indicator f | m] x|) =ᵐ[μ] λ x, |s.indicator (μ[f | m]) x| :=
+      eventually_eq.fun_comp (condexp_indicator hfint hs) _,
+    refine eventually_eq.trans (eventually_of_forall $ λ x, _) this.symm,
+    rw [← real.norm_eq_abs, norm_indicator_eq_indicator_norm],
+    refl },
+  rw [this, ← integral_indicator],
+  swap, { exact hnm _ hs },
+  refine (integral_abs_condexp_le _).trans (le_of_eq $ integral_congr_ae $
+    eventually_of_forall $ λ x, _),
+  rw [← real.norm_eq_abs, norm_indicator_eq_indicator_norm],
+  refl,
+end
+
+/-- If the real valued function `f` is bounded almost everywhere by `R`, then so is its conditional
+expectation. -/
+lemma ae_bdd_condexp_of_ae_bdd {R : ℝ≥0} {f : α → ℝ}
+  (hbdd : ∀ᵐ x ∂μ, |f x| ≤ R) :
+  ∀ᵐ x ∂μ, |μ[f | m] x| ≤ R :=
+begin
+  by_cases hnm : m ≤ m0,
+  swap,
+  { simp_rw [condexp_of_not_le hnm, pi.zero_apply, abs_zero],
+    refine eventually_of_forall (λ x, R.coe_nonneg) },
+  by_cases hfint : integrable f μ,
+  swap,
+  { simp_rw [condexp_undef hfint],
+    filter_upwards [hbdd] with x hx,
+    rw [pi.zero_apply, abs_zero],
+    exact (abs_nonneg _).trans hx },
+  by_contra h,
+  change μ _ ≠ 0 at h,
+  simp only [← zero_lt_iff, set.compl_def, set.mem_set_of_eq, not_le] at h,
+  suffices : (μ {x | ↑R < |μ[f | m] x|}).to_real * ↑R < (μ {x | ↑R < |μ[f | m] x|}).to_real * ↑R,
+  { exact this.ne rfl },
+  refine lt_of_lt_of_le (set_integral_gt_gt R.coe_nonneg _ _ h.ne.symm) _,
+  { simp_rw [← real.norm_eq_abs],
+    exact (strongly_measurable_condexp.mono hnm).measurable.norm },
+  { exact integrable_condexp.abs.integrable_on },
+  refine (set_integral_abs_condexp_le _ _).trans _,
+  { simp_rw [← real.norm_eq_abs],
+    exact @measurable_set_lt _ _ _ _ _ m _ _ _ _ _ measurable_const
+      strongly_measurable_condexp.norm.measurable },
+  simp only [← smul_eq_mul, ← set_integral_const, nnreal.val_eq_coe,
+    is_R_or_C.coe_real_eq_id, id.def],
+  refine set_integral_mono_ae hfint.abs.integrable_on _ _,
+  { refine ⟨ae_strongly_measurable_const, lt_of_le_of_lt _
+      (integrable_condexp.integrable_on : integrable_on (μ[f | m]) {x | ↑R < |μ[f | m] x|} μ).2⟩,
+    refine set_lintegral_mono (measurable.nnnorm _).coe_nnreal_ennreal
+      (strongly_measurable_condexp.mono hnm).measurable.nnnorm.coe_nnreal_ennreal (λ x hx, _),
+    { exact measurable_const },
+    { rw [ennreal.coe_le_coe, real.nnnorm_of_nonneg R.coe_nonneg],
+      exact subtype.mk_le_mk.2 (le_of_lt hx) } },
+  { exact hbdd },
+end
+
 /-- Given a integrable function `g`, the conditional expectations of `g` with respect to
 a sequence of sub-σ-algebras is uniformly integrable. -/
 lemma integrable.uniform_integrable_condexp {ι : Type*} [is_finite_measure μ]

src/measure_theory/integral/bochner.lean

@@ -1611,4 +1611,65 @@ lemma ae_le_trim_iff
 
 end integral_trim
 
+section snorm_bound
+
+variables {m0 : measurable_space α} {μ : measure α}
+
+lemma snorm_one_le_of_le {r : ℝ≥0} {f : α → ℝ}
+  (hfint : integrable f μ) (hfint' : 0 ≤ ∫ x, f x ∂μ) (hf : ∀ᵐ ω ∂μ, f ω ≤ r) :
+  snorm f 1 μ ≤ 2 * μ set.univ * r :=
+begin
+  by_cases hr : r = 0,
+  { suffices : f =ᵐ[μ] 0,
+    { rw [snorm_congr_ae this, snorm_zero, hr, ennreal.coe_zero, mul_zero],
+      exact le_rfl },
+    rw [hr, nonneg.coe_zero] at hf,
+    have hnegf : ∫ x, -f x ∂μ = 0,
+    { rw [integral_neg, neg_eq_zero],
+      exact le_antisymm (integral_nonpos_of_ae hf) hfint' },
+    have := (integral_eq_zero_iff_of_nonneg_ae _ hfint.neg).1 hnegf,
+    { filter_upwards [this] with ω hω,
+      rwa [pi.neg_apply, pi.zero_apply, neg_eq_zero] at hω },
+    { filter_upwards [hf] with ω hω,
+      rwa [pi.zero_apply, pi.neg_apply, right.nonneg_neg_iff] } },
+  by_cases hμ : is_finite_measure μ,
+  swap,
+  { have : μ set.univ = ∞,
+    { by_contra hμ',
+      exact hμ (is_finite_measure.mk $ lt_top_iff_ne_top.2 hμ') },
+    rw [this, ennreal.mul_top, if_neg, ennreal.top_mul, if_neg],
+    { exact le_top },
+    { simp [hr] },
+    { norm_num } },
+  haveI := hμ,
+  rw [integral_eq_integral_pos_part_sub_integral_neg_part hfint, sub_nonneg] at hfint',
+  have hposbdd : ∫ ω, max (f ω) 0 ∂μ ≤ (μ set.univ).to_real • r,
+  { rw ← integral_const,
+    refine integral_mono_ae hfint.real_to_nnreal (integrable_const r) _,
+    filter_upwards [hf] with ω hω using real.to_nnreal_le_iff_le_coe.2 hω },
+  rw [mem_ℒp.snorm_eq_integral_rpow_norm one_ne_zero ennreal.one_ne_top
+      (mem_ℒp_one_iff_integrable.2 hfint),
+    ennreal.of_real_le_iff_le_to_real (ennreal.mul_ne_top
+      (ennreal.mul_ne_top ennreal.two_ne_top $ @measure_ne_top _ _ _ hμ _) ennreal.coe_ne_top)],
+  simp_rw [ennreal.one_to_real, _root_.inv_one, real.rpow_one, real.norm_eq_abs,
+    ← max_zero_add_max_neg_zero_eq_abs_self, ← real.coe_to_nnreal'],
+  rw integral_add hfint.real_to_nnreal,
+  { simp only [real.coe_to_nnreal', ennreal.to_real_mul, ennreal.to_real_bit0,
+    ennreal.one_to_real, ennreal.coe_to_real] at hfint' ⊢,
+    refine (add_le_add_left hfint' _).trans _,
+    rwa [← two_mul, mul_assoc, mul_le_mul_left (two_pos : (0 : ℝ) < 2)] },
+  { exact hfint.neg.sup (integrable_zero _ _ μ) }
+end
+
+lemma snorm_one_le_of_le' {r : ℝ} {f : α → ℝ}
+  (hfint : integrable f μ) (hfint' : 0 ≤ ∫ x, f x ∂μ) (hf : ∀ᵐ ω ∂μ, f ω ≤ r) :
+  snorm f 1 μ ≤ 2 * μ set.univ * ennreal.of_real r :=
+begin
+  refine snorm_one_le_of_le hfint hfint' _,
+  simp only [real.coe_to_nnreal', le_max_iff],
+  filter_upwards [hf] with ω hω using or.inl hω,
+end
+
+end snorm_bound
+
 end measure_theory

src/measure_theory/integral/set_integral.lean

@@ -396,6 +396,30 @@ begin
   exact hfi.ae_strongly_measurable.ae_measurable.null_measurable (measurable_set_singleton 0).compl
 end
 
+lemma set_integral_gt_gt {R : ℝ} {f : α → ℝ} (hR : 0 ≤ R) (hfm : measurable f)
+  (hfint : integrable_on f {x | ↑R < f x} μ) (hμ : μ {x | ↑R < f x} ≠ 0):
+  (μ {x | ↑R < f x}).to_real * R < ∫ x in {x | ↑R < f x}, f x ∂μ :=
+begin
+  have : integrable_on (λ x, R) {x | ↑R < f x} μ,
+  { refine ⟨ae_strongly_measurable_const, lt_of_le_of_lt _ hfint.2⟩,
+    refine set_lintegral_mono (measurable.nnnorm _).coe_nnreal_ennreal
+      hfm.nnnorm.coe_nnreal_ennreal (λ x hx, _),
+    { exact measurable_const },
+    { simp only [ennreal.coe_le_coe, real.nnnorm_of_nonneg hR,
+        real.nnnorm_of_nonneg (hR.trans $ le_of_lt hx), subtype.mk_le_mk],
+      exact le_of_lt hx } },
+  rw [← sub_pos, ← smul_eq_mul, ← set_integral_const, ← integral_sub hfint this,
+    set_integral_pos_iff_support_of_nonneg_ae],
+  { rw ← zero_lt_iff at hμ,
+    rwa set.inter_eq_self_of_subset_right,
+    exact λ x hx, ne.symm (ne_of_lt $ sub_pos.2 hx) },
+  { change ∀ᵐ x ∂(μ.restrict _), _,
+    rw ae_restrict_iff,
+    { exact eventually_of_forall (λ x hx, sub_nonneg.2 $ le_of_lt hx) },
+    { exact measurable_set_le measurable_zero (hfm.sub measurable_const) } },
+  { exact integrable.sub hfint this },
+end
+
 lemma set_integral_trim {α} {m m0 : measurable_space α} {μ : measure α} (hm : m ≤ m0) {f : α → E}
   (hf_meas : strongly_measurable[m] f) {s : set α} (hs : measurable_set[m] s) :
   ∫ x in s, f x ∂μ = ∫ x in s, f x ∂(μ.trim hm) :=

src/probability/martingale/basic.lean

@@ -66,6 +66,16 @@ lemma martingale_const (ℱ : filtration ι m0) (μ : measure Ω) [is_finite_mea
   martingale (λ _ _, x) ℱ μ :=
 ⟨adapted_const ℱ _, λ i j hij, by rw condexp_const (ℱ.le _)⟩
 
+lemma martingale_const_fun [order_bot ι]
+  (ℱ : filtration ι m0) (μ : measure Ω) [is_finite_measure μ]
+  {f : Ω → E} (hf : strongly_measurable[ℱ ⊥] f) (hfint : integrable f μ) :
+  martingale (λ _, f) ℱ μ :=
+begin
+  refine ⟨λ i, hf.mono $ ℱ.mono bot_le, λ i j hij, _⟩,
+  rw condexp_of_strongly_measurable (ℱ.le _) (hf.mono $ ℱ.mono bot_le) hfint,
+  apply_instance,
+end
+
 variables (E)
 lemma martingale_zero (ℱ : filtration ι m0) (μ : measure Ω) :
   martingale (0 : ι → Ω → E) ℱ μ :=