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

@[instance_reducible]

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

• One or more equations did not get rendered due to their size.

@[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

noncomputable 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 ⋯

@[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

noncomputable 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ᗮ.

Equations

• K.orthogonalDecomposition = { toLinearEquiv := (K.prodEquivOfIsCompl Kᗮ ⋯).symm.trans (WithLp.linearEquiv 2 𝕜 (↥K × ↥Kᗮ)).symm, norm_map' := ⋯ }

@[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.orthogonalProjectionOnto x, Kᗮ.orthogonalProjectionOnto 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 = ↑(WithLp.prodContinuousLinearEquiv 2 𝕜 ↥K ↥Kᗮ).symm ∘SL K.orthogonalProjectionOnto.prod Kᗮ.orthogonalProjectionOnto

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 = K.subtypeL.coprod Kᗮ.subtypeL ∘SL ↑(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.orthogonalProjectionOnto 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ᗮ.orthogonalProjectionOnto 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ᗮ ∘SL ↑↑K.orthogonalDecomposition = K.orthogonalProjectionOnto

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ᗮ ∘SL ↑↑K.orthogonalDecomposition = Kᗮ.orthogonalProjectionOnto

noncomputable def Submodule.quotientEquivOrthogonal {𝕜 : Type u_1} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] : E ⧸ K ≃ₗᵢ[𝕜] ↥Kᗮ

If a subspace K of an inner product space E admits an orthogonal projection, then the quotient E ⧸ K is isometrically isomorphic to the orthogonal complement Kᗮ of K.

Equations

• K.quotientEquivOrthogonal = { toLinearEquiv := K.quotientEquivOfIsCompl Kᗮ ⋯, norm_map' := ⋯ }

@[simp]

theorem Submodule.coe_quotientEquivOrthogonal {𝕜 : Type u_1} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] : ⇑K.quotientEquivOrthogonal = ⇑(K.quotientEquivOfIsCompl Kᗮ ⋯)

@[simp]

theorem Submodule.coe_quotientEquivOrthogonal_symm {𝕜 : Type u_1} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] : ⇑K.quotientEquivOrthogonal.symm = ⇑(K.quotientEquivOfIsCompl Kᗮ ⋯).symm

@[simp]

theorem Submodule.toLinearEquiv_quotientEquivOrthogonal {𝕜 : Type u_1} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] : K.quotientEquivOrthogonal.toLinearEquiv = K.quotientEquivOfIsCompl Kᗮ ⋯

theorem Submodule.quotientEquivOrthogonal_mk {𝕜 : Type u_1} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] (x : E) (hx : x ∈ Kᗮ) : K.quotientEquivOrthogonal (Quotient.mk x) = ⟨x, hx⟩

theorem Submodule.quotientEquivOrthogonal_symm_eq_mk {𝕜 : Type u_1} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] (x : E) (hx : x ∈ Kᗮ) : K.quotientEquivOrthogonal.symm ⟨x, hx⟩ = Quotient.mk x

@[instance_reducible]

noncomputable instance Submodule.instQuotientInnerProductSpace {𝕜 : Type u_1} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] : InnerProductSpace 𝕜 (E ⧸ K)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Submodule.inner_quotient_eq {𝕜 : Type u_1} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] (x y : E ⧸ K) : inner 𝕜 x y = inner 𝕜 (K.quotientEquivOrthogonal x) (K.quotientEquivOrthogonal y)

theorem Submodule.Quotient.inner_mk_mk {𝕜 : Type u_1} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] (x y : E) (hx : x ∈ Kᗮ) (hy : y ∈ Kᗮ) : inner 𝕜 (mk x) (mk y) = inner 𝕜 x y