Theorems · Definition · probability

ProbabilityTheory.Kernel.iIndep

{α : Type u_1} →
  {Ω : Type u_2} →
    {ι : Type u_3} →
      {_mα : MeasurableSpace α} →
        (ι → MeasurableSpace Ω) →
          {_mΩ : MeasurableSpace Ω} →
            ProbabilityTheory.Kernel α Ω →
              autoParam (MeasureTheory.Measure α) ProbabilityTheory.Kernel.iIndep._auto_1 → Prop

A family of measurable space structures (i.e. of σ-algebras) is independent with respect to a kernel κ and a measure μ if the family of sets of measurable sets they define is independent.

Defined in

Mathlib.Probability.Independence.Kernel.Indep

Cited by

33 results in Mathlib

Foundations

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