Theorems · Theorem · probability

ProbabilityTheory.integral_truncation_eq_intervalIntegral

∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  MeasureTheory.AEStronglyMeasurable f μ →
    ∀ {A : ℝ},
      0 ≤ A → ∫ (x : α), ProbabilityTheory.truncation f A x ∂μ = ∫ (y : ℝ) in -A..A, y ∂MeasureTheory.Measure.map f μ

Defined in

Mathlib.Probability.StrongLaw

Cited by

0 results in Mathlib

Foundations

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