theorem wald_diagonal_terms {Ω : 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_int : MeasureTheory.Integrable (X 0) μ) (hX_sq_int : MeasureTheory.Integrable (fun (ω : Ω) => X 0 ω ^ 2) μ) {f : MeasureTheory.Filtration ℕ m} {T : Ω → ℕ} (hT : MeasureTheory.IsStoppingTime f fun (ω : Ω) => ↑(T ω)) (hXf : ∀ (k : ℕ), ProbabilityTheory.Indep (MeasurableSpace.comap (X k) inferInstance) (↑f k) μ) (hT_int : MeasureTheory.Integrable (fun (ω : Ω) => ↑(T ω)) μ) : ∫ (ω : Ω), ∑ i ∈ Finset.range (T ω), X i ω ^ 2 ∂μ = (∫ (ω : Ω), X 0 ω ^ 2 ∂μ) * ∫ (ω : Ω), ↑(T ω) ∂μ

Diagonal-term contribution to Wald's second equation: applying Wald's equation to the squared sequence Y_i = X_i ^ 2 yields E[∑_{i < T} X_i^2] = E[X_0^2] · E[T].

theorem cross_pair_integral_zero {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → ℝ} (hX_iid : ∀ (i j : ℕ), ProbabilityTheory.IdentDistrib (X i) (X j) μ μ) (hX_int : MeasureTheory.Integrable (X 0) μ) (hmean : ∫ (ω : Ω), X 0 ω ∂μ = 0) {f : MeasureTheory.Filtration ℕ m} {T : Ω → ℕ} (hT : MeasureTheory.IsStoppingTime f fun (ω : Ω) => ↑(T ω)) (hXf : ∀ (k : ℕ), ProbabilityTheory.Indep (MeasurableSpace.comap (X k) inferInstance) (↑f k) μ) (hadapt : ∀ (j k : ℕ), j < k → Measurable (X j)) (j i : ℕ) (hji : j < i) : ∫ (ω : Ω), if i < T ω then X j ω * X i ω else 0 ∂μ = 0

A single cross term E[X_j · X_i · 1_{T > i}] (with j < i) vanishes when the X_i are i.i.d. mean-zero and X_i is independent of (X_j, 1_{T > i}).

theorem wald_cross_terms_zero {Ω : 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_int : MeasureTheory.Integrable (X 0) μ) (hmean : ∫ (ω : Ω), X 0 ω ∂μ = 0) {f : MeasureTheory.Filtration ℕ m} {T : Ω → ℕ} (hT : MeasureTheory.IsStoppingTime f fun (ω : Ω) => ↑(T ω)) (hXf : ∀ (k : ℕ), ProbabilityTheory.Indep (MeasurableSpace.comap (X k) inferInstance) (↑f k) μ) (hadapt : ∀ (j k : ℕ), j < k → Measurable (X j)) (haesm : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => if n < T ω then ∑ j ∈ Finset.range n, X j ω * X n ω else 0) μ) (hsumm : ∑' (n : ℕ), ∫⁻ (ω : Ω), ‖if n < T ω then ∑ j ∈ Finset.range n, X j ω * X n ω else 0‖ₑ ∂μ ≠ ⊤) : ∫ (ω : Ω), ∑ i ∈ Finset.range (T ω), ∑ j ∈ Finset.range i, X j ω * X i ω ∂μ = 0

The full cross-term contribution to E[(S_T)^2] vanishes: E[∑_{i < T} ∑_{j < i} X_j X_i] = 0 under the i.i.d./independence/mean-zero assumptions, given suitable measurability and summability bookkeeping.

theorem sum_sq_expansion (n : ℕ) (f : ℕ → ℝ) : (∑ i ∈ Finset.range n, f i) ^ 2 = ∑ i ∈ Finset.range n, f i ^ 2 + 2 * ∑ i ∈ Finset.range n, ∑ j ∈ Finset.range i, f j * f i

Algebraic identity expanding the square of a finite sum into diagonal and cross-term contributions: (∑_{i<n} f i)^2 = ∑_{i<n} (f i)^2 + 2 ∑_{i<n} ∑_{j<i} f j · f i.

theorem integrable_stopped_sum_sq_diag {Ω : 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_sq_int : MeasureTheory.Integrable (fun (ω : Ω) => X 0 ω ^ 2) μ) {f : MeasureTheory.Filtration ℕ m} {T : Ω → ℕ} (hT : MeasureTheory.IsStoppingTime f fun (ω : Ω) => ↑(T ω)) (hXf : ∀ (k : ℕ), ProbabilityTheory.Indep (MeasurableSpace.comap (X k) inferInstance) (↑f k) μ) (hT_int : MeasureTheory.Integrable (fun (ω : Ω) => ↑(T ω)) μ) : MeasureTheory.Integrable (fun (ω : Ω) => ∑ i ∈ Finset.range (T ω), X i ω ^ 2) μ

The stopped sum of squares ω ↦ ∑_{i < T(ω)} X_i(ω)^2 is integrable, under i.i.d./independence assumptions with E[X_0^2] < ∞ and E T < ∞.

noncomputable def predictableFiltration {Ω : Type u_1} (m : MeasurableSpace Ω) (X : ℕ → Ω → ℝ) (hX_meas : ∀ (i : ℕ), Measurable (X i)) : MeasureTheory.Filtration ℕ m

The "predictable" filtration associated to a sequence X : ℕ → Ω → ℝ: ℱ_k = σ(X_0, …, X_{k-1}), i.e. the supremum of the σ-algebras generated by X_j for j < k. This makes each X_j measurable strictly before time j+1.

theorem wald_second_equation {Ω : 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 ω)) μ) : ∫ (ω : Ω), (∑ i ∈ Finset.range (T ω), X i ω) ^ 2 ∂μ = (∫ (ω : Ω), X 0 ω ^ 2 ∂μ) * ∫ (ω : Ω), ↑(T ω) ∂μ

Wald's second equation. Let X_i be i.i.d. with E[X_i] = 0 and E[X_i^2] = σ^2 ∈ (0, ∞). If T is a stopping time (for the predictable filtration generated by X) with E[T] < ∞, then E[S_T^2] = σ^2 · E[T], where S_T = ∑_{i < T} X_i.