Wald's equations

TheoremVanishing of a single cross term in Wald's second equation#✓fully proved

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

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

Used by 1

Used byVanishing of the cross terms in Wald's second equation

TheoremVanishing of the cross terms in Wald's second equation#✓fully proved

The full cross-term contribution to E[(S_T)^2] vanishes: E[∑_{i < T} ∑_{j < i} X_j X_i] = 0 for identically distributed, mean-zero variables, with each X_i independent of the filtration at time i and measurable at time i + 1, given absolute summability of the stopped cross-term series.

theorem wald_cross_terms_zero
    {Ω : Type*} {m : MeasurableSpace Ω} {μ : Measure Ω} [IsProbabilityMeasure μ]
    {X : ℕ → Ω → ℝ}
    (hX_iid : ∀ i j, IdentDistrib (X i) (X j) μ μ)
    (hX_int : Integrable (X 0) μ)
    (hmean : ∫ ω, X 0 ω ∂μ = 0)
    {f : Filtration ℕ m} {T : Ω → ℕ}
    (hT : IsStoppingTime f (fun ω => (T ω : WithTop ℕ)))
    (hXf : ∀ k, Indep (MeasurableSpace.comap (X k) inferInstance) (f k) μ)
    (hadapt : ∀ k, @Measurable Ω ℝ (f (k + 1)) inferInstance (X k))
    (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

Uses 1 · Used by 1

Proof usesVanishing of a single cross term in Wald's second equation

Used byCross terms vanish for a bounded stopping time

TheoremSquare of a finite sum as diagonal plus cross terms#✓fully proved

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 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

TheoremCross terms vanish for a bounded stopping time#✓fully proved

The total cross-term contribution vanishes for a stopping time bounded by a constant, with no extra summability or measurability hypotheses: the sums are finite, and every term past the bound is zero.

theorem wald_cross_terms_zero_of_bounded
    {Ω : Type*} {m : MeasurableSpace Ω} {μ : Measure Ω} [IsProbabilityMeasure μ]
    {X : ℕ → Ω → ℝ}
    (hX_iid : ∀ i j, IdentDistrib (X i) (X j) μ μ)
    (hX_int : Integrable (X 0) μ)
    (hmean : ∫ ω, X 0 ω ∂μ = 0)
    {f : Filtration ℕ m} {T : Ω → ℕ}
    (hT : IsStoppingTime f (fun ω => (T ω : WithTop ℕ)))
    (hXf : ∀ k, Indep (MeasurableSpace.comap (X k) inferInstance) (f k) μ)
    (hadapt : ∀ k, @Measurable Ω ℝ (f (k + 1)) inferInstance (X k))
    {N : ℕ} (hT_bdd : ∀ ω, T ω ≤ N) :
    ∫ ω, (∑ i ∈ Finset.range (T ω), ∑ j ∈ Finset.range i,
      X j ω * X i ω) ∂μ = 0

Uses 1

Proof usesVanishing of the cross terms in Wald's second equation

TheoremIntegrability of the stopped sum in Wald's equation#✓fully proved

Under Wald's hypotheses, the stopped sum is integrable. This reuses Wald's summable L¹ series and applies Mathlib's sum measurability and norm bound.

theorem wald_integrable_stopped_sum
    {Ω : Type*} {m : MeasurableSpace Ω} {μ : Measure Ω} [IsProbabilityMeasure μ]
    {X : ℕ → Ω → ℝ}
    (hX_iid : ∀ i j, IdentDistrib (X i) (X j) μ μ)
    (hX_int : Integrable (X 0) μ)
    {f : Filtration ℕ m} {T : Ω → ℕ}
    (hT : IsStoppingTime f (fun ω => (T ω : WithTop ℕ)))
    (hXf : ∀ k, Indep (MeasurableSpace.comap (X k) inferInstance) (f k) μ)
    (hT_int : Integrable (fun ω => (T ω : ℝ)) μ) :
    Integrable (fun ω => ∑ i ∈ Finset.range (T ω), X i ω) μ

Used by 1

Used byIntegrability of the stopped sum of squares

TheoremWald's equation#✓fully proved

Let Xᵢ be identically distributed integrable real random variables and T a stopping time with E T < ∞, with each Xₖ independent of the filtration at time k. Then E[S_T] = E[X₁] · E[T], where S_T = ∑_{i < T} Xᵢ.

theorem wald_equation
    {Ω : Type*} {m : MeasurableSpace Ω} {μ : Measure Ω} [IsProbabilityMeasure μ]
    {X : ℕ → Ω → ℝ}
    (hX_iid : ∀ i j, IdentDistrib (X i) (X j) μ μ)
    (hX_int : Integrable (X 0) μ)
    {f : Filtration ℕ m} {T : Ω → ℕ}
    (hT : IsStoppingTime f (fun ω => (T ω : WithTop ℕ)))
    (hXf : ∀ k, Indep (MeasurableSpace.comap (X k) inferInstance) (f k) μ)
    (hT_int : Integrable (fun ω => (T ω : ℝ)) μ) :
    ∫ ω, (∑ i ∈ Finset.range (T ω), X i ω) ∂μ =
      (∫ ω, X 0 ω ∂μ) * (∫ ω, (T ω : ℝ) ∂μ)

Used by 1

Used byDiagonal identity in Wald's second equation

TheoremIntegrability of the stopped sum of squares#✓fully proved

The stopped sum of squares is integrable under the stated diagonal hypotheses.

theorem integrable_stopped_sum_sq_diag
    {Ω : Type*} {m : MeasurableSpace Ω} {μ : Measure Ω} [IsProbabilityMeasure μ]
    {X : ℕ → Ω → ℝ}
    (hX_iid : ∀ i j, IdentDistrib (X i) (X j) μ μ)
    (hX_sq_int : Integrable (fun ω => (X 0 ω) ^ 2) μ)
    {f : Filtration ℕ m} {T : Ω → ℕ}
    (hT : IsStoppingTime f (fun ω => (T ω : WithTop ℕ)))
    (hXf : ∀ k, Indep (MeasurableSpace.comap (X k) inferInstance) (f k) μ)
    (hT_int : Integrable (fun ω => (T ω : ℝ)) μ) :
    Integrable (fun ω => ∑ i ∈ Finset.range (T ω), (X i ω) ^ 2) μ

Uses 1

Proof usesIntegrability of the stopped sum in Wald's equation

TheoremDiagonal identity in Wald's second equation#✓fully proved

Wald's equation applied to the squared increments gives the diagonal identity.

theorem wald_diagonal_terms
    {Ω : Type*} {m : MeasurableSpace Ω} {μ : Measure Ω} [IsProbabilityMeasure μ]
    {X : ℕ → Ω → ℝ}
    (hX_iid : ∀ i j, IdentDistrib (X i) (X j) μ μ)
    (hX_sq_int : Integrable (fun ω => (X 0 ω) ^ 2) μ)
    {f : Filtration ℕ m} {T : Ω → ℕ}
    (hT : IsStoppingTime f (fun ω => (T ω : WithTop ℕ)))
    (hXf : ∀ k, Indep (MeasurableSpace.comap (X k) inferInstance) (f k) μ)
    (hT_int : Integrable (fun ω => (T ω : ℝ)) μ) :
    ∫ ω, (∑ i ∈ Finset.range (T ω), (X i ω) ^ 2) ∂μ =
      (∫ ω, (X 0 ω) ^ 2 ∂μ) * (∫ ω, (T ω : ℝ) ∂μ)

Uses 1

Proof usesWald's equation

TheoremWald's second equation#✓fully proved

Let \((\Omega, \mathbb{P})\) be a probability space with a filtration \((\mathcal{F}_k)_{k \ge 0}\), and let \(X_0, X_1, \dots\) be identically distributed real random variables with \(\mathbb{E}|X_0| < \infty\), \(\mathbb{E}[X_0] = 0\) and \(\mathbb{E}[X_0^2] < \infty\). Let \(T\) be an \(\mathbb{N}\)-valued stopping time for \((\mathcal{F}_k)\) with \(\mathbb{E}[T] < \infty\). Suppose each \(X_k\) is independent of \(\mathcal{F}_k\) and is \(\mathcal{F}_{k+1}\)-measurable. Then \(\mathbb{E}\big[\big(\sum_{i < T} X_i\big)^2\big] = \mathbb{E}[X_0^2] \cdot \mathbb{E}[T]\).

public theorem wald_second_equation
    {Ω : Type*} {m : MeasurableSpace Ω} {μ : Measure Ω} [IsProbabilityMeasure μ]
    {X : ℕ → Ω → ℝ}
    (hX_iid : ∀ i j, IdentDistrib (X i) (X j) μ μ)
    (hX_int : Integrable (X 0) μ)
    (hmean : ∫ ω, X 0 ω ∂μ = 0)
    (hX_sq_int : Integrable (fun ω => (X 0 ω) ^ 2) μ)
    {ℱ : Filtration ℕ m} {T : Ω → ℕ}
    (hT : IsStoppingTime ℱ (fun ω => (T ω : WithTop ℕ)))
    (hXf : ∀ k, Indep (MeasurableSpace.comap (X k) inferInstance) (ℱ k) μ)
    (hadapt : ∀ k, @Measurable Ω ℝ (ℱ (k + 1)) inferInstance (X k))
    (hT_int : Integrable (fun ω => (T ω : ℝ)) μ) :
    ∫ ω, (∑ i ∈ Finset.range (T ω), X i ω) ^ 2 ∂μ =
      (∫ ω, (X 0 ω) ^ 2 ∂μ) * (∫ ω, (T ω : ℝ) ∂μ)

Used by 2

Used bySquare-integrability of the maximal stopped partial sum · Square-integrability of a stopped partial sum

DefinitionPredictable filtration of a sequence#✓fully proved

The "predictable" filtration associated to a sequence X : ℕ → Ω → ℝ: ℱ_k = σ(X_0, …, X_{k-1}). Ported verbatim from v1 WaldSecondEquation.lean.

noncomputable def predictableFiltration
    {Ω : Type*} (m : MeasurableSpace Ω) (X : ℕ → Ω → ℝ)
    (hX_meas : ∀ i, Measurable (X i)) : Filtration ℕ m where
  seq k := ⨆ (j : ℕ) (_ : j < k), MeasurableSpace.comap (X j) inferInstance
  mono' _i _j hij := iSup₂_le fun l hl => le_iSup₂ (f := fun (l' : ℕ) (_ : l' < _j) =>
    MeasurableSpace.comap (X l') inferInstance) l (Nat.lt_of_lt_of_le hl hij)
  le' _k := iSup₂_le fun j _ => (hX_meas j).comap_le

Used by 3

Used bySquare-integrability of the maximal stopped partial sum · Successor step of the predictable filtration · Predictable filtration at time zero is trivial

TheoremPredictable filtration at time zero is trivial#✓fully proved

The predictable filtration contains no observations at time zero.

@[simp] theorem predictableFiltration_zero {X : ℕ → Ω → ℝ}
    (hX_meas : ∀ i, Measurable (X i)) :
    predictableFiltration m0 X hX_meas 0 = ⊥

Uses 1

Statement usesPredictable filtration of a sequence

TheoremSuccessor step of the predictable filtration#✓fully proved

A successor step adds exactly the next observation to the predictable filtration.

theorem predictableFiltration_succ {X : ℕ → Ω → ℝ}
    (hX_meas : ∀ i, Measurable (X i)) (k : ℕ) :
    predictableFiltration m0 X hX_meas (k + 1) =
      predictableFiltration m0 X hX_meas k ⊔ MeasurableSpace.comap (X k) inferInstance

Uses 1

Statement usesPredictable filtration of a sequence

TheoremSquare-integrability of a stopped partial sum#✓fully proved

Square-integrability of a stopped partial sum, general-filtration form.

theorem integrable_stopped_partialSum_sq {X : ℕ → Ω → ℝ}
    (hX_iid : ∀ i j, IdentDistrib (X i) (X j) μ μ)
    (hX_int : Integrable (X 0) μ)
    (hX_sq_int : Integrable (fun ω => (X 0 ω) ^ 2) μ)
    (hmean : ∫ ω, X 0 ω ∂μ = 0)
    {ℱ : Filtration ℕ m0}
    (hIndep : ∀ k, Indep (MeasurableSpace.comap (X k) inferInstance) (ℱ k) μ)
    (hadapt : ∀ k, Measurable[ℱ (k + 1)] (X k))
    {τ : Ω → ℕ} (hT : IsStoppingTime ℱ (fun ω => (τ ω : WithTop ℕ)))
    (hτ_int : Integrable (fun ω => (τ ω : ℝ)) μ) :
    Integrable (fun ω => (∑ i ∈ Finset.range (τ ω), X i ω) ^ 2) μ

Uses 2

Proof usesDoob's L² maximal inequality, finite horizon · Wald's second equation

TheoremSquare-integrability of the maximal stopped partial sum#✓fully proved

Square-integrability of the maximal stopped partial sum, in v1's form: max_{0 ≤ k ≤ T} Sₖ² is integrable. This is v1's integrable_maximal_stopped_partial_sum_sq, whose proof in v1 was left unproved.

theorem integrable_maximal_stopped_partial_sum_sq {X : ℕ → Ω → ℝ}
    (hX_iid : ∀ i j, IdentDistrib (X i) (X j) μ μ)
    (hX_ind : iIndepFun (β := fun _ => ℝ) X μ)
    (hX_meas : ∀ i, Measurable (X i))
    (hX_int : Integrable (X 0) μ)
    (hmean : ∫ ω, X 0 ω ∂μ = 0)
    (hX_sq_int : Integrable (fun ω => (X 0 ω) ^ 2) μ)
    {T : Ω → ℕ}
    (hT : IsStoppingTime (predictableFiltration m0 X hX_meas) (fun ω => (T ω : WithTop ℕ)))
    (hT_int : Integrable (fun ω => (T ω : ℝ)) μ) :
    Integrable (fun ω => (Finset.range (T ω + 1)).sup'
      ⟨0, Finset.mem_range.mpr (Nat.lt_succ_of_le (Nat.zero_le _))⟩
      (fun k => (∑ i ∈ Finset.range k, X i ω) ^ 2)) μ

Uses 3

Statement usesPredictable filtration of a sequence

Proof usesDoob's L² maximal inequality, finite horizon · Wald's second equation

14 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.