Laws of large numbers and random series
Almost-sure behaviour of sums of independent variables: strong and weak laws of large numbers, Kolmogorov's three-series theorem and maximal inequality, truncation techniques, the law of the iterated logarithm, and the Monte Carlo variance rate of sample means.
TheoremKolmogorov's maximal inequality for finitely-valued variables#✓fully proved
Let \(\alpha\) be a finite nonempty set and \(n \in \mathbb{N}\). For each \(i \in \{0, \dots, n-1\}\) let \(p_i\) be a probability vector on \(\alpha\), so \(p_i(a) \ge 0\) and \(\sum_{a \in \alpha} p_i(a) = 1\), and let \(X_i : \alpha \to \mathbb{R}\) satisfy \(\sum_{a \in \alpha} p_i(a) X_i(a) = 0\). Give each \(\omega \in \alpha^n\) the weight \(\prod_{i=0}^{n-1} p_i(\omega_i)\), so that the coordinates are independent with laws \(p_i\). Then for every real \(\lambda > 0\), the total weight of the \(\omega\) for which \(\bigl|\sum_{j \le i} X_j(\omega_j)\bigr| \ge \lambda\) for some \(i\) is at most \(\lambda^{-2} \sum_{i=0}^{n-1} \sum_{a \in \alpha} p_i(a) X_i(a)^2\).
MathlibExt.Probability.KolmogorovMaximal.kolmogorov_maximal_inequality · 16 lines
public theorem kolmogorov_maximal_inequality
{α : Type*} [Fintype α] [Nonempty α]
{n : ℕ}
(p : Fin n → α → ℝ)
(hp_nonneg : ∀ i a, 0 ≤ p i a)
(hp_sum : ∀ i, ∑ a : α, p i a = 1)
(X : Fin n → α → ℝ)
(h_mean : ∀ i, ∑ a : α, p i a * X i a = 0)
(lam : ℝ) (hlam : 0 < lam) :
(∑ ω ∈ Finset.univ.filter
(fun ω : Fin n → α =>
∃ i : Fin n,
|∑ j ∈ Finset.univ.filter
(fun j : Fin n => j ≤ i), X j (ω j)| ≥ lam),
∏ i : Fin n, p i (ω i))
≤ (∑ i : Fin n, ∑ a : α, p i a * (X i a) ^ 2) / lam ^ 2Sources
- A. Kolmogoroff, "Über die Summen durch den Zufall bestimmter unabhängiger Größen", Math. Ann. 99 (1928), 309–319, DOI 10.1007/BF01459098.
TheoremLarge deviations of mean-zero sums on the cube have vanishing measure#●ready to prove
Let \(f : \mathbb{R} \to \mathbb{R}\) be square integrable on \([0,1]\) with \(\int_0^1 f = 0\) and \(\int_0^1 |f|^2 > 0\), and let \((a_n)_{n \in \mathbb{N}}\) be a sequence of positive reals with \(a_n \to \infty\). For each \(n\) let
Then \(m_n(F_n) \to 0\) as \(n \to \infty\), where \(m_n\) is Lebesgue measure on \(\mathbb{R}^n\).
public theorem_wanted tendsto_volume_abs_sum_ge_mul_sqrt (f : ℝ → ℝ) (a : ℕ → ℝ)
(hf_L2 : MemLp f 2 (volume.restrict (Set.Icc (0 : ℝ) 1)))
(hf_mean_zero : ∫ x, f x ∂(volume.restrict (Set.Icc (0 : ℝ) 1)) = 0)
(hf_sq_pos : 0 < ∫ x, |f x| ^ 2 ∂(volume.restrict (Set.Icc (0 : ℝ) 1)))
(ha_pos : ∀ n, 0 < a n)
(ha_tendsto : Filter.Tendsto a Filter.atTop Filter.atTop)
(F : ∀ n : ℕ, Set (Fin n → ℝ))
(hF : ∀ n x, x ∈ F n ↔
(∀ i : Fin n, x i ∈ Set.Icc (0 : ℝ) 1) ∧
a n * Real.sqrt n ≤ |∑ i : Fin n, f (x i)|) :
Filter.Tendsto (fun n => volume (F n)) Filter.atTop (nhds 0)Sources
- MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Measure and integration; Classical measure theory), problem
ma_proofbench_l2_06.
TheoremVariance of the sample mean of i.i.d. samples#✓fully proved
Let \(X_0, X_1, X_2, \dots\) be real-valued random variables on a measure space \((\Omega, \mu)\) that are mutually independent and each have the same distribution as \(X_0\), and suppose \(X_0\) is square-integrable. Then for every integer \(n \ge 1\), with variances taken with respect to \(\mu\),
Square-integrability is required only of \(X_0\); identical distribution transfers it to every sample.
theorem variance_sample_mean_of_iid
{Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω}
(X : ℕ → Ω → ℝ)
(hIndep : iIndepFun X μ)
(hIdent : ∀ i, IdentDistrib (X i) (X 0) μ μ)
(hMemLp : MemLp (X 0) 2 μ)
(n : ℕ) (hn : n ≠ 0) :
variance (fun ω => (∑ i ∈ Finset.range n, X i ω) / (n : ℝ)) μ
= variance (X 0) μ / (n : ℝ)Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.