hasSum_inner — Mathlib

English

Fix an index i and a vector a ∈ G_i. Then the inner product with lp.single 2 i a reduces to the coordinate inner product: ⟪lp.single 2 i a, f⟫ = ⟪a, f(i)⟫.

Русский

Фиксируем индекс i и вектор a ∈ G_i. Тогда скалярное произведение с lp.single 2 i a сводится к поперечному произведению по координатам: ⟪lp.single 2 i a, f⟫ = ⟪a, f(i)⟫.

LaTeX

$$$ \\langle lp.single \\\\ 2 i a, f \\rangle = \\langle a, f(i) \\rangle $$$

Lean4

theorem hasSum_inner (f g : lp G 2) : HasSum (fun i => ⟪f i, g i⟫) ⟪f, g⟫ :=
  (summable_inner f g).hasSum

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