English
Let φ be a function from ℝ to continuous linear maps F →L[𝕜] E such that φ is interval-integrable on [a, b]. Then for every v ∈ F, the action of the operator-valued integral on v equals the scalar integral of φ(x) applied to v; i.e., (∫_a^b φ(x) dμ)(v) = ∫_a^b φ(x)(v) dμ.
Русский
Пусть φ: ℝ → (F →L[𝕜] E) -- функция, принимающая каждое число x в непрерывно линейное отображение, и пусть φ интеґрируема по промежутку [a, b]. Тогда для любого v ∈ F верно, что применение интеграла к v равно интегралу по x: (∫_a^b φ(x) dμ)(v) = ∫_a^b φ(x)(v) dμ.
LaTeX
$$$$\left(\int_{a}^{b} \phi(x) \, d\mu\right)(v) = \int_{a}^{b} \phi(x)(v) \, d\mu.$$$$
Lean4
theorem _root_.ContinuousLinearMap.intervalIntegral_apply {a b : ℝ} {φ : ℝ → F →L[𝕜] E}
(hφ : IntervalIntegrable φ μ a b) (v : F) : (∫ x in a..b, φ x ∂μ) v = ∫ x in a..b, φ x v ∂μ := by
simp_rw [intervalIntegral_eq_integral_uIoc, ← integral_apply hφ.def' v, coe_smul', Pi.smul_apply]
