integral_inner — Mathlib

English

If f is integrable and all inner products with any vector c have zero integral, then the integral of f is zero.

Русский

Если f интегрируемо и для каждого вектора c все внутренние произведения интегрируются в нуль, то интеграл f равен нулю.

LaTeX

$$$ \\operatorname{Integrable}(f,\\mu) \\rightarrow (\\forall c, \\int x, \\langle c, f(x)\\rangle \\partial\\mu = 0) \\Rightarrow \\int x, f(x)\\partial\\mu = 0$$$

Lean4

theorem _root_.integral_inner {f : α → E} (hf : Integrable f μ) (c : E) : ∫ x, ⟪c, f x⟫ ∂μ = ⟪c, ∫ x, f x ∂μ⟫ :=
  ((innerSL 𝕜 c).restrictScalars ℝ).integral_comp_comm hf

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