English
The almost sure convergence of truncated sums implies convergence of the full sums via Cesàro averaging.
Русский
Практикуется почти наверняка, что усечённые суммы ведут к сходению полных сумм через усреднение Чезаро.
LaTeX
$$∀ᵐ ω, Tendsto (λ n, (∑_{i< n} truncation(X_i) i ω)/n) atTop (𝓝 (𝔼[∑ X_0 0]))$$
Lean4
/-- **Strong law of large numbers**, almost sure version: if `X n` is a sequence of independent
identically distributed integrable real-valued random variables, then `∑ i ∈ range n, X i / n`
converges almost surely to `𝔼[X 0]`. We give here the strong version, due to Etemadi, that only
requires pairwise independence. Superseded by `strong_law_ae`, which works for random variables
taking values in any Banach space. -/
theorem strong_law_ae_real {Ω : Type*} {m : MeasurableSpace Ω} {μ : Measure Ω} (X : ℕ → Ω → ℝ)
(hint : Integrable (X 0) μ) (hindep : Pairwise ((IndepFun · · μ) on X))
(hident : ∀ i, IdentDistrib (X i) (X 0) μ μ) :
∀ᵐ ω ∂μ, Tendsto (fun n : ℕ => (∑ i ∈ range n, X i ω) / n) atTop (𝓝 μ[X 0]) :=
by
let mΩ : MeasureSpace Ω :=
⟨μ⟩
-- first get rid of 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)
-- then consider separately the positive and the negative part, and apply the result
-- for nonnegative functions to them.
let pos : ℝ → ℝ := fun x => max x 0
let neg : ℝ → ℝ := fun x => max (-x) 0
have posm : Measurable pos := measurable_id'.max measurable_const
have negm : Measurable neg := measurable_id'.neg.max measurable_const
have A : ∀ᵐ ω, Tendsto (fun n : ℕ => (∑ i ∈ range n, (pos ∘ X i) ω) / n) atTop (𝓝 𝔼[pos ∘ X 0]) :=
strong_law_aux7 _ hint.pos_part (fun i j hij => (hindep hij).comp posm posm) (fun i => (hident i).comp posm)
fun i ω => le_max_right _ _
have B : ∀ᵐ ω, Tendsto (fun n : ℕ => (∑ i ∈ range n, (neg ∘ X i) ω) / n) atTop (𝓝 𝔼[neg ∘ X 0]) :=
strong_law_aux7 _ hint.neg_part (fun i j hij => (hindep hij).comp negm negm) (fun i => (hident i).comp negm)
fun i ω => le_max_right _ _
filter_upwards [A, B] with ω hωpos hωneg
convert hωpos.sub hωneg using 2
· simp only [pos, neg, ← sub_div, ← sum_sub_distrib, max_zero_sub_max_neg_zero_eq_self, Function.comp_apply]
·
simp only [pos, neg, ← integral_sub hint.pos_part hint.neg_part, max_zero_sub_max_neg_zero_eq_self,
Function.comp_apply, mΩ]
