Theorems · Theorem · probability

ProbabilityTheory.moment_truncation_eq_intervalIntegral

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

Defined in

Mathlib.Probability.StrongLaw

Cited by

1 results in Mathlib

Foundations

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