Theorems · Definition · probability

ProbabilityTheory.Kernel.iIndepSets

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

A family of sets of sets π : ι → Set (Set Ω) is independent with respect to a kernel κ and a measure μ if for any finite set of indices s = {i_1, ..., i_n}, for any sets f i_1 ∈ π i_1, ..., f i_n ∈ π i_n, then ∀ᵐ a ∂μ, κ a (⋂ i in s, f i) = ∏ i ∈ s, κ a (f i). It will be used for families of π-systems.

Defined in

Mathlib.Probability.Independence.Kernel.Indep

Cited by

21 results in Mathlib

Foundations

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