Theorems · Theorem · probability

ProbabilityTheory.lintegral_mul_indicator_eq_lintegral_mul_lintegral_indicator

∀ {Ω : Type u_1} {f : Ω → ENNReal} {Mf mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω},
  Mf ≤ mΩ →
    ∀ (c : ENNReal) {T : Set Ω},
      MeasurableSet T →
        ProbabilityTheory.IndepSets {s | MeasurableSet s} {T} μ →
          Measurable f →
            ∫⁻ (ω : Ω), f ω * T.indicator (fun x => c) ω ∂μ =
              (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x => c) ω ∂μ

If a random variable f in ℝ≥0∞ is independent of an event T, then if you restrict the random variable to T, then E[f * indicator T c 0]=E[f] * E[indicator T c 0]. It is useful for lintegral_mul_eq_lintegral_mul_lintegral_of_independent_measurableSpace.

Defined in

Mathlib.Probability.Independence.Integration

Cited by

1 results in Mathlib

Foundations

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