English
For i.i.d. real-valued integrable X_n, the averages ∑_{i< n} X_i / n converge almost surely to E[X_0].
Русский
Для независимых и одинаково распределённых вещественных интегрируемых X_n среднее сходится почти surely к E[X_0].
LaTeX
$$∀ᵐ ω, Tendsto (λ n, (∑_{i=0}^{n-1} X_i ω)/n) atTop (𝓝(𝔼[X_0]))$$
Lean4
/-- The truncation of `Xᵢ` up to `i` satisfies the strong law of large numbers
(with respect to the original expectation) along the sequence
`c^n`, for any `c > 1`. This follows from the version from the truncated expectation, and the
fact that the truncated and the original expectations have the same asymptotic behavior. -/
theorem strong_law_aux4 {c : ℝ} (c_one : 1 < c) :
∀ᵐ ω,
(fun n : ℕ => ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) i ω - ⌊c ^ n⌋₊ * 𝔼[X 0]) =o[atTop] fun n : ℕ =>
(⌊c ^ n⌋₊ : ℝ) :=
by
filter_upwards [strong_law_aux2 X hint hindep hident hnonneg c_one] with ω hω
have A : Tendsto (fun n : ℕ => ⌊c ^ n⌋₊) atTop atTop :=
tendsto_nat_floor_atTop.comp (tendsto_pow_atTop_atTop_of_one_lt c_one)
convert hω.add ((strong_law_aux3 X hint hident).comp_tendsto A) using 1
ext1 n
simp
