Theorems · Theorem · probability

ProbabilityTheory.condIndepFun_iff

∀ {Ω : Type u_1} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] (hm' : m' ≤ mΩ)
  {β : Type u_3} {γ : Type u_4} [mβ : MeasurableSpace β] [mγ : MeasurableSpace γ] (f : Ω → β) (g : Ω → γ),
  Measurable f →
    Measurable g →
      ∀ (μ : MeasureTheory.Measure Ω) [inst_1 : MeasureTheory.IsFiniteMeasure μ],
        ProbabilityTheory.CondIndepFun m' hm' f g μ ↔
          ∀ (t1 t2 : Set Ω),
            MeasurableSet t1 →
              MeasurableSet t2 →
                μ[(t1 ∩ t2).indicator fun ω => 1 | m'] =ᵐ[μ]
                  μ[t1.indicator fun ω => 1 | m'] * μ[t2.indicator fun ω => 1 | m']

Defined in

Mathlib.Probability.Independence.Conditional

Cited by

2 results in Mathlib

Foundations

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

Assumes

StandardBorelSpaceMeasurableSpaceMeasurableSpaceMeasureTheory.IsFiniteMeasure