Theorems · Theorem · probability

ProbabilityTheory.Kernel.IndepSets.indep_aux

∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {m₂ m : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω}
  {μ : MeasureTheory.Measure α} [ProbabilityTheory.IsZeroOrMarkovKernel κ] {p1 p2 : Set (Set Ω)},
  m₂ ≤ m →
    IsPiSystem p2 →
      m₂ = MeasurableSpace.generateFrom p2 →
        ProbabilityTheory.Kernel.IndepSets p1 p2 κ μ →
          ∀ {t1 t2 : Set Ω},
            t1 ∈ p1 → MeasurableSet t1 → MeasurableSet t2 → ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Defined in

Mathlib.Probability.Independence.Kernel.Indep

Cited by

1 results in Mathlib

Foundations

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

Assumes

ProbabilityTheory.IsZeroOrMarkovKernel