Theorems · Theorem · probability

ProbabilityTheory.Indep.setIntegral_eq_mul

∀ {Ω : Type u_5} {𝓧 : Type u_6} {m mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [m𝓧 : MeasurableSpace 𝓧]
  {X : Ω → 𝓧} {A : Set Ω},
  m ≤ mΩ →
    ∀ {f : 𝓧 → ℝ},
      ProbabilityTheory.Indep m (MeasurableSpace.comap X m𝓧) P →
        AEMeasurable X P →
          MeasurableSet A →
            MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map X P) →
              ∫ (ω : Ω) in A, f (X ω) ∂P = P.real A * ∫ (ω : Ω), f (X ω) ∂P

If a random variable X is independent of a sigma-algebra m and A is a set in m then ∫ ω in A, f (X ω) ∂P = P.real A * ∫ ω, f (X ω) ∂P for a measurable function f : 𝓧 → ℝ.

Defined in

Mathlib.Probability.Independence.Integration

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpace