integral_comp_comm — Mathlib

English

Let L be a linear isometry L: E → 𝕜 F, φ: X → E be integrable. Then the integral commutes with L: ∫_X L(φ(x)) dμ = L(∫_X φ(x) dμ).

Русский

Пусть L — линейная изометрия L: E → F, φ: X → E интегрируема. Тогда интеграл и применение L взаимно переставляются: ∫_X L(φ(x)) dμ = L(∫_X φ(x) dμ).

LaTeX

$$$\\int_X L(\\phi(x))\\,d\\mu = L\\left(\\int_X \\phi(x)\\,d\\mu\\right)$$$

Lean4

theorem integral_comp_comm (L : E →ₗᵢ[𝕜] F) (φ : X → E) : ∫ x, L (φ x) ∂μ = L (∫ x, φ x ∂μ) :=
  L.toContinuousLinearMap.integral_comp_comm' L.antilipschitz _

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