inner_const — Mathlib

English

If f is integrable, then for any fixed vector c, the integral of ⟪c, f(x)⟫ equals ⟪c, ∫ f(x) dx⟫.

Русский

Если f интегрируемо, то для любого фиксированного вектора c выполняется равенство интеграла ⟪c, f(x)⟫ равен ⟪c, ∫ f(x) dx⟫.

LaTeX

$$$ \\int x, \\langle c, f(x)\\rangle \\partial\\mu = \\langle c, \\int x, f(x) \\partial\\mu \\rangle $$$

Lean4

@[fun_prop]
theorem inner_const (hf : Integrable f μ) (c : E) : Integrable (fun x => ⟪f x, c⟫) μ := by
  rw [← memLp_one_iff_integrable] at hf ⊢; exact hf.inner_const c

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