Theorems · Definition · probability

ProbabilityTheory.CondIndep

{Ω : Type u_1} →
  (m' : MeasurableSpace Ω) →
    MeasurableSpace Ω →
      MeasurableSpace Ω →
        {mΩ : MeasurableSpace Ω} →
          [StandardBorelSpace Ω] →
            m' ≤ mΩ →
              (μ : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.CondIndep._auto_1) →
                [MeasureTheory.IsFiniteMeasure μ] → Prop

Two measurable space structures (or σ-algebras) m₁, m₂ are conditionally independent given m' with respect to a measure μ (defined on a third σ-algebra) if for any sets t₁ ∈ m₁, t₂ ∈ m₂, μ⟦t₁ ∩ t₂ | m'⟧ =ᵐ[μ] μ⟦t₁ | m'⟧ * μ⟦t₂ | m'⟧. See ProbabilityTheory.condIndep_iff.

Defined in

Mathlib.Probability.Independence.Conditional

Cited by

30 results in Mathlib

Foundations

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

Assumes

StandardBorelSpaceMeasureTheory.IsFiniteMeasure