Strong Markov property of i.i.d. sequences

DefinitionPost-stopping-time sequence#✓fully proved

Given maps \(X_0, X_1, X_2, \dots\) from a set \(\Omega\) to a set \(S\) and a map \(T : \Omega \to \mathbb{N}\), the post-stopping-time sequence is the sequence \((Y_k)_{k \in \mathbb{N}}\) of maps from \(\Omega\) to \(S\) given by \(Y_k(\omega) = X_{T(\omega)+k+1}(\omega)\). When \(T\) is a stopping time, this is the sequence of observations immediately after time \(T\).

def postStoppingTimeSeq (X : ℕ → Ω → S) (T : Ω → ℕ) : ℕ → Ω → S :=
  fun k ω => X (T ω + k + 1) ω

Used by 6

Used byThe post-stopping-time sequence is a.e. measurable · Preimage measures of a post-stopping-time variable · Strong Markov property for i.i.d. sequences: independence after a stopping time · Strong Markov property for i.i.d. sequences: the law after a stopping time · Strong Markov property (independence from the past) · Strong Markov property for i.i.d. sequences: the post-stopping-time sequence is i.i.d

LemmaShifted terms of an identically distributed sequence#✓fully proved

Let \(\mu\) be a measure on a measurable space \(\Omega\) and let \(X_0, X_1, X_2, \dots\) be maps from \(\Omega\) to a measurable space \(S\) such that \(X_i\) and \(X_j\) are identically distributed under \(\mu\) for all \(i, j\). Then for all \(n, k \in \mathbb{N}\) the map \(X_{n+k+1}\) has the same distribution under \(\mu\) as \(X_0\).

lemma identDistrib_tail {X : ℕ → Ω → S}
    (hX_id : ∀ i j, IdentDistrib (X i) (X j) μ μ)
    (n k : ℕ) :
    IdentDistrib (X (n + k + 1)) (X 0) μ μ

Used by 1

Used byStrong Markov property for i.i.d. sequences: the law after a stopping time

LemmaA stopping-time event is independent of a later observation#✓fully proved

Let \(\mu\) be a probability measure on a measurable space \(\Omega\), let \((\mathcal{F}_n)_{n \in \mathbb{N}}\) be a filtration on \(\Omega\), and let \(X_0, X_1, X_2, \dots\) be measurable maps from \(\Omega\) to a measurable space \(S\) that are mutually independent under \(\mu\). Suppose that for every \(n\) the σ-algebra \(\mathcal{F}_n\) is contained in the σ-algebra generated by \(X_0, \dots, X_n\), and let \(T : \Omega \to \mathbb{N}\) be a stopping time for \((\mathcal{F}_n)\). Then for all \(n, k \in \mathbb{N}\) and every measurable set \(A \subseteq S\), \(\mu(\{T = n\} \cap X_{n+k+1}^{-1}(A)) = \mu(\{T = n\})\,\mu(X_{n+k+1}^{-1}(A))\).

lemma indep_stopping_time_tail
    (X : ℕ → Ω → S) (f : Filtration ℕ m) (T : Ω → ℕ)
    (hX_ind : iIndepFun (m := fun _ => ‹MeasurableSpace S›) X μ)
    (hX_meas : ∀ i, Measurable (X i))
    (hT : IsStoppingTime f (fun ω => (T ω : ℕ∞)))
    (hfX : ∀ n, f n ≤ ⨆ i ∈ Finset.range (n + 1), MeasurableSpace.comap (X i) ‹MeasurableSpace S›)
    [IsProbabilityMeasure μ]
    (n k : ℕ) (A : Set S) (hA : MeasurableSet A) :
    μ ({ω | T ω = n} ∩ (X (n + k + 1)) ⁻¹' A) =
      μ {ω | T ω = n} * μ ((X (n + k + 1)) ⁻¹' A)

Used by 2

Used byPreimage measures of a post-stopping-time variable · Strong Markov property for i.i.d. sequences: the law after a stopping time

LemmaLevel sets of a stopping time are measurable#✓fully proved

Let \((\mathcal{F}_n)_{n \in \mathbb{N}}\) be a filtration on a measurable space \(\Omega\) and let \(T : \Omega \to \mathbb{N}\) be a stopping time for \((\mathcal{F}_n)\). Then for every \(n \in \mathbb{N}\) the set \(\{\omega : T(\omega) = n\}\) is measurable in the σ-algebra of \(\Omega\).

lemma measurableSet_stoppingTime_eq {f : Filtration ℕ m} {T : Ω → ℕ}
    (hT : IsStoppingTime f (fun ω => (T ω : ℕ∞))) (n : ℕ) :
    MeasurableSet {ω | T ω = n}

Used by 5

Used byThe post-stopping-time sequence is a.e. measurable · Preimage measures of a post-stopping-time variable · Strong Markov property for i.i.d. sequences: independence after a stopping time · Strong Markov property for i.i.d. sequences: the law after a stopping time · Strong Markov property (independence from the past)

LemmaThe post-stopping-time sequence is a.e. measurable#✓fully proved

Let \(\mu\) be a measure on a measurable space \(\Omega\), let \((\mathcal{F}_n)_{n \in \mathbb{N}}\) be a filtration on \(\Omega\), let \(X_0, X_1, X_2, \dots\) be maps from \(\Omega\) to a measurable space \(S\) that are each \(\mu\)-almost-everywhere measurable, and let \(T : \Omega \to \mathbb{N}\) be a stopping time for \((\mathcal{F}_n)\). Then for every \(k \in \mathbb{N}\) the map \(\omega \mapsto X_{T(\omega)+k+1}(\omega)\) is \(\mu\)-almost-everywhere measurable.

lemma aemeasurable_postStoppingTimeSeq
    {X : ℕ → Ω → S} {f : Filtration ℕ m} {T : Ω → ℕ}
    (hX_aem : ∀ i, AEMeasurable (X i) μ)
    (hT : IsStoppingTime f (fun ω => (T ω : ℕ∞)))
    (k : ℕ) :
    AEMeasurable (postStoppingTimeSeq X T k) μ

Uses 2 · Used by 1

Statement usesPost-stopping-time sequence

Proof usesLevel sets of a stopping time are measurable

Used byStrong Markov property for i.i.d. sequences: the law after a stopping time

TheoremStrong Markov property for i.i.d. sequences: the law after a stopping time#✓fully proved

Let \(\mu\) be a probability measure on a measurable space \(\Omega\), let \((\mathcal{F}_n)_{n \in \mathbb{N}}\) be a filtration on \(\Omega\), and let \(X_0, X_1, X_2, \dots\) be measurable maps from \(\Omega\) to a measurable space \(S\) that are mutually independent and identically distributed under \(\mu\). Suppose that for every \(n\) the σ-algebra \(\mathcal{F}_n\) is contained in the σ-algebra generated by \(X_0, \dots, X_n\), and let \(T : \Omega \to \mathbb{N}\) be a stopping time for \((\mathcal{F}_n)\). Then for every \(k \in \mathbb{N}\) the map \(\omega \mapsto X_{T(\omega)+k+1}(\omega)\) has the same distribution under \(\mu\) as \(X_0\).

theorem strong_markov_iid_identDistrib
    {X : ℕ → Ω → S} {f : Filtration ℕ m} {T : Ω → ℕ}
    (hX_id : ∀ i j, IdentDistrib (X i) (X j) μ μ)
    (hX_ind : iIndepFun (m := fun _ => ‹MeasurableSpace S›) X μ)
    (hX_meas : ∀ i, Measurable (X i))
    (hT : IsStoppingTime f (fun ω => (T ω : ℕ∞)))
    (hfX : ∀ n, f n ≤ ⨆ i ∈ Finset.range (n + 1), MeasurableSpace.comap (X i) ‹MeasurableSpace S›)
    [IsProbabilityMeasure μ]
    (k : ℕ) :
    IdentDistrib (postStoppingTimeSeq X T k) (X 0) μ μ

Uses 5 · Used by 1

Statement usesPost-stopping-time sequence

Proof usesThe post-stopping-time sequence is a.e. measurable · Shifted terms of an identically distributed sequence · A stopping-time event is independent of a later observation · Level sets of a stopping time are measurable

Used byStrong Markov property for i.i.d. sequences: the post-stopping-time sequence is i.i.d

LemmaA stopping-time event is independent of finitely many later observations#✓fully proved

Let \(\mu\) be a probability measure on a measurable space \(\Omega\), let \((\mathcal{F}_n)_{n \in \mathbb{N}}\) be a filtration on \(\Omega\), and let \(X_0, X_1, X_2, \dots\) be measurable maps from \(\Omega\) to a measurable space \(S\) that are mutually independent under \(\mu\). Suppose that for every \(n\) the σ-algebra \(\mathcal{F}_n\) is contained in the σ-algebra generated by \(X_0, \dots, X_n\), and let \(T : \Omega \to \mathbb{N}\) be a stopping time for \((\mathcal{F}_n)\). Then for every \(n \in \mathbb{N}\), every finite set \(F \subseteq \mathbb{N}\) and all sets \(A_k \subseteq S\) (\(k \in \mathbb{N}\)) such that \(A_k\) is measurable for every \(k \in F\), \(\mu(\{T = n\} \cap \bigcap_{k \in F} X_{n+k+1}^{-1}(A_k)) = \mu(\{T = n\}) \prod_{k \in F} \mu(X_{n+k+1}^{-1}(A_k))\).

lemma indep_stopping_time_tail_finset
    (X : ℕ → Ω → S) (f : Filtration ℕ m) (T : Ω → ℕ)
    (hX_ind : iIndepFun (m := fun _ => ‹MeasurableSpace S›) X μ)
    (hX_meas : ∀ i, Measurable (X i))
    (hT : IsStoppingTime f (fun ω => (T ω : ℕ∞)))
    (hfX : ∀ n, f n ≤ ⨆ i ∈ Finset.range (n + 1), MeasurableSpace.comap (X i) ‹MeasurableSpace S›)
    [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)

Used by 2

Used byStrong Markov property for i.i.d. sequences: independence after a stopping time · Strong Markov property (independence from the past)

LemmaPreimage measures of a post-stopping-time variable#✓fully proved

Let \(\mu\) be a probability measure on a measurable space \(\Omega\), let \((\mathcal{F}_n)_{n \in \mathbb{N}}\) be a filtration on \(\Omega\), and let \(X_0, X_1, X_2, \dots\) be measurable maps from \(\Omega\) to a measurable space \(S\) that are mutually independent and identically distributed under \(\mu\). Suppose that for every \(n\) the σ-algebra \(\mathcal{F}_n\) is contained in the σ-algebra generated by \(X_0, \dots, X_n\), and let \(T : \Omega \to \mathbb{N}\) be a stopping time for \((\mathcal{F}_n)\). Then for every \(k \in \mathbb{N}\) and every measurable set \(A \subseteq S\), \(\mu(\{\omega : X_{T(\omega)+k+1}(\omega) \in A\}) = \mu(X_0^{-1}(A))\).

lemma postStoppingTimeSeq_preimage_eq
    {X : ℕ → Ω → S} {f : Filtration ℕ m} {T : Ω → ℕ}
    (hX_id : ∀ i j, IdentDistrib (X i) (X j) μ μ)
    (hX_ind : iIndepFun (m := fun _ => ‹MeasurableSpace S›) X μ)
    (hX_meas : ∀ i, Measurable (X i))
    (hT : IsStoppingTime f (fun ω => (T ω : ℕ∞)))
    (hfX : ∀ n, f n ≤ ⨆ i ∈ Finset.range (n + 1), MeasurableSpace.comap (X i) ‹MeasurableSpace S›)
    [IsProbabilityMeasure μ]
    (k : ℕ) (A : Set S) (hA : MeasurableSet A) :
    μ ((postStoppingTimeSeq X T k) ⁻¹' A) = μ ((X 0) ⁻¹' A)

Uses 3 · Used by 1

Statement usesPost-stopping-time sequence

Proof usesA stopping-time event is independent of a later observation · Level sets of a stopping time are measurable

Used byStrong Markov property for i.i.d. sequences: independence after a stopping time

TheoremStrong Markov property for i.i.d. sequences: independence after a stopping time#✓fully proved

Let \(\mu\) be a probability measure on a measurable space \(\Omega\), let \((\mathcal{F}_n)_{n \in \mathbb{N}}\) be a filtration on \(\Omega\), and let \(X_0, X_1, X_2, \dots\) be measurable maps from \(\Omega\) to a measurable space \(S\) that are mutually independent and identically distributed under \(\mu\). Suppose that for every \(n\) the σ-algebra \(\mathcal{F}_n\) is contained in the σ-algebra generated by \(X_0, \dots, X_n\), and let \(T : \Omega \to \mathbb{N}\) be a stopping time for \((\mathcal{F}_n)\). Then the maps \(Y_k(\omega) = X_{T(\omega)+k+1}(\omega)\), \(k \in \mathbb{N}\), are mutually independent under \(\mu\).

theorem strong_markov_iid_iIndepFun
    {X : ℕ → Ω → S} {f : Filtration ℕ m} {T : Ω → ℕ}
    (hX_id : ∀ i j, IdentDistrib (X i) (X j) μ μ)
    (hX_ind : iIndepFun (m := fun _ => ‹MeasurableSpace S›) X μ)
    (hX_meas : ∀ i, Measurable (X i))
    (hT : IsStoppingTime f (fun ω => (T ω : ℕ∞)))
    (hfX : ∀ n, f n ≤ ⨆ i ∈ Finset.range (n + 1), MeasurableSpace.comap (X i) ‹MeasurableSpace S›)
    [IsProbabilityMeasure μ] :
    iIndepFun (m := fun _ => ‹MeasurableSpace S›) (postStoppingTimeSeq X T) μ

Uses 4 · Used by 1

Statement usesPost-stopping-time sequence

Proof usesA stopping-time event is independent of finitely many later observations · Level sets of a stopping time are measurable · Preimage measures of a post-stopping-time variable

Used byStrong Markov property for i.i.d. sequences: the post-stopping-time sequence is i.i.d

TheoremStrong Markov property for i.i.d. sequences: the post-stopping-time sequence is i.i.d#✓fully proved

Let \(\mu\) be a probability measure on a measurable space \(\Omega\), let \((\mathcal{F}_n)_{n \in \mathbb{N}}\) be a filtration on \(\Omega\), and let \(X_0, X_1, X_2, \dots\) be measurable maps from \(\Omega\) to a measurable space \(S\) that are mutually independent and identically distributed under \(\mu\). Suppose that for every \(n\) the σ-algebra \(\mathcal{F}_n\) is contained in the σ-algebra generated by \(X_0, \dots, X_n\), and let \(T : \Omega \to \mathbb{N}\) be a stopping time for \((\mathcal{F}_n)\). Then the post-stopping-time sequence \(Y_k(\omega) = X_{T(\omega)+k+1}(\omega)\), \(k \in \mathbb{N}\), is again i.i.d. with the law of \(X_0\): each \(Y_k\) has the same distribution under \(\mu\) as \(X_0\), and \((Y_k)_{k \in \mathbb{N}}\) is mutually independent under \(\mu\).

theorem strong_markov_iid_postStoppingTimeSeq
    {X : ℕ → Ω → S} {f : Filtration ℕ m} {T : Ω → ℕ}
    (hX_id : ∀ i j, IdentDistrib (X i) (X j) μ μ)
    (hX_ind : iIndepFun (m := fun _ => ‹MeasurableSpace S›) X μ)
    (hX_meas : ∀ i, Measurable (X i))
    (hT : IsStoppingTime f (fun ω => (T ω : ℕ∞)))
    (hfX : ∀ n, f n ≤ ⨆ i ∈ Finset.range (n + 1), MeasurableSpace.comap (X i) ‹MeasurableSpace S›)
    [IsProbabilityMeasure μ] :
    (∀ k, IdentDistrib (postStoppingTimeSeq X T k) (X 0) μ μ) ∧
    iIndepFun (m := fun _ => ‹MeasurableSpace S›) (postStoppingTimeSeq X T) μ

Uses 3

Statement usesPost-stopping-time sequence

Proof usesStrong Markov property for i.i.d. sequences: independence after a stopping time · Strong Markov property for i.i.d. sequences: the law after a stopping time

TheoremStrong Markov property (independence from the past)#✓fully proved

Let \(X_0, X_1, \dots\) be measurable random variables on a probability space \((\Omega, \mu)\) with values in a measurable space \(S\), mutually independent and all with the same distribution. Let \((\mathcal F_n)_{n \ge 0}\) be a filtration with \(\mathcal F_n \subseteq \sigma(X_0, \dots, X_n)\) for every \(n\), and let \(T : \Omega \to \mathbb N\) be a stopping time for \((\mathcal F_n)\), finite everywhere. Then the stopped σ-algebra \(\mathcal F_T\) is independent of the σ-algebra generated by the post-stopping-time sequence \((X_{T+k+1})_{k \ge 0}\).

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

Uses 3

Statement usesPost-stopping-time sequence

Proof usesA stopping-time event is independent of finitely many later observations · Level sets of a stopping time are measurable

11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.