English
The space WithLp 2 of the product E×F carries the natural inner product defined by the sum of the inner products on E and on F: ⟪(x1,x2),(y1,y2)⟫ = ⟪x1,y1⟫ + ⟪x2,y2⟫.
Русский
Пространство WithLp 2 от произведения E×F имеет естественное скалярное произведение: ⟪(x1,x2),(y1,y2)⟫ = ⟪x1,y1⟫ + ⟪x2,y2⟫.
LaTeX
$$$\langle x,y\rangle_{𝕜} = \langle x_{.1}, y_{.1}\rangle_{𝕜} + \langle x_{.2}, y_{.2}\rangle_{𝕜}$$$
Lean4
noncomputable instance instProdInnerProductSpace : InnerProductSpace 𝕜 (WithLp 2 (E × F))
where
inner x y := ⟪x.fst, y.fst⟫_𝕜 + ⟪x.snd, y.snd⟫_𝕜
norm_sq_eq_re_inner x := by simp [prod_norm_sq_eq_of_L2, ← norm_sq_eq_re_inner]
conj_inner_symm x y := by simp
add_left x y
z := by
simp only [add_fst, add_snd, inner_add_left]
ring
smul_left x y
r := by
simp only [smul_fst, inner_smul_left, smul_snd]
ring
