Theorems · Definition · probability

ProbabilityTheory.Kernel.IndepFun

{α : Type u_1} →
  {Ω : Type u_2} →
    {β : Type u_4} →
      {γ : Type u_6} →
        {mα : MeasurableSpace α} →
          {mΩ : MeasurableSpace Ω} →
            [mβ : MeasurableSpace β] →
              [mγ : MeasurableSpace γ] →
                (Ω → β) →
                  (Ω → γ) →
                    ProbabilityTheory.Kernel α Ω →
                      autoParam (MeasureTheory.Measure α) ProbabilityTheory.Kernel.IndepFun._auto_1 → Prop

Two functions are independent if the two measurable space structures they generate are independent. For a function f with codomain having measurable space structure m, the generated measurable space structure is MeasurableSpace.comap f m.

Defined in

Mathlib.Probability.Independence.Kernel.IndepFun

Cited by

70 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpace