English
Under the same independence and identical distribution hypotheses as the vector-valued SLLN, but assuming measurability of the index process, one obtains the same almost-sure convergence of the averages to μ[X_0].
Русский
При тех же гипотезах независимости и одинакового распределения для векторного случая, но с дополнительной измеримостью процесса, средние по векторам сходятся почти surely к μ[X_0].
LaTeX
$$$\forall\, \text{ae } \omega ∂μ,\; \displaystyle \lim_{n \to \infty} \frac{1}{n} \sum_{i=0}^{n-1} X_i(\omega) = μ[X_0]$$$
Lean4
/-- **Strong law of large numbers**, almost sure version: if `X n` is a sequence of independent
identically distributed integrable random variables taking values in a Banach space,
then `n⁻¹ • ∑ i ∈ range n, X i` converges almost surely to `𝔼[X 0]`. We give here the strong
version, due to Etemadi, that only requires pairwise independence. -/
theorem strong_law_ae (X : ℕ → Ω → E) (hint : Integrable (X 0) μ) (hindep : Pairwise ((IndepFun · · μ) on X))
(hident : ∀ i, IdentDistrib (X i) (X 0) μ μ) :
∀ᵐ ω ∂μ, Tendsto (fun n : ℕ ↦ (n : ℝ)⁻¹ • (∑ i ∈ range n, X i ω)) atTop (𝓝 μ[X 0]) := by
-- First exclude the trivial case where the space is not a probability space
by_cases h : ∀ᵐ ω ∂μ, X 0 ω = 0
· have I : ∀ᵐ ω ∂μ, ∀ i, X i ω = 0 := by
rw [ae_all_iff]
intro i
exact (hident i).symm.ae_snd (p := fun x ↦ x = 0) measurableSet_eq h
filter_upwards [I] with ω hω
simpa [hω] using (integral_eq_zero_of_ae h).symm
have : IsProbabilityMeasure μ :=
hint.isProbabilityMeasure_of_indepFun (X 0) (X 1) h
(hindep zero_ne_one)
-- we reduce to the case of strongly measurable random variables, by using `Y i` which is strongly
-- measurable and ae equal to `X i`.
have A : ∀ i, Integrable (X i) μ := fun i ↦ (hident i).integrable_iff.2 hint
let Y : ℕ → Ω → E := fun i ↦ (A i).1.mk (X i)
have B : ∀ᵐ ω ∂μ, ∀ n, X n ω = Y n ω := ae_all_iff.2 (fun i ↦ AEStronglyMeasurable.ae_eq_mk (A i).1)
have Yint : Integrable (Y 0) μ := Integrable.congr hint (AEStronglyMeasurable.ae_eq_mk (A 0).1)
have C : ∀ᵐ ω ∂μ, Tendsto (fun n : ℕ ↦ (n : ℝ)⁻¹ • (∑ i ∈ range n, Y i ω)) atTop (𝓝 μ[Y 0]) := by
apply
strong_law_ae_of_measurable Y Yint ((A 0).1.stronglyMeasurable_mk)
(fun i j hij ↦ IndepFun.congr (hindep hij) (A i).1.ae_eq_mk (A j).1.ae_eq_mk)
(fun i ↦ ((A i).1.identDistrib_mk.symm.trans (hident i)).trans (A 0).1.identDistrib_mk)
filter_upwards [B, C] with ω h₁ h₂
have : μ[X 0] = μ[Y 0] := integral_congr_ae (AEStronglyMeasurable.ae_eq_mk (A 0).1)
rw [this]
apply Tendsto.congr (fun n ↦ ?_) h₂
congr with i
exact (h₁ i).symm
