L² inner product space structure on products of inner product spaces #
The L² 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))
Equations
- One or more equations did not get rendered due to their size.
@[simp]
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))
: