theorem integrable_maximal_stopped_partial_sum_sq {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → ℝ} (hX_iid : ∀ (i j : ℕ), ProbabilityTheory.IdentDistrib (X i) (X j) μ μ) (hX_ind : ProbabilityTheory.iIndepFun X μ) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (hX_int : MeasureTheory.Integrable (X 0) μ) (hmean : ∫ (ω : Ω), X 0 ω ∂μ = 0) (hX_sq_int : MeasureTheory.Integrable (fun (ω : Ω) => X 0 ω ^ 2) μ) {T : Ω → ℕ} (hT : MeasureTheory.IsStoppingTime (predictableFiltration m X hX_meas) fun (ω : Ω) => ↑(T ω)) (hT_int : MeasureTheory.Integrable (fun (ω : Ω) => ↑(T ω)) μ) : MeasureTheory.Integrable (fun (ω : Ω) => (Finset.range (T ω + 1)).sup' ⋯ fun (k : ℕ) => (∑ i ∈ Finset.range k, X i ω) ^ 2) μ

Let X₁, X₂, … be i.i.d. with E[X₁] = 0 and E[X₁²] < ∞, and let T be a stopping time (relative to the natural filtration) with E[T] < ∞. Writing Sₖ = X₁ + ⋯ + Xₖ, the random variable max_{0 ≤ k ≤ T} Sₖ² is integrable. This is used in conjunction with Wald's second equation to control stopped partial-sum processes.