Theorems · Theorem · probability

ProbabilityTheory.Kernel.indepSet_iff_measure_inter_eq_mul

∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {s t : Set Ω} {_m0 : MeasurableSpace Ω},
  MeasurableSet s →
    MeasurableSet t →
      ∀ (κ : ProbabilityTheory.Kernel α Ω) (μ : MeasureTheory.Measure α) [ProbabilityTheory.IsZeroOrMarkovKernel κ],
        ProbabilityTheory.Kernel.IndepSet s t κ μ ↔ ∀ᵐ (a : α) ∂μ, (κ a) (s ∩ t) = (κ a) s * (κ a) t

Defined in

Mathlib.Probability.Independence.Kernel.Indep

Cited by

2 results in Mathlib

Foundations

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

Assumes

ProbabilityTheory.IsZeroOrMarkovKernel