English
Let I be a finite index set and (F_i) be inner product spaces. In the Hilbert space ⊕_{i∈I} F_i equipped with the L2 inner product, the inner product of two elements x = (x_i) and y = (y_i) is the sum of the coordinate inner products: ⟪x,y⟫ = ∑_{i∈I} ⟪x_i, y_i⟫.
Русский
Пусть I — конечное множество индексов, и для каждого i∈I задано скалярное произведение на F_i. В гильбертовом пространстве ⊕_{i∈I} F_i с интегрированным по L2 скалярным произведением скалярное произведение двух векторов x=(x_i) и y=(y_i) равно сумме скалярных произведений по компонентам: ⟪x,y⟫ = ∑_{i∈I} ⟪x_i, y_i⟫.
LaTeX
$$$\langle x,y\rangle = \sum_{i} \langle x_i, y_i\rangle$$$
Lean4
theorem inner_apply {ι : Type*} [Fintype ι] {f : ι → Type*} [∀ i, NormedAddCommGroup (f i)]
[∀ i, InnerProductSpace 𝕜 (f i)] (x y : PiLp 2 f) : ⟪x, y⟫ = ∑ i, ⟪x i, y i⟫ :=
rfl
