English
Let X_n: Ω → E be independent and identically distributed vector-valued random variables on a probability space, with E a Banach space. For any simple function φ: E → E, the averages of φ(X_n) converge almost surely to the pushforward expectation μ[φ ∘ X_0], i.e. μ-a.e. ω satisfies lim_{n→∞} (1/n) ∑_{i=0}^{n-1} φ(X_i(ω)) = μ[φ ∘ X_0].
Русский
Пусть X_n: Ω → E — независимая последовательность вектор-случайных величин в банаховом пространстве E, одинаково распределённых. Для любой простой функции φ: E → E средние значения φ(X_n) сходятся почти surely к μ[φ(X_0)].
LaTeX
$$$\forall\, \text{ae } \omega \in \Omega,\; \displaystyle \lim_{n \to \infty} \frac{1}{n} \sum_{i=0}^{n-1} \phi(X_i\omega) = \mu[\phi \circ X_0]$$$
Lean4
/-- Preliminary lemma for the strong law of large numbers for vector-valued random variables:
the composition of the random variables with a simple function satisfies the strong law of large
numbers. -/
theorem strong_law_ae_simpleFunc_comp (X : ℕ → Ω → E) (h' : Measurable (X 0))
(hindep : Pairwise ((IndepFun · · μ) on X)) (hident : ∀ i, IdentDistrib (X i) (X 0) μ μ) (φ : SimpleFunc E E) :
∀ᵐ ω ∂μ, Tendsto (fun n : ℕ ↦ (n : ℝ)⁻¹ • (∑ i ∈ range n, φ (X i ω))) atTop (𝓝 μ[φ ∘ (X 0)]) := by
-- this follows from the one-dimensional version when `φ` takes a single value, and is then
-- extended to the general case by linearity.
classical
refine
SimpleFunc.induction (motive := fun ψ ↦
∀ᵐ ω ∂μ, Tendsto (fun n : ℕ ↦ (n : ℝ)⁻¹ • (∑ i ∈ range n, ψ (X i ω))) atTop (𝓝 μ[ψ ∘ (X 0)])) ?_ ?_ φ
· intro c s hs
simp only [SimpleFunc.const_zero, SimpleFunc.coe_piecewise, SimpleFunc.coe_const, SimpleFunc.coe_zero,
piecewise_eq_indicator, Function.comp_apply]
let F : E → ℝ := indicator s 1
have F_meas : Measurable F := (measurable_indicator_const_iff 1).2 hs
let Y : ℕ → Ω → ℝ := fun n ↦ F ∘ (X n)
have : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ (n : ℝ)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 μ[Y 0]) :=
by
simp only [smul_eq_mul, ← div_eq_inv_mul]
apply strong_law_ae_real
·
exact
SimpleFunc.integrable_of_isFiniteMeasure
((SimpleFunc.piecewise s hs (SimpleFunc.const _ (1 : ℝ)) (SimpleFunc.const _ (0 : ℝ))).comp (X 0) h')
· exact fun i j hij ↦ IndepFun.comp (hindep hij) F_meas F_meas
· exact fun i ↦ (hident i).comp F_meas
filter_upwards [this] with ω hω
have I : indicator s (Function.const E c) = (fun x ↦ (indicator s (1 : E → ℝ) x) • c) :=
by
ext
rw [← indicator_smul_const_apply]
congr! 1
ext
simp
simp only [I, integral_smul_const]
convert Tendsto.smul_const hω c using 1
simp [F, Y, ← sum_smul, smul_smul]
· rintro φ ψ - hφ hψ
filter_upwards [hφ, hψ] with ω hωφ hωψ
convert hωφ.add hωψ using 1
· simp [sum_add_distrib]
· congr 1
rw [← integral_add]
· rfl
· exact (φ.comp (X 0) h').integrable_of_isFiniteMeasure
· exact (ψ.comp (X 0) h').integrable_of_isFiniteMeasure
