Theorems · Theorem · probability

ProbabilityTheory.cond_iInter

∀ {ι : Type u_6} {Ω : Type u_7} {α : Type u_8} {β : Type u_9} {mΩ : MeasurableSpace Ω} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → α} {Y : ι → Ω → β} {f : ι → Set Ω} {t : ι → Set β}
  {s : Finset ι} [Finite ι],
  (∀ (i : ι), Measurable (Y i)) →
    ProbabilityTheory.iIndepFun (fun i ω => (X i ω, Y i ω)) μ →
      (∀ i ∈ s, MeasurableSet (f i)) →
        (∀ i ∉ s, μ (Y i ⁻¹' t i) ≠ 0) →
          (∀ (i : ι), MeasurableSet (t i)) → μ[⋂ i ∈ s, f i | ⋂ i, Y i ⁻¹' t i] = ∏ i ∈ s, μ[f i | Y i ⁻¹' t i]

The probability of an intersection of preimages conditioning on another intersection factors into a product.

Defined in

Mathlib.Probability.Independence.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

Finite