def postStoppingTimeSeq {Ω : Type u_1} {S : Type u_2} (X : ℕ → Ω → S) (T : Ω → ℕ) : ℕ → Ω → S

The post-stopping-time sequence (X_{T+k+1})_{k ≥ 0} obtained from a sequence X : ℕ → Ω → S by shifting the index by T(ω) + 1. This is the sequence of observations immediately after the stopping time T.

theorem identDistrib_tail {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {S : Type u_2} [MeasurableSpace S] {X : ℕ → Ω → S} (hX_id : ∀ (i j : ℕ), ProbabilityTheory.IdentDistrib (X i) (X j) μ μ) (n k : ℕ) : ProbabilityTheory.IdentDistrib (X (n + k + 1)) (X 0) μ μ

For an identically distributed sequence, the shifted variable X (n + k + 1) has the same distribution as X 0.

theorem indep_stopping_time_tail {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {S : Type u_2} [MeasurableSpace S] (X : ℕ → Ω → S) (f : MeasureTheory.Filtration ℕ m) (T : Ω → ℕ) (hX_ind : ProbabilityTheory.iIndepFun X μ) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (hT : MeasureTheory.IsStoppingTime f fun (ω : Ω) => ↑(T ω)) (hfX : ∀ (n : ℕ), ↑f n ≤ ⨆ i ∈ Finset.range (n + 1), MeasurableSpace.comap (X i) inst✝) [MeasureTheory.IsProbabilityMeasure μ] (n k : ℕ) (A : Set S) (hA : MeasurableSet A) : μ ({ω : Ω | T ω = n} ∩ X (n + k + 1) ⁻¹' A) = μ {ω : Ω | T ω = n} * μ (X (n + k + 1) ⁻¹' A)

Key independence lemma: the event {T = n} (which lies in F_n) is independent of the preimage (X_{n+k+1})⁻¹(A) (which depends on a strictly later index), since the underlying sequence is independent.

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

The level set {ω | T(ω) = n} of a stopping time T is measurable in the ambient σ-algebra.

theorem aemeasurable_postStoppingTimeSeq {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {S : Type u_2} [MeasurableSpace S] {X : ℕ → Ω → S} {f : MeasureTheory.Filtration ℕ m} {T : Ω → ℕ} (hX_aem : ∀ (i : ℕ), AEMeasurable (X i) μ) (hT : MeasureTheory.IsStoppingTime f fun (ω : Ω) => ↑(T ω)) (k : ℕ) : AEMeasurable (postStoppingTimeSeq X T k) μ

The post-stopping-time sequence postStoppingTimeSeq X T k is almost-everywhere measurable whenever each X i is and T is a stopping time.

theorem strong_markov_iid_identDistrib {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {S : Type u_2} [MeasurableSpace S] {X : ℕ → Ω → S} {f : MeasureTheory.Filtration ℕ m} {T : Ω → ℕ} (hX_id : ∀ (i j : ℕ), ProbabilityTheory.IdentDistrib (X i) (X j) μ μ) (hX_ind : ProbabilityTheory.iIndepFun X μ) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (hT : MeasureTheory.IsStoppingTime f fun (ω : Ω) => ↑(T ω)) (hfX : ∀ (n : ℕ), ↑f n ≤ ⨆ i ∈ Finset.range (n + 1), MeasurableSpace.comap (X i) inst✝) [MeasureTheory.IsProbabilityMeasure μ] (k : ℕ) : ProbabilityTheory.IdentDistrib (postStoppingTimeSeq X T k) (X 0) μ μ

Strong Markov property (identically-distributed part).

For an i.i.d. sequence X : ℕ → Ω → S and a finite stopping time T, each variable postStoppingTimeSeq X T k = X_{T+k+1} has the same distribution as X 0.

theorem indep_stopping_time_tail_finset {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {S : Type u_2} [MeasurableSpace S] (X : ℕ → Ω → S) (f : MeasureTheory.Filtration ℕ m) (T : Ω → ℕ) (hX_ind : ProbabilityTheory.iIndepFun X μ) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (hT : MeasureTheory.IsStoppingTime f fun (ω : Ω) => ↑(T ω)) (hfX : ∀ (n : ℕ), ↑f n ≤ ⨆ i ∈ Finset.range (n + 1), MeasurableSpace.comap (X i) inst✝) [MeasureTheory.IsProbabilityMeasure μ] (n : ℕ) (SF : Finset ℕ) (sets : ℕ → Set S) (hsets : ∀ k ∈ SF, MeasurableSet (sets k)) : μ ({ω : Ω | T ω = n} ∩ ⋂ k ∈ SF, X (n + k + 1) ⁻¹' sets k) = μ {ω : Ω | T ω = n} * ∏ k ∈ SF, μ (X (n + k + 1) ⁻¹' sets k)

Finite-family version of indep_stopping_time_tail: on {T = n}, the intersection of preimages ⋂_{k ∈ SF} X_{n+k+1}⁻¹(sets k) is independent of {T = n} and the joint probability splits as a product.

theorem postStoppingTimeSeq_preimage_eq {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {S : Type u_2} [MeasurableSpace S] {X : ℕ → Ω → S} {f : MeasureTheory.Filtration ℕ m} {T : Ω → ℕ} (hX_id : ∀ (i j : ℕ), ProbabilityTheory.IdentDistrib (X i) (X j) μ μ) (hX_ind : ProbabilityTheory.iIndepFun X μ) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (hT : MeasureTheory.IsStoppingTime f fun (ω : Ω) => ↑(T ω)) (hfX : ∀ (n : ℕ), ↑f n ≤ ⨆ i ∈ Finset.range (n + 1), MeasurableSpace.comap (X i) inst✝) [MeasureTheory.IsProbabilityMeasure μ] (k : ℕ) (A : Set S) (hA : MeasurableSet A) : μ (postStoppingTimeSeq X T k ⁻¹' A) = μ (X 0 ⁻¹' A)

For each measurable set A, μ((postStoppingTimeSeq X T k)⁻¹(A)) = μ((X 0)⁻¹(A)), i.e. the law of each X_{T+k+1} agrees with that of X 0.

theorem strong_markov_iid_iIndepFun {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {S : Type u_2} [MeasurableSpace S] {X : ℕ → Ω → S} {f : MeasureTheory.Filtration ℕ m} {T : Ω → ℕ} (hX_id : ∀ (i j : ℕ), ProbabilityTheory.IdentDistrib (X i) (X j) μ μ) (hX_ind : ProbabilityTheory.iIndepFun X μ) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (hT : MeasureTheory.IsStoppingTime f fun (ω : Ω) => ↑(T ω)) (hfX : ∀ (n : ℕ), ↑f n ≤ ⨆ i ∈ Finset.range (n + 1), MeasurableSpace.comap (X i) inst✝) [MeasureTheory.IsProbabilityMeasure μ] : ProbabilityTheory.iIndepFun (postStoppingTimeSeq X T) μ

Strong Markov property (independence part).

For an i.i.d. sequence X and a finite stopping time T, the post-stopping sequence (X_{T+k+1})_{k ≥ 0} is itself an independent family.

theorem measurableSet_FT_inter_eq {Ω : Type u_1} {m : MeasurableSpace Ω} {f : MeasureTheory.Filtration ℕ m} {T : Ω → ℕ} (hT : MeasureTheory.IsStoppingTime f fun (ω : Ω) => ↑(T ω)) {A : Set Ω} (hA : MeasurableSet A) (n : ℕ) : MeasurableSet (A ∩ {ω : Ω | T ω = n})

If A is measurable in the stopped σ-algebra F_T, then A ∩ {T = n} is measurable in F_n.

theorem indep_fn_tail_finset {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {S : Type u_2} [MeasurableSpace S] (X : ℕ → Ω → S) (f : MeasureTheory.Filtration ℕ m) (hX_ind : ProbabilityTheory.iIndepFun X μ) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (hfX : ∀ (n : ℕ), ↑f n ≤ ⨆ i ∈ Finset.range (n + 1), MeasurableSpace.comap (X i) inst✝) [MeasureTheory.IsProbabilityMeasure μ] (n : ℕ) (A : Set Ω) (hA : MeasurableSet A) (SF : Finset ℕ) (sets : ℕ → Set S) (hsets : ∀ k ∈ SF, MeasurableSet (sets k)) : μ (A ∩ ⋂ k ∈ SF, X (n + k + 1) ⁻¹' sets k) = μ A * ∏ k ∈ SF, μ (X (n + k + 1) ⁻¹' sets k)

Generalization of indep_stopping_time_tail_finset: any set A ∈ F_n is independent of the finite intersection ⋂_{k ∈ SF} X_{n+k+1}⁻¹(sets k).

theorem strong_markov_iid_indep_past {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {S : Type u_2} [MeasurableSpace S] {X : ℕ → Ω → S} {f : MeasureTheory.Filtration ℕ m} {T : Ω → ℕ} (hX_id : ∀ (i j : ℕ), ProbabilityTheory.IdentDistrib (X i) (X j) μ μ) (hX_ind : ProbabilityTheory.iIndepFun X μ) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (hT : MeasureTheory.IsStoppingTime f fun (ω : Ω) => ↑(T ω)) (hfX : ∀ (n : ℕ), ↑f n ≤ ⨆ i ∈ Finset.range (n + 1), MeasurableSpace.comap (X i) inst✝) [MeasureTheory.IsProbabilityMeasure μ] : ProbabilityTheory.Indep hT.measurableSpace (⨆ (k : ℕ), MeasurableSpace.comap (postStoppingTimeSeq X T k) inst✝) μ

Strong Markov property (independence from the past).

The stopped σ-algebra F_T is independent of the σ-algebra generated by the post-stopping sequence (X_{T+k+1})_{k ≥ 0}.

theorem strong_markov_iid {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {S : Type u_2} [MeasurableSpace S] {X : ℕ → Ω → S} {f : MeasureTheory.Filtration ℕ m} {T : Ω → ℕ} (hX_id : ∀ (i j : ℕ), ProbabilityTheory.IdentDistrib (X i) (X j) μ μ) (hX_ind : ProbabilityTheory.iIndepFun X μ) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (hT : MeasureTheory.IsStoppingTime f fun (ω : Ω) => ↑(T ω)) (hfX : ∀ (n : ℕ), ↑f n ≤ ⨆ i ∈ Finset.range (n + 1), MeasurableSpace.comap (X i) inst✝) [MeasureTheory.IsProbabilityMeasure μ] : (∀ (k : ℕ), ProbabilityTheory.IdentDistrib (postStoppingTimeSeq X T k) (X 0) μ μ) ∧ ProbabilityTheory.iIndepFun (postStoppingTimeSeq X T) μ ∧ ProbabilityTheory.Indep hT.measurableSpace (⨆ (k : ℕ), MeasurableSpace.comap (postStoppingTimeSeq X T k) inst✝) μ

Strong Markov property for i.i.d. sequences.

Let X_1, X_2, … be i.i.d. with values in S, and let T be a finite ℕ-valued stopping time relative to a filtration that contains the filtration generated by X. Then, conditional on {T < ∞}:

1. each X_{T+k+1} has the same distribution as X_0,
2. the sequence (X_{T+k+1})_{k ≥ 0} is independent, and
3. it is independent of the stopped σ-algebra F_T.

In other words, (X_{T+k+1})_{k ≥ 0} is an i.i.d. copy of the original sequence, independent of the past F_T.