integral_truncation_eq_intervalIntegral

English

The integral of truncation f A equals the interval integral over [-A,A] of y with respect to the map measure.

Русский

Интеграл усечения равен интегралу по [-A,A] от y к мере map f μ.

LaTeX

$$$\int x\, \operatorname{truncation}(f,A)(x)\,d\mu(x) = \int_{-A}^{A} y \, d(\mathrm{map} \, f \mu)(y)$$$

Lean4

theorem integral_truncation_eq_intervalIntegral (hf : AEStronglyMeasurable f μ) {A : ℝ} (hA : 0 ≤ A) :
    ∫ x, truncation f A x ∂μ = ∫ y in -A..A, y ∂Measure.map f μ := by
  simpa using moment_truncation_eq_intervalIntegral hf hA one_ne_zero

Похожие утверждения