Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-generatedPipeline-generated
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Kolmogorov maximal inequality

Statement

Let X1,…,Xn be independent centered square-integrable real random variables, n≥1, and Sk=∑j=1kXj. For every λ>0, P(max⁡1≤k≤n∣Sk∣≥λ)≤Var⁡(Sn)λ2=∑j=1nVar⁡(Xj)λ2. Thus controlling the whole finite maximum costs no larger bound than controlling the final sum by Chebyshev.

Facts & Assumptions

[F1]

Disjoint groups of an independent sigma-algebra family remain independent: Let (Fi)i∈I be an independent family of sigma-algebras on a probability space, and let J0,…,Jm−1⊆I be pairwise disjoint index sets. For each r<m, define Gr:=σ(⋃i∈JrFi). Then the sigma-algebras G0,…,Gm−1 are independent.

[F2]

For n≥1, if X0,…,Xn−1 are independent real random variables and gi:R→R are Borel measurable with each gi(Xi) integrable, then ∏i<ngi(Xi) is integrable and E[∏i<ngi(Xi)]=∏i<nE[gi(Xi)] in R (Expectations factor over finite products of independent random variables).

[F3]

Variance and covariance identities for random variables: Let X,Y be square-integrable real random variables on one probability space. Then Var⁡(X)=E[X2]−E[X]2, Cov⁡(X,Y)=E[XY]−E[X]E[Y]. Moreover, covariance is symmetric and bilinear on finite linear combinations. On finite full-power-set probability spaces these formulas reduce to the published finite identities.

[F4]

Arithmetic and lattice operations preserve measurability whenever they are defined: Let (X,A) be a measurable space and let f,g:X→R‾ be measurable. Then: 1. cf is measurable for every real scalar c; 2. max⁡(f,g), min⁡(f,g), ∣f∣, f+, and f− are measurable; 3. if f+g is pointwise defined, then f+g is measurable; 4. with the total function-product convention declared in that theorem, the pointwise product fg is measurable.

Proof

Given: The objects and hypotheses of the statement.

1.1F4given

Let Ak={∣Sj∣<λ (j<k), ∣Sk∣≥λ}. These measurable events are disjoint, and their union is the event in the statement. Measurability follows by finite arithmetic.

2.1F1F2step 1.1

Grouping shows that Sk1Ak and Sn−Sk are independent. Both are integrable (their squares have finite expectation), and the latter has mean zero. Factorization therefore gives E[Sk1Ak(Sn−Sk)]=0. For k=n the tail is zero and the identity still holds.

3.1F3F2step 1.1step 2.1algebra∎

Expand the square on Ak: E[Sn21Ak]=E[Sk21Ak]+E[(Sn−Sk)21Ak]≥λ2P(Ak). Sum over the disjoint events. Centering gives ESn2=Var⁡(Sn), and covariance bilinearity with factorization cancels every off-diagonal covariance. This proves the bound even when the variance is zero or n=1.

Depends on

Used by

Dependency tree · two levels

34 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources