feat: strong law of large numbers for vector-valued random variables (#7218)

We already have the strong law of large numbers for real-valued integrable random variables. We generalize it to general vector-valued integrable random variables. This does not require any second-countability assumptions as integrable functions can by definition be approximated by simple functions, for which the result is deduced from the one-dimensional one.

Along the way, we extend a few lemmas in the library from the real case to the vector case, and remove unneeded second-countability assumptions.

Author: sgouezel

Mathlib/MeasureTheory/Function/SimpleFunc.lean

@@ -1318,6 +1318,56 @@ protected theorem induction {α γ} [MeasurableSpace α] [AddMonoid γ] {P : Sim
     · simp [piecewise_eq_of_not_mem _ _ _ hy, -piecewise_eq_indicator]
 #align measure_theory.simple_func.induction MeasureTheory.SimpleFunc.induction
 
+/-- In a topological vector space, the addition of a measurable function and a simple function is
+measurable. -/
+theorem _root_.Measurable.add_simpleFunc
+    {E : Type*} {_ : MeasurableSpace α} [MeasurableSpace E] [AddGroup E] [MeasurableAdd E]
+    {g : α → E} (hg : Measurable g) (f : SimpleFunc α E) :
+    Measurable (g + (f : α → E)) := by
+  classical
+  induction' f using SimpleFunc.induction with c s hs f f' hff' hf hf'
+  · simp only [SimpleFunc.const_zero, SimpleFunc.coe_piecewise, SimpleFunc.coe_const,
+      SimpleFunc.coe_zero]
+    change Measurable (g + s.piecewise (Function.const α c) (0 : α → E))
+    rw [← piecewise_same s g, ← piecewise_add]
+    exact Measurable.piecewise hs (hg.add_const _) (hg.add_const _)
+  · have : (g + ↑(f + f'))
+        = (Function.support f).piecewise (g + (f : α → E)) (g + f') := by
+      ext x
+      by_cases hx : x ∈ Function.support f
+      · simpa only [SimpleFunc.coe_add, Pi.add_apply, Function.mem_support, ne_eq, not_not,
+          Set.piecewise_eq_of_mem _ _ _ hx, _root_.add_right_inj, add_right_eq_self]
+          using Set.disjoint_left.1 hff' hx
+      · simpa only [SimpleFunc.coe_add, Pi.add_apply, Function.mem_support, ne_eq, not_not,
+          Set.piecewise_eq_of_not_mem _ _ _ hx, _root_.add_right_inj, add_left_eq_self] using hx
+    rw [this]
+    exact Measurable.piecewise f.measurableSet_support hf hf'
+
+/-- In a topological vector space, the addition of a simple function and a measurable function is
+measurable. -/
+theorem _root_.Measurable.simpleFunc_add
+    {E : Type*} {_ : MeasurableSpace α} [MeasurableSpace E] [AddGroup E] [MeasurableAdd E]
+    {g : α → E} (hg : Measurable g) (f : SimpleFunc α E) :
+    Measurable ((f : α → E) + g) := by
+  classical
+  induction' f using SimpleFunc.induction with c s hs f f' hff' hf hf'
+  · simp only [SimpleFunc.const_zero, SimpleFunc.coe_piecewise, SimpleFunc.coe_const,
+      SimpleFunc.coe_zero]
+    change Measurable (s.piecewise (Function.const α c) (0 : α → E) + g)
+    rw [← piecewise_same s g, ← piecewise_add]
+    exact Measurable.piecewise hs (hg.const_add _) (hg.const_add _)
+  · have : (↑(f + f') + g)
+        = (Function.support f).piecewise ((f : α → E) + g) (f' + g) := by
+      ext x
+      by_cases hx : x ∈ Function.support f
+      · simpa only [coe_add, Pi.add_apply, Function.mem_support, ne_eq, not_not,
+          Set.piecewise_eq_of_mem _ _ _ hx, _root_.add_left_inj, add_right_eq_self]
+          using Set.disjoint_left.1 hff' hx
+      · simpa only [SimpleFunc.coe_add, Pi.add_apply, Function.mem_support, ne_eq, not_not,
+          Set.piecewise_eq_of_not_mem _ _ _ hx, _root_.add_left_inj, add_left_eq_self] using hx
+    rw [this]
+    exact Measurable.piecewise f.measurableSet_support hf hf'
+
 end SimpleFunc
 
 end MeasureTheory

Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

@@ -467,6 +467,45 @@ protected theorem smul_const {𝕜} [TopologicalSpace 𝕜] [SMul 𝕜 β] [Cont
 #align measure_theory.strongly_measurable.smul_const MeasureTheory.StronglyMeasurable.smul_const
 #align measure_theory.strongly_measurable.vadd_const MeasureTheory.StronglyMeasurable.vadd_const
 
+/-- In a normed vector space, the addition of a measurable function and a strongly measurable
+function is measurable. Note that this is not true without further second-countability assumptions
+for the addition of two measurable functions. -/
+theorem _root_.Measurable.add_stronglyMeasurable
+    {α E : Type*} {_ : MeasurableSpace α} [AddGroup E] [TopologicalSpace E]
+    [MeasurableSpace E] [BorelSpace E] [ContinuousAdd E] [PseudoMetrizableSpace E]
+    {g f : α → E} (hg : Measurable g) (hf : StronglyMeasurable f) :
+    Measurable (g + f) := by
+  rcases hf with ⟨φ, hφ⟩
+  have : Tendsto (fun n x ↦ g x + φ n x) atTop (𝓝 (g + f)) :=
+    tendsto_pi_nhds.2 (fun x ↦ tendsto_const_nhds.add (hφ x))
+  apply measurable_of_tendsto_metrizable (fun n ↦ ?_) this
+  exact hg.add_simpleFunc _
+
+/-- In a normed vector space, the subtraction of a measurable function and a strongly measurable
+function is measurable. Note that this is not true without further second-countability assumptions
+for the subtraction of two measurable functions. -/
+theorem _root_.Measurable.sub_stronglyMeasurable
+    {α E : Type*} {_ : MeasurableSpace α} [AddCommGroup E] [TopologicalSpace E]
+    [MeasurableSpace E] [BorelSpace E] [ContinuousAdd E] [ContinuousNeg E] [PseudoMetrizableSpace E]
+    {g f : α → E} (hg : Measurable g) (hf : StronglyMeasurable f) :
+    Measurable (g - f) := by
+  rw [sub_eq_add_neg]
+  exact hg.add_stronglyMeasurable hf.neg
+
+/-- In a normed vector space, the addition of a strongly measurable function and a measurable
+function is measurable. Note that this is not true without further second-countability assumptions
+for the addition of two measurable functions. -/
+theorem _root_.Measurable.stronglyMeasurable_add
+    {α E : Type*} {_ : MeasurableSpace α} [AddGroup E] [TopologicalSpace E]
+    [MeasurableSpace E] [BorelSpace E] [ContinuousAdd E] [PseudoMetrizableSpace E]
+    {g f : α → E} (hg : Measurable g) (hf : StronglyMeasurable f) :
+    Measurable (f + g) := by
+  rcases hf with ⟨φ, hφ⟩
+  have : Tendsto (fun n x ↦ φ n x + g x) atTop (𝓝 (f + g)) :=
+    tendsto_pi_nhds.2 (fun x ↦ (hφ x).add tendsto_const_nhds)
+  apply measurable_of_tendsto_metrizable (fun n ↦ ?_) this
+  exact hg.simpleFunc_add _
+
 end Arithmetic
 
 section MulAction

Mathlib/MeasureTheory/Function/UniformIntegrable.lean

@@ -917,23 +917,19 @@ theorem uniformIntegrable_iff [IsFiniteMeasure μ] (hp : 1 ≤ p) (hp' : p ≠ 
 #align measure_theory.uniform_integrable_iff MeasureTheory.uniformIntegrable_iff
 
 /-- The averaging of a uniformly integrable sequence is also uniformly integrable. -/
-theorem uniformIntegrable_average (hp : 1 ≤ p) {f : ℕ → α → ℝ} (hf : UniformIntegrable f p μ) :
-    UniformIntegrable (fun n => (∑ i in Finset.range n, f i) / (n : α → ℝ)) p μ := by
+theorem uniformIntegrable_average
+    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
+    (hp : 1 ≤ p) {f : ℕ → α → E} (hf : UniformIntegrable f p μ) :
+    UniformIntegrable (fun (n : ℕ) => (n : ℝ)⁻¹ • (∑ i in Finset.range n, f i)) p μ := by
   obtain ⟨hf₁, hf₂, hf₃⟩ := hf
   refine' ⟨fun n => _, fun ε hε => _, _⟩
-  · simp_rw [div_eq_mul_inv]
-    exact (Finset.aestronglyMeasurable_sum' _ fun i _ => hf₁ i).mul
-      (aestronglyMeasurable_const : AEStronglyMeasurable (fun _ => (↑n : ℝ)⁻¹) μ)
+  · exact (Finset.aestronglyMeasurable_sum' _ fun i _ => hf₁ i).const_smul _
   · obtain ⟨δ, hδ₁, hδ₂⟩ := hf₂ hε
     refine' ⟨δ, hδ₁, fun n s hs hle => _⟩
-    simp_rw [div_eq_mul_inv, Finset.sum_mul, Set.indicator_finset_sum]
-    refine' le_trans (snorm_sum_le (fun i _ => ((hf₁ i).mul_const (↑n)⁻¹).indicator hs) hp) _
-    have : ∀ i, s.indicator (f i * (n : α → ℝ)⁻¹) = (↑n : ℝ)⁻¹ • s.indicator (f i) := by
-      intro i
-      rw [mul_comm, (_ : (↑n)⁻¹ * f i = fun ω => (↑n : ℝ)⁻¹ • f i ω)]
-      · rw [Set.indicator_const_smul s (↑n : ℝ)⁻¹ (f i)]
-        rfl
-      · rfl
+    simp_rw [Finset.smul_sum, Set.indicator_finset_sum]
+    refine' le_trans (snorm_sum_le (fun i _ => ((hf₁ i).const_smul _).indicator hs) hp) _
+    have : ∀ i, s.indicator ((n : ℝ) ⁻¹ • f i) = (↑n : ℝ)⁻¹ • s.indicator (f i) :=
+      fun i ↦ indicator_const_smul _ _ _
     simp_rw [this, snorm_const_smul, ← Finset.mul_sum, nnnorm_inv, Real.nnnorm_coe_nat]
     by_cases hn : (↑(↑n : ℝ≥0)⁻¹ : ℝ≥0∞) = 0
     · simp only [hn, zero_mul, zero_le]
@@ -946,13 +942,9 @@ theorem uniformIntegrable_average (hp : 1 ≤ p) {f : ℕ → α → ℝ} (hf :
         ENNReal.inv_mul_cancel _ (ENNReal.nat_ne_top _), one_mul]
       all_goals simpa only [Ne.def, Nat.cast_eq_zero]
   · obtain ⟨C, hC⟩ := hf₃
-    simp_rw [div_eq_mul_inv, Finset.sum_mul]
-    refine' ⟨C, fun n => (snorm_sum_le (fun i _ => (hf₁ i).mul_const (↑n)⁻¹) hp).trans _⟩
-    have : ∀ i, (fun ω => f i ω * (↑n)⁻¹) = (↑n : ℝ)⁻¹ • fun ω => f i ω := by
-      intro i
-      ext ω
-      simp only [mul_comm, Pi.smul_apply, Algebra.id.smul_eq_mul]
-    simp_rw [this, snorm_const_smul, ← Finset.mul_sum, nnnorm_inv, Real.nnnorm_coe_nat]
+    simp_rw [Finset.smul_sum]
+    refine' ⟨C, fun n => (snorm_sum_le (fun i _ => (hf₁ i).const_smul _) hp).trans _⟩
+    simp_rw [snorm_const_smul, ← Finset.mul_sum, nnnorm_inv, Real.nnnorm_coe_nat]
     by_cases hn : (↑(↑n : ℝ≥0)⁻¹ : ℝ≥0∞) = 0
     · simp only [hn, zero_mul, zero_le]
     refine' le_trans _ (_ : ↑(↑n : ℝ≥0)⁻¹ * (n • C : ℝ≥0∞) ≤ C)
@@ -965,7 +957,14 @@ theorem uniformIntegrable_average (hp : 1 ≤ p) {f : ℕ → α → ℝ} (hf :
       rw [ENNReal.coe_smul, nsmul_eq_mul, ← mul_assoc, ENNReal.coe_inv, ENNReal.coe_nat,
         ENNReal.inv_mul_cancel _ (ENNReal.nat_ne_top _), one_mul]
       all_goals simpa only [Ne.def, Nat.cast_eq_zero]
-#align measure_theory.uniform_integrable_average MeasureTheory.uniformIntegrable_average
+
+/-- The averaging of a uniformly integrable real-valued sequence is also uniformly integrable. -/
+theorem uniformIntegrable_average_real (hp : 1 ≤ p) {f : ℕ → α → ℝ} (hf : UniformIntegrable f p μ) :
+    UniformIntegrable (fun n => (∑ i in Finset.range n, f i) / (n : α → ℝ)) p μ := by
+  convert uniformIntegrable_average hp hf using 2 with n
+  ext x
+  simp [div_eq_inv_mul]
+#align measure_theory.uniform_integrable_average MeasureTheory.uniformIntegrable_average_real
 
 end UniformIntegrable
 

Mathlib/MeasureTheory/Integral/Bochner.lean

@@ -1445,6 +1445,17 @@ theorem tendsto_integral_approxOn_of_measurable_of_range_subset [MeasurableSpace
   exact eventually_of_forall fun x => subset_closure (hs (Set.mem_union_left _ (mem_range_self _)))
 #align measure_theory.tendsto_integral_approx_on_of_measurable_of_range_subset MeasureTheory.tendsto_integral_approxOn_of_measurable_of_range_subset
 
+theorem tendsto_integral_norm_approxOn_sub [MeasurableSpace E] [BorelSpace E] {f : α → E}
+    (fmeas : Measurable f) (hf : Integrable f μ) [SeparableSpace (range f ∪ {0} : Set E)] :
+    Tendsto (fun n ↦ ∫ x, ‖SimpleFunc.approxOn f fmeas (range f ∪ {0}) 0 (by simp) n x - f x‖ ∂μ)
+      atTop (𝓝 0) := by
+  convert (tendsto_toReal zero_ne_top).comp (tendsto_approxOn_range_L1_nnnorm fmeas hf) with n
+  rw [integral_norm_eq_lintegral_nnnorm]
+  · simp
+  · apply (SimpleFunc.aestronglyMeasurable _).sub
+    apply (stronglyMeasurable_iff_measurable_separable.2 ⟨fmeas, ?_⟩ ).aestronglyMeasurable
+    exact (isSeparable_of_separableSpace_subtype (range f ∪ {0})).mono (subset_union_left _ _)
+
 variable {ν : Measure α}
 
 theorem integral_add_measure {f : α → G} (hμ : Integrable f μ) (hν : Integrable f ν) :

Mathlib/Probability/IdentDistrib.lean

@@ -120,6 +120,15 @@ protected theorem of_ae_eq {g : α → γ} (hf : AEMeasurable f μ) (heq : f =
     map_eq := Measure.map_congr heq }
 #align probability_theory.ident_distrib.of_ae_eq ProbabilityTheory.IdentDistrib.of_ae_eq
 
+lemma _root_.MeasureTheory.AEMeasurable.identDistrib_mk
+    (hf : AEMeasurable f μ) : IdentDistrib f (hf.mk f) μ μ :=
+  IdentDistrib.of_ae_eq hf hf.ae_eq_mk
+
+lemma _root_.MeasureTheory.AEStronglyMeasurable.identDistrib_mk
+    [TopologicalSpace γ] [PseudoMetrizableSpace γ] [BorelSpace γ]
+    (hf : AEStronglyMeasurable f μ) : IdentDistrib f (hf.mk f) μ μ :=
+  IdentDistrib.of_ae_eq hf.aemeasurable hf.ae_eq_mk
+
 theorem measure_mem_eq (h : IdentDistrib f g μ ν) {s : Set γ} (hs : MeasurableSet s) :
     μ (f ⁻¹' s) = ν (g ⁻¹' s) := by
   rw [← Measure.map_apply_of_aemeasurable h.aemeasurable_fst hs, ←
@@ -306,7 +315,7 @@ section UniformIntegrable
 open TopologicalSpace
 
 variable {E : Type*} [MeasurableSpace E] [NormedAddCommGroup E] [BorelSpace E]
-  [SecondCountableTopology E] {μ : Measure α} [IsFiniteMeasure μ]
+  {μ : Measure α} [IsFiniteMeasure μ]
 
 /-- This lemma is superseded by `Memℒp.uniformIntegrable_of_identDistrib` which only requires
 `AEStronglyMeasurable`. -/
@@ -318,17 +327,21 @@ theorem Memℒp.uniformIntegrable_of_identDistrib_aux {ι : Type*} {f : ι → 
   swap; · exact ⟨0, fun i => False.elim (hι <| Nonempty.intro i)⟩
   obtain ⟨C, hC₁, hC₂⟩ := hℒp.snorm_indicator_norm_ge_pos_le μ (hfmeas _) hε
   refine' ⟨⟨C, hC₁.le⟩, fun i => le_trans (le_of_eq _) hC₂⟩
-  have : {x : α | (⟨C, hC₁.le⟩ : ℝ≥0) ≤ ‖f i x‖₊}.indicator (f i) =
-      (fun x : E => if (⟨C, hC₁.le⟩ : ℝ≥0) ≤ ‖x‖₊ then x else 0) ∘ f i := by
+  have : {x | (⟨C, hC₁.le⟩ : ℝ≥0) ≤ ‖f i x‖₊} = {x | C ≤ ‖f i x‖} := by
+    ext x
+    simp_rw [← norm_toNNReal]
+    exact Real.le_toNNReal_iff_coe_le (norm_nonneg _)
+  rw [this, ← snorm_norm, ← snorm_norm (Set.indicator _ _)]
+  simp_rw [norm_indicator_eq_indicator_norm, coe_nnnorm]
+  let F : E → ℝ := (fun x : E => if (⟨C, hC₁.le⟩ : ℝ≥0) ≤ ‖x‖₊ then ‖x‖ else 0)
+  have F_meas : Measurable F := by
+    apply measurable_norm.indicator (measurableSet_le measurable_const measurable_nnnorm)
+  have : ∀ k, (fun x ↦ Set.indicator {x | C ≤ ‖f k x‖} (fun a ↦ ‖f k a‖) x) = F ∘ f k := by
+    intro k
     ext x
     simp only [Set.indicator, Set.mem_setOf_eq]; norm_cast
-  simp_rw [coe_nnnorm, this]
-  rw [← snorm_map_measure _ (hf i).aemeasurable_fst, (hf i).map_eq,
-    snorm_map_measure _ (hf j).aemeasurable_fst]
-  · rfl
-  all_goals
-    exact_mod_cast aestronglyMeasurable_id.indicator
-      (measurableSet_le measurable_const measurable_nnnorm)
+  rw [this, this, ← snorm_map_measure F_meas.aestronglyMeasurable (hf i).aemeasurable_fst,
+    (hf i).map_eq, snorm_map_measure F_meas.aestronglyMeasurable (hf j).aemeasurable_fst]
 #align probability_theory.mem_ℒp.uniform_integrable_of_ident_distrib_aux ProbabilityTheory.Memℒp.uniformIntegrable_of_identDistrib_aux
 
 /-- A sequence of identically distributed Lᵖ functions is p-uniformly integrable. -/