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_4)
(F : Type u_5)
[RCLike 𝕜]
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
[NormedAddCommGroup F]
[InnerProductSpace 𝕜 F]
:
InnerProductSpace 𝕜 (WithLp 2 (E × F))
Equations
- WithLp.instProdInnerProductSpace E F = InnerProductSpace.mk ⋯ ⋯ ⋯ ⋯
@[simp]
theorem
WithLp.prod_inner_apply
{𝕜 : Type u_1}
{E : Type u_4}
{F : Type u_5}
[RCLike 𝕜]
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
[NormedAddCommGroup F]
[InnerProductSpace 𝕜 F]
(x y : WithLp 2 (E × F))
:
def
OrthonormalBasis.prod
{𝕜 : Type u_1}
{ι₁ : Type u_2}
{ι₂ : Type u_3}
{E : Type u_4}
{F : Type u_5}
[RCLike 𝕜]
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
[NormedAddCommGroup F]
[InnerProductSpace 𝕜 F]
[Fintype ι₁]
[Fintype ι₂]
(v : OrthonormalBasis ι₁ 𝕜 E)
(w : OrthonormalBasis ι₂ 𝕜 F)
:
OrthonormalBasis (ι₁ ⊕ ι₂) 𝕜 (WithLp 2 (E × F))
The product of two orthonormal bases is a basis for the L2-product.
Equations
- v.prod w = ((v.toBasis.prod w.toBasis).map (WithLp.linearEquiv 2 𝕜 (E × F)).symm).toOrthonormalBasis ⋯
Instances For
@[simp]
theorem
OrthonormalBasis.prod_apply
{𝕜 : Type u_1}
{ι₁ : Type u_2}
{ι₂ : Type u_3}
{E : Type u_4}
{F : Type u_5}
[RCLike 𝕜]
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
[NormedAddCommGroup F]
[InnerProductSpace 𝕜 F]
[Fintype ι₁]
[Fintype ι₂]
(v : OrthonormalBasis ι₁ 𝕜 E)
(w : OrthonormalBasis ι₂ 𝕜 F)
(i : ι₁ ⊕ ι₂)
:
(v.prod w) i = Sum.elim (⇑(LinearMap.inl 𝕜 E F) ∘ ⇑v) (⇑(LinearMap.inr 𝕜 E F) ∘ ⇑w) i