integralCLM_apply — Mathlib

English

Let μ be a measure and f a Schwartz map f: D → V. Then the continuous linear integration of f with respect to μ equals the Bochner (Lebesgue) integral of f: integralCLM 𝕜 μ f = ∫ x f(x) ∂μ.

Русский

Пусть μ — мера на D, а f: D → V — отображение Шварца. Тогда непрерывно-линейный интеграл по μ совпадает с интегралом Бо́хнера: integralCLM 𝕜 μ f = ∫ x f(x) dμ.

LaTeX

$$$$ \\mathrm{integralCLM}_{\\mathbb{k}}(\\mu, f) = \\int x\, f(x) \\, \\partial\\mu.$$$$

Lean4

@[simp]
theorem integralCLM_apply (f : 𝓢(D, V)) : integralCLM 𝕜 μ f = ∫ x, f x ∂μ := by rfl

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