hasSum_linearIsometry

Mathlib.Analysis.InnerProductSpace.l2Space

URI: https://scilib.ai/kg/mathlib#OrthogonalFamily.hasSum_linearIsometry

English

If i ∈ ι and a ∈ G_i, then hV.linearIsometry(lp.single 2 i a) = V_i(a).

Русский

Если i ∈ ι и a ∈ G_i, то hV.linearIsometry(lp.single 2 i a) = V_i(a).

LaTeX

$$$ hV.linearIsometry(\\,lp.single 2 i a\\,) = V_i(a) $$$

Lean4

protected theorem hasSum_linearIsometry (f : lp G 2) : HasSum (fun i => V i (f i)) (hV.linearIsometry f) :=
  (hV.summable_of_lp f).hasSum

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru