Maximal bounds for centered independent partial sums

Independent integrable centered increments yield a martingale of inclusive partial sums. Its second moment is the sum of increment second moments, giving Doob's explicit maximal bound. This complements the tail-based walk inequalities in RealWalkMaximal without duplicating them.

theorem BGW.Probability.martingale_centered_partialSums {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X : ℕ → Ω → ℝ} (hm : ∀ (i : ℕ), MeasureTheory.StronglyMeasurable (X i)) (hi : ProbabilityTheory.iIndepFun X P) (hint : ∀ (i : ℕ), MeasureTheory.Integrable (X i) P) (hzero : ∀ (i : ℕ), ∫ (ω : Ω), X i ω ∂P = 0) : MeasureTheory.Martingale (fun (n : ℕ) (ω : Ω) => ∑ i ∈ Finset.range (n + 1), X i ω) (MeasureTheory.Filtration.natural X hm) P

Independent integrable centered increments give a martingale of inclusive partial sums.

theorem BGW.Probability.integral_partialSum_sq_eq_sum {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X : ℕ → Ω → ℝ} (hmem : ∀ (i : ℕ), MeasureTheory.MemLp (X i) 2 P) (hi : ProbabilityTheory.iIndepFun X P) (hzero : ∀ (i : ℕ), ∫ (ω : Ω), X i ω ∂P = 0) (s : Finset ℕ) : ∫ (ω : Ω), (∑ i ∈ s, X i ω) ^ 2 ∂P = ∑ i ∈ s, ∫ (ω : Ω), X i ω ^ 2 ∂P

The centered second moment of independent partial sums is the sum of their variances.

theorem BGW.Probability.measure_partialSum_maximal_le {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X : ℕ → Ω → ℝ} (hm : ∀ (i : ℕ), MeasureTheory.StronglyMeasurable (X i)) (hi : ProbabilityTheory.iIndepFun X P) (hmem : ∀ (i : ℕ), MeasureTheory.MemLp (X i) 2 P) (hzero : ∀ (i : ℕ), ∫ (ω : Ω), X i ω ∂P = 0) (m : ℕ) {r : ℝ} (hr : 0 < r) : P {ω : Ω | ∃ N ∈ Finset.range (m + 1), r < |∑ i ∈ Finset.range N, X i ω|} ≤ ENNReal.ofReal ((4 * ∑ i ∈ Finset.range (m + 1), ∫ (ω : Ω), X i ω ^ 2 ∂P) / r ^ 2)

A second-moment maximal bound for independent centered increments, allowing one extra terminal increment in the upper bound.