integral_apply — Mathlib

English

Let f map into continuous functions Y → E, i.e., f: X → C(Y,E), with f integrable. Then evaluating the Bochner integral at y ∈ Y is the integral of the evaluations: (∫ f) (y) = ∫ f(·)(y) dμ.

Русский

Пусть f: X → C(Y,E) интегрируема; тогда значение интеграла в точке y равно интегралу значений: (∫ f)(y) = ∫ f(x)(y) dμ.

LaTeX

$$$\\left(\\int_X f(x)\\,d\\mu\\right)(y) = \\int_X f(x)(y)\\,d\\mu \\,.$$$

Lean4

theorem integral_apply {R : Type*} [NormedCommRing R] [Zero Y] [NormedAlgebra ℝ R] [CompleteSpace R] {f : X → C(Y, R)₀}
    (hf : MeasureTheory.Integrable f μ) (y : Y) : (∫ (x : X), f x ∂μ) y = ∫ (x : X), (f x) y ∂μ := by
  calc
    (∫ x, f x ∂μ) y = ContinuousMapZero.evalCLM ℝ y (∫ x, f x ∂μ) := rfl
    _ = ∫ x, ContinuousMapZero.evalCLM ℝ y (f x) ∂μ := (ContinuousLinearMap.integral_comp_comm _ hf).symm
    _ = _ := rfl

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