Theorems · Definition · probability

ProbabilityTheory.IndepFun

{Ω : Type u_1} →
  {β : Type u_6} →
    {γ : Type u_7} →
      {_mΩ : MeasurableSpace Ω} →
        [MeasurableSpace β] →
          [MeasurableSpace γ] →
            (Ω → β) → (Ω → γ) → autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.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. We use the notation f ⟂ᵢ[μ] g for IndepFun f g μ (scoped in ProbabilityTheory).

Defined in

Mathlib.Probability.Independence.Basic

Cited by

192 results in Mathlib

Foundations

Depth 179 from the axioms, rests on 4,717 definitions · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceMeasurableSpace