Transporting Hilbert bases by linear isometric equivalences

This file adds the Hilbert-basis analogue of Basis.map: a Hilbert basis of a Hilbert space can be transported across a linear isometric equivalence. It also follows Mathlib's OrthonormalBasis.map API for transporting orthonormal bases. The construction is the Part 0 HilbertBasis.mapₗᵢ primitive from the OrthogonalL2Bases roadmap, used later to move weighted orthogonal-polynomial bases across the weight-change isometry.

The API is intentionally small: the representation equality and pointwise simp lemmas expose the transport, while Mathlib's existing Hilbert-basis coordinate and Parseval lemmas supply the derived coordinate identities after rewriting through the inverse isometry.

noncomputable def HilbertBasis.mapₗᵢ {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (b : HilbertBasis ι 𝕜 E) (e : E ≃ₗᵢ[𝕜] F) : HilbertBasis ι 𝕜 F

Transport a Hilbert basis along a linear isometric equivalence.

Equations

• b.mapₗᵢ e = { repr := e.symm.trans b.repr }

@[simp]

theorem HilbertBasis.repr_mapₗᵢ {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (b : HilbertBasis ι 𝕜 E) (e : E ≃ₗᵢ[𝕜] F) : (b.mapₗᵢ e).repr = e.symm.trans b.repr

The coordinate representation of b.mapₗᵢ e is b.repr after applying e.symm.

@[simp]

theorem HilbertBasis.mapₗᵢ_apply {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (b : HilbertBasis ι 𝕜 E) (e : E ≃ₗᵢ[𝕜] F) (i : ι) : (b.mapₗᵢ e) i = e (b i)

The ith vector of the transported basis is the image of the ith vector.

@[simp]

theorem HilbertBasis.coe_mapₗᵢ {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (b : HilbertBasis ι 𝕜 E) (e : E ≃ₗᵢ[𝕜] F) : ⇑(b.mapₗᵢ e) = ⇑e ∘ ⇑b

Function-level form of HilbertBasis.mapₗᵢ_apply.

@[simp]

theorem HilbertBasis.mapₗᵢ_refl {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (b : HilbertBasis ι 𝕜 E) : b.mapₗᵢ (LinearIsometryEquiv.refl 𝕜 E) = b

Transport along the identity isometry leaves a Hilbert basis unchanged.

@[simp]

theorem HilbertBasis.mapₗᵢ_trans {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {G : Type u_5} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (b : HilbertBasis ι 𝕜 E) (e : E ≃ₗᵢ[𝕜] F) (f : F ≃ₗᵢ[𝕜] G) : (b.mapₗᵢ e).mapₗᵢ f = b.mapₗᵢ (e.trans f)

Transporting along two linear isometric equivalences is the same as transporting along their composition.

theorem HilbertBasis.mapₗᵢ_symm {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (b : HilbertBasis ι 𝕜 E) (e : E ≃ₗᵢ[𝕜] F) : (b.mapₗᵢ e).mapₗᵢ e.symm = b

Transporting a Hilbert basis across an isometry and then back across the inverse isometry recovers the original basis.

theorem HilbertBasis.mapₗᵢ_symm_self {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (b : HilbertBasis ι 𝕜 F) (e : E ≃ₗᵢ[𝕜] F) : (b.mapₗᵢ e.symm).mapₗᵢ e = b

Transporting a Hilbert basis back across an inverse isometry and then forward again recovers the original basis.