integral_apply — Mathlib

English

For a linear isometry L: E → F and φ: X → E integrable, the integrals satisfy ∫_X L(φ(x)) dμ = L(∫_X φ(x) dμ).

Русский

Для линейной изометрии L: E → F и интегрируемой φ: X → E выполняется ∫_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_apply [NormedSpace ℝ E] [CompleteSpace E] {f : X → C(Y, E)} (hf : Integrable f μ) (y : Y) :
    (∫ x, f x ∂μ) y = ∫ x, f x y ∂μ := by
  calc
    (∫ x, f x ∂μ) y = ContinuousMap.evalCLM ℝ y (∫ x, f x ∂μ) := rfl
    _ = ∫ x, ContinuousMap.evalCLM ℝ y (f x) ∂μ := (ContinuousLinearMap.integral_comp_comm _ hf).symm
    _ = _ := rfl

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