inner product space structure on products of inner product spaces #

The norm on product of two inner product spaces is compatible with an inner product $$ \langle x, y\rangle = \langle x_1, y_1 \rangle + \langle x_2, y_2 \rangle. $$ This is recorded in this file as an inner product space instance on WithLp 2 (E × F).

noncomputable instance WithLp.instProdInnerProductSpace {𝕜 : Type u_1} (E : Type u_2) (F : Type u_3) [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] :
InnerProductSpace 𝕜 (WithLp 2 (E × F))
  • One or more equations did not get rendered due to their size.
theorem WithLp.prod_inner_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (x : WithLp 2 (E × F)) (y : WithLp 2 (E × F)) :
inner x y = inner x.1 y.1 + inner x.2 y.2