integral_comp_comm — Mathlib

English

Let L be a continuous linear equivalence E ≃L[𝕜] F. Then the Bochner integral commutes with L: ∫_X L(φ(x)) dμ = L(∫_X φ(x) dμ).

Русский

Пусть L — непрерывно-обратимое линейное эквивалентное отображение E ≃ L[𝕜] F. Тогда интеграл отвергнутого отображения коммутирует с 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 ≃L[𝕜] F) (φ : X → E) : ∫ x, L (φ x) ∂μ = L (∫ x, φ x ∂μ) :=
  by
  have : CompleteSpace E ↔ CompleteSpace F := completeSpace_congr (e := L.toEquiv) L.isUniformEmbedding
  obtain ⟨_, _⟩ | ⟨_, _⟩ := iff_iff_and_or_not_and_not.mp this
  · exact L.toContinuousLinearMap.integral_comp_comm' L.antilipschitz _
  · simp [integral, *]

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