integral_apply — Mathlib

English

The integral of a semilinear map preserves integral under compatible scalar embeddings.

Русский

Интеграл сохраняется под совместной линейной структурой через совместимые отображения скаляров.

LaTeX

$$$\\int φ = φ(\\int) $$$

Lean4

theorem integral_apply {H : Type*} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {φ : X → H →L[𝕜] E} (φ_int : Integrable φ μ)
    (v : H) : (∫ x, φ x ∂μ) v = ∫ x, φ x v ∂μ :=
  by
  by_cases hE : CompleteSpace E
  · exact ((ContinuousLinearMap.apply 𝕜 E v).integral_comp_comm φ_int).symm
  · rcases subsingleton_or_nontrivial H with hH | hH
    · simp [Subsingleton.eq_zero v]
    · have : ¬(CompleteSpace (H →L[𝕜] E)) := by rwa [SeparatingDual.completeSpace_continuousLinearMap_iff]
      simp [integral, hE, this]

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