Theorems · Definition · probability

ProbabilityTheory.Kernel.iIndepFun

{α : Type u_1} →
  {Ω : Type u_2} →
    {ι : Type u_3} →
      {mα : MeasurableSpace α} →
        {mΩ : MeasurableSpace Ω} →
          {β : ι → Type u_8} →
            [m : (x : ι) → MeasurableSpace (β x)] →
              ((x : ι) → Ω → β x) →
                ProbabilityTheory.Kernel α Ω →
                  autoParam (MeasureTheory.Measure α) ProbabilityTheory.Kernel.iIndepFun._auto_1 → Prop

A family of functions defined on the same space Ω and taking values in possibly different spaces, each with a measurable space structure, is independent if the family of measurable space structures they generate on Ω is independent. For a function g with codomain having measurable space structure m, the generated measurable space structure is MeasurableSpace.comap g m.

Defined in

Mathlib.Probability.Independence.Kernel.IndepFun

Cited by

65 results in Mathlib

Foundations

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

Assumes

MeasurableSpace