Theorems · Definition · probability

ProbabilityTheory.CondIndepSets

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

Two sets of sets s₁, s₂ are conditionally independent given m' with respect to a measure μ if for any sets t₁ ∈ s₁, t₂ ∈ s₂, then μ⟦t₁ ∩ t₂ | m'⟧ =ᵐ[μ] μ⟦t₁ | m'⟧ * μ⟦t₂ | m'⟧. See ProbabilityTheory.condIndepSets_iff.

Defined in

Mathlib.Probability.Independence.Conditional

Cited by

21 results in Mathlib

Foundations

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

Assumes

StandardBorelSpaceMeasureTheory.IsFiniteMeasure