Theorems · Theorem · probability

ProbabilityTheory.condIndepFun_iff_map_prod_eq_prod_comp_trim

∀ {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {f : Ω → β} {g : Ω → β'}
  {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'},
  Measurable f →
    Measurable g →
      (ProbabilityTheory.CondIndepFun m' hm' f g μ ↔
        MeasureTheory.Measure.map (fun ω => (ω, f ω, g ω)) μ =
          (μ.trim hm').bind
            ⇑(ProbabilityTheory.Kernel.id.prod
                (((ProbabilityTheory.condExpKernel μ m').map f).prod ((ProbabilityTheory.condExpKernel μ m').map g))))

Two random variables are conditionally independent with respect to m' iff the law of (id, f, g) under μ, in which the identity is to the space with σ-algebra m', can be written as a product involving the conditional expectations of f and g given m'. For a random variable f, (condExpKernel μ m').map f is the law of the conditional expectation of f given m': almost surely, (condExpKernel μ m').map f ω s = μ⟦f ⁻¹' s | m'⟧ ω.

Defined in

Mathlib.Probability.Independence.Conditional

Cited by

1 results in Mathlib

Foundations

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

Assumes

StandardBorelSpaceMeasureTheory.IsFiniteMeasure