integral_comp_comm — Mathlib

English

The integral of a composed map L ∘ φ equals the integral of φ mapped by L when φ is integrable.

Русский

Интеграл от композиции L ∘ φ равен интегралу φ под действием L при интегрируемости φ.

LaTeX

$$$\\int L(φ(x)) \\, dμ = L(\\int φ(x) \\, dμ)$$$

Lean4

theorem integral_comp_comm [CompleteSpace E] (L : E →L[𝕜] Fₗ) {φ : X → E} (φ_int : Integrable φ μ) :
    ∫ x, L (φ x) ∂μ = L (∫ x, φ x ∂μ) :=
  integral_comp_commSL (by simp) L φ_int

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