theorem measurable_of_isStoppingTime {Ω : Type u_1} {m : MeasurableSpace Ω} {f : MeasureTheory.Filtration ℕ m} {T : Ω → ℕ} (hT : MeasureTheory.IsStoppingTime f fun (ω : Ω) => ↑(T ω)) : Measurable T

If T : Ω → ℕ, viewed as a WithTop ℕ-valued process, is a stopping time with respect to a filtration f, then T is measurable (with respect to the ambient σ-algebra).

theorem tsum_measure_gt_eq_lintegral {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {T : Ω → ℕ} (hT_meas : Measurable T) : ∑' (i : ℕ), μ {ω : Ω | i < T ω} = ∫⁻ (ω : Ω), ↑(T ω) ∂μ

For a measurable T : Ω → ℕ, the layer-cake identity in ℝ≥0∞: ∑'_i μ {T > i} = ∫⁻ T dμ.

theorem nat_eq_tsum_indicator (k : ℕ) : ↑k = ∑' (n : ℕ), if n < k then 1 else 0

Express k : ℕ (cast to ℝ) as the tsum ∑' n, 1_{n < k}.

theorem integral_nat_eq_tsum_prob {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {T : Ω → ℕ} (hT_meas : Measurable T) (hT_int : MeasureTheory.Integrable (fun (ω : Ω) => ↑(T ω)) μ) : ∫ (ω : Ω), ↑(T ω) ∂μ = ∑' (n : ℕ), (μ {ω : Ω | n < T ω}).toReal

Real-valued layer-cake identity: if T : Ω → ℕ is measurable and integrable, then E T = ∑'_n P(T > n).

theorem sum_range_eq_tsum_ite (f : ℕ → ℝ) (n : ℕ) : ∑ i ∈ Finset.range n, f i = ∑' (i : ℕ), if i < n then f i else 0

Rewrite a finite sum ∑_{i < n} f i as an infinite tsum with indicator weights.

theorem indepFun_indicator_of_indep {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {g : Ω → ℝ} {m' : MeasurableSpace Ω} (hindep : ProbabilityTheory.Indep (MeasurableSpace.comap g inferInstance) m' μ) {A : Set Ω} (hA : MeasurableSet A) : ProbabilityTheory.IndepFun g (A.indicator fun (x : Ω) => 1) μ

If the σ-algebra generated by g : Ω → ℝ is independent of a σ-algebra m', and A is m'-measurable, then g is independent of the indicator 1_A (as real-valued random variables).

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

Factorisation lemma underlying Wald's equation: for a stopping time T and i.i.d. sequence X with each X k independent of the filtration at time k, E[X_n · 1_{T > n}] = E[X_n] · P(T > n).

theorem lintegral_enorm_indicator_le {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → ℝ} (hX_ind : ProbabilityTheory.iIndepFun X μ) (hX_int : MeasureTheory.Integrable (X 0) μ) (hX_iid : ∀ (i j : ℕ), ProbabilityTheory.IdentDistrib (X i) (X j) μ μ) {f : MeasureTheory.Filtration ℕ m} {T : Ω → ℕ} (hT : MeasureTheory.IsStoppingTime f fun (ω : Ω) => ↑(T ω)) (hXf : ∀ (k : ℕ), ProbabilityTheory.Indep (MeasurableSpace.comap (X k) inferInstance) (↑f k) μ) (hT_meas : Measurable T) (n : ℕ) : ∫⁻ (a : Ω) in {ω : Ω | n < T ω}, ‖X n a‖ₑ ∂μ ≤ (∫⁻ (a : Ω), ‖X 0 a‖ₑ ∂μ) * μ {ω : Ω | n < T ω}

Per-term bound for Wald's series: the truncated L¹ norm of X n over {T > n} is at most E|X_0| · P(T > n).

theorem summability_condition {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → ℝ} (hX_ind : ProbabilityTheory.iIndepFun X μ) (hX_int : MeasureTheory.Integrable (X 0) μ) (hX_iid : ∀ (i j : ℕ), ProbabilityTheory.IdentDistrib (X i) (X j) μ μ) {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 ω)) μ) : ∑' (n : ℕ), ∫⁻ (a : Ω), ‖if n < T a then X n a else 0‖ₑ ∂μ ≠ ⊤

Summability of the truncated L¹ norms used to justify the interchange of sum and integral in Wald's equation: under the i.i.d./independence hypotheses and E T < ∞, the series ∑'_n ∫ |X_n · 1_{T > n}| dμ is finite.

theorem aesm_summand {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → ℝ} (hX_iid : ∀ (i j : ℕ), ProbabilityTheory.IdentDistrib (X i) (X j) μ μ) (hX_int : MeasureTheory.Integrable (X 0) μ) {T : Ω → ℕ} (hT_meas : Measurable T) (n : ℕ) : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => if n < T ω then X n ω else 0) μ

The truncated summand ω ↦ X_n(ω) · 1_{T(ω) > n} is AEStronglyMeasurable, provided X_n is and T is measurable.

theorem wald_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_int : MeasureTheory.Integrable (X 0) μ) {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 ω ∂μ = (∫ (ω : Ω), X 0 ω ∂μ) * ∫ (ω : Ω), ↑(T ω) ∂μ

Wald's equation. Let X_i be i.i.d. integrable real random variables and T a stopping time with E T < ∞, with each X_k independent of the filtration at time k. Then E[S_T] = E[X_1] · E[T], where S_T = ∑_{i < T} X_i.