Theorems · Theorem · probability

ProbabilityTheory.Kernel.trajContent_tendsto_zero

∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {A : ℕ → Set ((n : ℕ) → X n)},
  (∀ (n : ℕ), A n ∈ MeasureTheory.measurableCylinders X) →
    Antitone A →
      ⋂ n, A n = ∅ →
        ∀ {p : ℕ} (x₀ : (i : ↥(Finset.Iic p)) → X ↑i),
          Filter.Tendsto (fun n => (ProbabilityTheory.Kernel.trajContent κ x₀) (A n)) Filter.atTop (nhds 0)

This is the key theorem to prove the existence of the traj: the trajContent of a decreasing sequence of cylinders with empty intersection converges to 0. This implies the σ-additivity of trajContent (see addContent_iUnion_eq_sum_of_tendsto_zero), which allows to extend it to the σ-algebra by Carathéodory's theorem.

Defined in

Mathlib.Probability.Kernel.IonescuTulcea.Traj

Cited by

1 results in Mathlib

Foundations

Depth 264 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceProbabilityTheory.IsMarkovKernel