English
If f ≥ 0, then for n ≠ 0, the nth moment of truncation equals the interval integral over 0..A.
Русский
Если f ≥ 0, то для n ≠ 0 момент усечения равен интегралу по 0..A.
LaTeX
$$$\int x\, (\operatorname{truncation}(f,A)(x))^n \mathrm{d}\mu(x) = \int_{0}^{A} y^n \, d(\mathrm{map} \, f \mu)(y)$, при $f\ge 0$ и $n\neq 0$$$
Lean4
theorem moment_truncation_eq_intervalIntegral_of_nonneg (hf : AEStronglyMeasurable f μ) {A : ℝ} {n : ℕ} (hn : n ≠ 0)
(h'f : 0 ≤ f) : ∫ x, truncation f A x ^ n ∂μ = ∫ y in 0..A, y ^ n ∂Measure.map f μ :=
by
have M : MeasurableSet (Set.Ioc 0 A) := measurableSet_Ioc
have M' : MeasurableSet (Set.Ioc A 0) := measurableSet_Ioc
rw [truncation_eq_of_nonneg h'f]
change ∫ x, (fun z => indicator (Set.Ioc 0 A) id z ^ n) (f x) ∂μ = _
rcases le_or_gt 0 A with (hA | hA)
· rw [← integral_map (f := fun z => _ ^ n) hf.aemeasurable, intervalIntegral.integral_of_le hA, ←
integral_indicator M]
· simp only [indicator, zero_pow hn, id, ite_pow]
· exact ((measurable_id.indicator M).pow_const n).aestronglyMeasurable
· rw [← integral_map (f := fun z => _ ^ n) hf.aemeasurable, intervalIntegral.integral_of_ge hA.le, ←
integral_indicator M']
· simp only [Set.Ioc_eq_empty_of_le hA.le, zero_pow hn, Set.indicator_empty, integral_zero, zero_eq_neg]
apply integral_eq_zero_of_ae
have : ∀ᵐ x ∂Measure.map f μ, (0 : ℝ) ≤ x :=
(ae_map_iff hf.aemeasurable measurableSet_Ici).2 (Eventually.of_forall h'f)
filter_upwards [this] with x hx
simp only [indicator, Set.mem_Ioc, Pi.zero_apply, ite_eq_right_iff, and_imp]
intro _ h''x
have : x = 0 := by linarith
simp [this, zero_pow hn]
· exact ((measurable_id.indicator M).pow_const n).aestronglyMeasurable
