English
The nth moment of truncation(f,A) equals the interval integral of y^n with respect to map f μ.
Русский
nth момент усечения равен интегралу по интервалу от y^n относительно отображённой меры map f μ.
LaTeX
$$$\int x\,(\operatorname{truncation}(f,A)(x))^n \mathrm{d}\mu(x) = \int_{-A}^{A} y^n \, \mathrm{d}(\mathrm{map} \, f \mu)(y)$$$
Lean4
theorem moment_truncation_eq_intervalIntegral (hf : AEStronglyMeasurable f μ) {A : ℝ} (hA : 0 ≤ A) {n : ℕ}
(hn : n ≠ 0) : ∫ x, truncation f A x ^ n ∂μ = ∫ y in -A..A, y ^ n ∂Measure.map f μ :=
by
have M : MeasurableSet (Set.Ioc (-A) A) := measurableSet_Ioc
change ∫ x, (fun z => indicator (Set.Ioc (-A) A) id z ^ n) (f x) ∂μ = _
rw [← integral_map (f := fun z => _ ^ n) hf.aemeasurable, intervalIntegral.integral_of_le, ← integral_indicator M]
· simp only [indicator, zero_pow hn, id, ite_pow]
· linarith
· exact ((measurable_id.indicator M).pow_const n).aestronglyMeasurable
