Theorems · Theorem · probability

ProbabilityTheory.iCondIndepSet.condIndep_generateFrom_le_nat

∀ {Ω : Type u_1} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω}
  [inst_1 : MeasureTheory.IsFiniteMeasure μ] {s : ℕ → Set Ω},
  (∀ (n : ℕ), MeasurableSet (s n)) →
    ProbabilityTheory.iCondIndepSet m' hm' s μ →
      ∀ (n : ℕ),
        ProbabilityTheory.CondIndep m' (MeasurableSpace.generateFrom {s (n + 1)})
          (MeasurableSpace.generateFrom {t | ∃ k ≤ n, s k = t}) hm' μ

Defined in

Mathlib.Probability.Independence.Conditional

Cited by

0 results in Mathlib

Foundations

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

Assumes

StandardBorelSpaceMeasureTheory.IsFiniteMeasure