def partialSum {Ω : Type u_1} {n : ℕ} (X : Fin n → Ω → ℝ) (k : Fin n) (ω : Ω) : ℝ

The partial sum Sₖ(ω) = ∑_{i ≤ k} Xᵢ(ω) of a finite family of random variables.

def stoppingEvent {Ω : Type u_1} {n : ℕ} (X : Fin n → Ω → ℝ) (ε : ℝ) (k : Fin n) : Set Ω

The "first crossing at time k" event: the set of ω for which |Sₖ(ω)| ≥ ε but |Sⱼ(ω)| < ε for every j < k. These events partition {∃ k, |Sₖ| ≥ ε} into disjoint pieces and are the standard tool in the proof of Kolmogorov's maximal inequality.

def fullSum {Ω : Type u_1} {n : ℕ} (X : Fin n → Ω → ℝ) (ω : Ω) : ℝ

The full sum Sₙ(ω) = ∑_{i : Fin n} Xᵢ(ω) of the family X.

def tailSum {Ω : Type u_1} {n : ℕ} (X : Fin n → Ω → ℝ) (k : Fin n) (ω : Ω) : ℝ

The tail sum ∑_{i > k} Xᵢ(ω) after index k.

theorem fullSum_eq_partialSum_add_tailSum {Ω : Type u_1} {n : ℕ} (X : Fin n → Ω → ℝ) (k : Fin n) (ω : Ω) : fullSum X ω = partialSum X k ω + tailSum X k ω

Decomposition Sₙ = Sₖ + (Sₙ - Sₖ) of the full sum into the partial sum up to k plus the tail after k.

theorem stopping_events_disjoint {Ω : Type u_1} {n : ℕ} (X : Fin n → Ω → ℝ) (ε : ℝ) : Pairwise fun (i j : Fin n) => Disjoint (stoppingEvent X ε i) (stoppingEvent X ε j)

The "first crossing at time k" events are pairwise disjoint over k : Fin n.

theorem stopping_events_cover {Ω : Type u_1} {n : ℕ} (X : Fin n → Ω → ℝ) {ε : ℝ} (_hε : 0 < ε) : {ω : Ω | ∃ (k : Fin n), |partialSum X k ω| ≥ ε} = ⋃ (k : Fin n), stoppingEvent X ε k

The event {∃ k, |Sₖ| ≥ ε} decomposes as the disjoint union of the "first crossing" stopping events stoppingEvent X ε k over k : Fin n.

theorem measurable_partialSum {Ω : Type u_1} {m : MeasurableSpace Ω} {n : ℕ} (X : Fin n → Ω → ℝ) (hmeas : ∀ (i : Fin n), Measurable (X i)) (k : Fin n) : Measurable (partialSum X k)

Each partial sum Sₖ is measurable whenever each Xᵢ is measurable.

theorem stopping_events_measurable {Ω : Type u_1} {m : MeasurableSpace Ω} {n : ℕ} (X : Fin n → Ω → ℝ) (hmeas : ∀ (i : Fin n), Measurable (X i)) (ε : ℝ) (k : Fin n) : MeasurableSet (stoppingEvent X ε k)

The stopping events stoppingEvent X ε k are measurable whenever each Xᵢ is.

theorem partialSum_measurable {Ω : Type u_1} {m : MeasurableSpace Ω} {n : ℕ} {X : Fin n → Ω → ℝ} (hmeas : ∀ (i : Fin n), Measurable (X i)) (k : Fin n) : Measurable (partialSum X k)

Variant of measurable_partialSum with X implicit.

theorem partialSum_sq_integrable {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} {X : Fin n → Ω → ℝ} (hmeas : ∀ (i : Fin n), Measurable (X i)) (hvar : ∀ (i : Fin n), MeasureTheory.Integrable (fun (ω : Ω) => X i ω ^ 2) μ) (k : Fin n) : MeasureTheory.Integrable (fun (ω : Ω) => partialSum X k ω ^ 2) μ

If each Xᵢ is square-integrable then each partial sum Sₖ is square-integrable.

theorem tailSum_sq_integrable {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} {X : Fin n → Ω → ℝ} (hmeas : ∀ (i : Fin n), Measurable (X i)) (hvar : ∀ (i : Fin n), MeasureTheory.Integrable (fun (ω : Ω) => X i ω ^ 2) μ) (k : Fin n) : MeasureTheory.Integrable (fun (ω : Ω) => tailSum X k ω ^ 2) μ

If each Xᵢ is square-integrable then each tail sum is square-integrable.

theorem cross_term_integrable {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} {X : Fin n → Ω → ℝ} (hmeas : ∀ (i : Fin n), Measurable (X i)) (hvar : ∀ (i : Fin n), MeasureTheory.Integrable (fun (ω : Ω) => X i ω ^ 2) μ) (k : Fin n) : MeasureTheory.Integrable (fun (ω : Ω) => partialSum X k ω * tailSum X k ω) μ

Integrability of the cross term Sₖ · (Sₙ - Sₖ) from Cauchy–Schwarz applied to the square-integrable partial and tail sums.

def piPartialSum' {n : ℕ} (k : Fin n) (v : ↥(Finset.Iic k) → ℝ) (j : Fin n) : ℝ

The "abstract" partial sum: given a vector v indexed by Finset.Iic k, sum its components at indices ≤ j. Used to express Sⱼ as a function of (Xᵢ)_{i ≤ k} for independence arguments.

def piStoppingSet {n : ℕ} (ε : ℝ) (k : Fin n) : Set (↥(Finset.Iic k) → ℝ)

The "abstract" version of stoppingEvent as a subset of ↥(Finset.Iic k) → ℝ.

noncomputable def piPhi' {n : ℕ} (ε : ℝ) (k : Fin n) : (↥(Finset.Iic k) → ℝ) → ℝ

The function Φ on ↥(Finset.Iic k) → ℝ that takes value Sₖ(v) on the stopping set and 0 outside it. When composed with ω ↦ (Xᵢ(ω))_{i ≤ k} it recovers the indicator-weighted partial sum 1_{stoppingEvent} · Sₖ.

def piPsi' {n : ℕ} (k : Fin n) (v : ↥(Finset.Ioi k) → ℝ) : ℝ

The function Ψ on ↥(Finset.Ioi k) → ℝ summing all coordinates; composed with ω ↦ (Xᵢ(ω))_{i > k} it gives the tail sum Sₙ - Sₖ.

theorem piPartialSum'_comp {Ω : Type u_1} {n : ℕ} (X : Fin n → Ω → ℝ) (k : Fin n) (ω : Ω) (j : Fin n) (hj : j ≤ k) : piPartialSum' k (fun (i : ↥(Finset.Iic k)) => X (↑i) ω) j = partialSum X j ω

Compatibility of piPartialSum' with partialSum: feeding the actual sample values (Xᵢ(ω))_{i ≤ k} and evaluating at j ≤ k recovers partialSum X j ω.

theorem piPhi'_comp {Ω : Type u_1} {n : ℕ} (X : Fin n → Ω → ℝ) (ε : ℝ) (k : Fin n) (ω : Ω) : (piPhi' ε k fun (i : ↥(Finset.Iic k)) => X (↑i) ω) = (stoppingEvent X ε k).indicator (partialSum X k) ω

Composing piPhi' with ω ↦ (Xᵢ(ω))_{i ≤ k} gives the indicator-weighted partial sum 1_{stoppingEvent X ε k}(ω) · Sₖ(ω).

theorem piPsi'_comp {Ω : Type u_1} {n : ℕ} (X : Fin n → Ω → ℝ) (k : Fin n) (ω : Ω) : (piPsi' k fun (j : ↥(Finset.Ioi k)) => X (↑j) ω) = tailSum X k ω

Composing piPsi' with ω ↦ (Xᵢ(ω))_{i > k} recovers the tail sum Sₙ - Sₖ.

theorem piStoppingSet_eq {n : ℕ} (ε : ℝ) (k : Fin n) : piStoppingSet ε k = {v : ↥(Finset.Iic k) → ℝ | ε ≤ |piPartialSum' k v k|} ∩ ⋂ j ∈ Finset.Iio k, {v : ↥(Finset.Iic k) → ℝ | |piPartialSum' k v j| < ε}

Rewriting piStoppingSet as an intersection of basic sets, convenient for proving measurability.

theorem measurable_piPhi' {n : ℕ} (ε : ℝ) (k : Fin n) : Measurable (piPhi' ε k)

piPhi' is measurable on the product space ↥(Finset.Iic k) → ℝ.

theorem measurable_piPsi' {n : ℕ} (k : Fin n) : Measurable (piPsi' k)

piPsi' is measurable on ↥(Finset.Ioi k) → ℝ.

theorem cross_term_vanishes {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} {X : Fin n → Ω → ℝ} (hind : ProbabilityTheory.iIndepFun X μ) (hmeas : ∀ (i : Fin n), Measurable (X i)) (hmean : ∀ (i : Fin n), ∫ (ω : Ω), X i ω ∂μ = 0) (hvar : ∀ (i : Fin n), MeasureTheory.Integrable (fun (ω : Ω) => X i ω ^ 2) μ) {ε : ℝ} (_hε : 0 < ε) (k : Fin n) : ∫ (ω : Ω) in stoppingEvent X ε k, partialSum X k ω * tailSum X k ω ∂μ = 0

The cross term integrates to zero on the stopping event: for independent mean-zero Xᵢ, ∫_{stoppingEvent X ε k} Sₖ · (Sₙ - Sₖ) dμ = 0. This uses independence between the σ-algebra generated by (Xᵢ)_{i ≤ k} and the tail (Xᵢ)_{i > k}.

theorem integral_partialSum_sq_le_fullSum_sq {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} {X : Fin n → Ω → ℝ} (hind : ProbabilityTheory.iIndepFun X μ) (hmeas : ∀ (i : Fin n), Measurable (X i)) (hmean : ∀ (i : Fin n), ∫ (ω : Ω), X i ω ∂μ = 0) (hvar : ∀ (i : Fin n), MeasureTheory.Integrable (fun (ω : Ω) => X i ω ^ 2) μ) {ε : ℝ} (hε : 0 < ε) (k : Fin n) : ∫ (ω : Ω) in stoppingEvent X ε k, partialSum X k ω ^ 2 ∂μ ≤ ∫ (ω : Ω) in stoppingEvent X ε k, fullSum X ω ^ 2 ∂μ

On each stopping event, ∫ Sₖ² ≤ ∫ Sₙ² (a consequence of vanishing of the cross term and nonnegativity of (Sₙ - Sₖ)²).

theorem per_event_bound {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} {X : Fin n → Ω → ℝ} (hind : ProbabilityTheory.iIndepFun X μ) (hmeas : ∀ (i : Fin n), Measurable (X i)) (hmean : ∀ (i : Fin n), ∫ (ω : Ω), X i ω ∂μ = 0) (hvar : ∀ (i : Fin n), MeasureTheory.Integrable (fun (ω : Ω) => X i ω ^ 2) μ) {ε : ℝ} (hε : 0 < ε) (k : Fin n) : ENNReal.ofReal (ε ^ 2) * μ (stoppingEvent X ε k) ≤ ENNReal.ofReal (∫ (ω : Ω) in stoppingEvent X ε k, fullSum X ω ^ 2 ∂μ)

The per-stopping-event bound: ε² · μ(stoppingEvent X ε k) ≤ ∫_{stoppingEvent X ε k} Sₙ² dμ. This is the key estimate that, summed over k, yields Kolmogorov's maximal inequality.

theorem variance_as_sum {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} {X : Fin n → Ω → ℝ} (hind : ProbabilityTheory.iIndepFun X μ) (hmeas : ∀ (i : Fin n), Measurable (X i)) (hmean : ∀ (i : Fin n), ∫ (ω : Ω), X i ω ∂μ = 0) (hvar : ∀ (i : Fin n), MeasureTheory.Integrable (fun (ω : Ω) => X i ω ^ 2) μ) : ∫ (ω : Ω), fullSum X ω ^ 2 ∂μ = ∑ i : Fin n, ∫ (ω : Ω), X i ω ^ 2 ∂μ

For independent mean-zero Xᵢ, the variance of Sₙ is the sum of variances: E[Sₙ²] = ∑ᵢ E[Xᵢ²].

theorem fullSum_sq_integrable {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} {X : Fin n → Ω → ℝ} (hmeas : ∀ (i : Fin n), Measurable (X i)) (hvar : ∀ (i : Fin n), MeasureTheory.Integrable (fun (ω : Ω) => X i ω ^ 2) μ) : MeasureTheory.Integrable (fun (ω : Ω) => fullSum X ω ^ 2) μ

The full sum Sₙ is square-integrable when each Xᵢ is square-integrable.

theorem aggregate_bound {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} {X : Fin n → Ω → ℝ} (hind : ProbabilityTheory.iIndepFun X μ) (hmeas : ∀ (i : Fin n), Measurable (X i)) (hmean : ∀ (i : Fin n), ∫ (ω : Ω), X i ω ∂μ = 0) (hvar : ∀ (i : Fin n), MeasureTheory.Integrable (fun (ω : Ω) => X i ω ^ 2) μ) {ε : ℝ} (hε : 0 < ε) : ENNReal.ofReal (ε ^ 2) * μ {ω : Ω | ∃ (k : Fin n), |partialSum X k ω| ≥ ε} ≤ ENNReal.ofReal (∫ (ω : Ω), fullSum X ω ^ 2 ∂μ)

Aggregating the per-event bound over all stopping events: ε² · μ{∃ k, |Sₖ| ≥ ε} ≤ E[Sₙ²].

theorem kolmogorov_maximal_inequality {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} {X : Fin n → Ω → ℝ} (hind : ProbabilityTheory.iIndepFun X μ) (hmeas : ∀ (i : Fin n), Measurable (X i)) (hmean : ∀ (i : Fin n), ∫ (ω : Ω), X i ω ∂μ = 0) (hvar : ∀ (i : Fin n), MeasureTheory.Integrable (fun (ω : Ω) => X i ω ^ 2) μ) {ε : ℝ} (hε : 0 < ε) : μ {ω : Ω | ∃ (k : Fin n), |partialSum X k ω| ≥ ε} ≤ ENNReal.ofReal (∑ i : Fin n, ∫ (ω : Ω), X i ω ^ 2 ∂μ) / ENNReal.ofReal (ε ^ 2)

Kolmogorov's maximal inequality. Suppose X₁, …, Xₙ are independent mean-zero random variables with finite variances and Sₖ = ∑_{i ≤ k} Xᵢ. Then for every ε > 0, P{max_{1 ≤ k ≤ n} |Sₖ| ≥ ε} ≤ ε⁻² · Var(Sₙ) = ε⁻² · ∑ᵢ E[Xᵢ²].