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))

@[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)) : inner 𝕜 x y = inner 𝕜 x.ofLp.1 y.ofLp.1 + inner 𝕜 x.ofLp.2 y.ofLp.2

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.

@[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 (WithLp.toLp 2 ∘ ⇑(LinearMap.inl 𝕜 E F) ∘ ⇑v) (WithLp.toLp 2 ∘ ⇑(LinearMap.inr 𝕜 E F) ∘ ⇑w) i

def Submodule.orthogonalDecomposition {𝕜 : Type u_1} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] : E ≃ₗᵢ[𝕜] WithLp 2 (↥K × ↥Kᗮ)

If a subspace K of an inner product space E admits an orthogonal projection, then E is isometrically isomorphic to the L² product of K and Kᗮ.

@[simp]

theorem Submodule.orthogonalDecomposition_symm_apply {𝕜 : Type u_1} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] (a✝ : WithLp 2 (↥K × ↥Kᗮ)) : K.orthogonalDecomposition.symm a✝ = ↑a✝.fst + ↑a✝.snd

@[simp]

theorem Submodule.orthogonalDecomposition_apply {𝕜 : Type u_1} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] (x : E) : K.orthogonalDecomposition x = WithLp.toLp 2 (K.orthogonalProjection x, Kᗮ.orthogonalProjection x)

theorem Submodule.toLinearEquiv_orthogonalDecomposition {𝕜 : Type u_1} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] : K.orthogonalDecomposition.toLinearEquiv = (K.prodEquivOfIsCompl Kᗮ ⋯).symm ≪≫ₗ (WithLp.linearEquiv 2 𝕜 (↥K × ↥Kᗮ)).symm

theorem Submodule.toLinearEquiv_orthogonalDecomposition_symm {𝕜 : Type u_1} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] : K.orthogonalDecomposition.symm.toLinearEquiv = WithLp.linearEquiv 2 𝕜 (↥K × ↥Kᗮ) ≪≫ₗ K.prodEquivOfIsCompl Kᗮ ⋯

theorem Submodule.coe_orthogonalDecomposition {𝕜 : Type u_1} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] : ↑K.orthogonalDecomposition.toContinuousLinearEquiv = (↑(WithLp.prodContinuousLinearEquiv 2 𝕜 ↥K ↥Kᗮ).symm).comp (K.orthogonalProjection.prod Kᗮ.orthogonalProjection)

theorem Submodule.coe_orthogonalDecomposition_symm {𝕜 : Type u_1} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] : ↑K.orthogonalDecomposition.symm.toContinuousLinearEquiv = (K.subtypeL.coprod Kᗮ.subtypeL).comp ↑(WithLp.prodContinuousLinearEquiv 2 𝕜 ↥K ↥Kᗮ)

theorem Submodule.fst_orthogonalDecomposition_apply {𝕜 : Type u_1} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] (x : E) : (K.orthogonalDecomposition x).fst = K.orthogonalProjection x

theorem Submodule.snd_orthogonalDecomposition_apply {𝕜 : Type u_1} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] (x : E) : (K.orthogonalDecomposition x).snd = Kᗮ.orthogonalProjection x

theorem Submodule.fstL_comp_coe_orthogonalDecomposition {𝕜 : Type u_1} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] : (WithLp.fstL 2 𝕜 ↥K ↥Kᗮ).comp ↑K.orthogonalDecomposition.toContinuousLinearEquiv = K.orthogonalProjection

theorem Submodule.sndL_comp_coe_orthogonalDecomposition {𝕜 : Type u_1} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] : (WithLp.sndL 2 𝕜 ↥K ↥Kᗮ).comp ↑K.orthogonalDecomposition.toContinuousLinearEquiv = Kᗮ.orthogonalProjection