integral_comp_L1_comm — Mathlib

English

Let L be a bounded linear map from E to F under 𝕜, and φ be an integrable function from X to E with respect to μ. Then applying L before integration yields the same as integrating first and then applying L: ∫_X L(φ(x)) dμ = L(∫_X φ(x) dμ).

Русский

Пусть L: E → F — ограниченное линейное отображение над 𝕜, и φ: X → E интегрируема по μ. Тогда применения L до интеграла та же операция, что и интеграл после применения 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_L1_comm (L : E →L[𝕜] Fₗ) (φ : X →₁[μ] E) : ∫ x, L (φ x) ∂μ = L (∫ x, φ x ∂μ) :=
  L.integral_comp_comm (L1.integrable_coeFn φ)

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