Partial isometries between Hilbert spaces

A map u : E → F between Hilbert spaces is a partial isometry when u u† u = u. Unlike the star-monoid predicate TauCeti.IsPartialIsometry, this makes sense for maps between two different spaces, as needed for the polar factor of a rectangular operator. This file develops the predicate for bounded operators between complete inner product spaces and for linear maps between finite-dimensional ones, and proves its geometric characterization: u is a partial isometry exactly when it preserves norms on its initial space (ker u)ᗮ. Equivalently, u† u is the orthogonal projection onto (ker u)ᗮ, or merely some star projection.

Main definitions

• ContinuousLinearMap.IsPartialIsometry u: the bounded operator u satisfies u u† u = u.
• LinearMap.IsPartialIsometry u: the finite-dimensional linear map u satisfies u u† u = u.

Main statements

• ContinuousLinearMap.isPartialIsometry_iff_norm_map, LinearMap.isPartialIsometry_iff_norm_map: a map is a partial isometry iff it preserves norms on the orthogonal complement of its kernel.
• ContinuousLinearMap.IsPartialIsometry.adjoint_comp_self_eq_starProjection: the initial projection u† u of a bounded partial isometry is the orthogonal projection onto (ker u)ᗮ.
• ContinuousLinearMap.IsPartialIsometry.comp_adjoint_eq_starProjection: the final projection u u† is the orthogonal projection onto the closure of the range of u, and ContinuousLinearMap.IsPartialIsometry.isClosed_range: that range is closed.
• ContinuousLinearMap.isPartialIsometry_iff_isStarProjection_adjoint_comp_self, LinearMap.isPartialIsometry_iff_isStarProjection_adjoint_comp_self: a map is a partial isometry iff u† u is a star projection.
• ContinuousLinearMap.isPartialIsometry_adjoint_iff, LinearMap.isPartialIsometry_adjoint_iff: the adjoint of a partial isometry is a partial isometry.
• ContinuousLinearMap.isPartialIsometry_iff_starMul, LinearMap.isPartialIsometry_iff_starMul: on endomorphisms the rectangular predicate agrees with the star-monoid predicate.
• ContinuousLinearMap.IsPartialIsometry.adjoint_comp_comp_comp_of_mapsTo: compression u† T u along a bounded partial isometry is multiplicative when the right factor preserves the range of u.
• LinearIsometry.isPartialIsometry_toContinuousLinearMap, LinearIsometry.isPartialIsometry_toLinearMap: linear isometries are partial isometries, and LinearIsometry.apply_adjoint_apply_of_mem_range: f f† fixes the range of f.
• LinearMap.adjoint_comp_eq_zero_of_comp_adjoint_add_eq_id: complementary final operators have orthogonal cross blocks if one block is a partial isometry.
• Submodule.exists_star_mul_self_eq_starProjection_and_starProjection_mul_eq_zero: if Kᗮ is at least as large as the finite-dimensional subspace K, some operator u maps K isometrically into Kᗮ and vanishes on Kᗮ, so that its initial projection is P_K and P_K * u = 0.

Provenance

The complementary-block orthogonality lemma is adapted from ForTauCeti/Analysis/InnerProductSpace/DoubleAngle/Gram.lean in the AIQ-Kitware DKPS formalization, released under Apache 2.0.

References

• J. B. Conway, A Course in Functional Analysis, 2nd ed., Springer (1990), the treatment of partial isometries and the polar decomposition.

def ContinuousLinearMap.IsPartialIsometry {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (u : E →L[𝕜] F) : Prop

A bounded operator u : E →L[𝕜] F is a partial isometry when u u† u = u.

theorem ContinuousLinearMap.isPartialIsometry_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] {u : E →L[𝕜] F} : u.IsPartialIsometry ↔ u ∘SL adjoint u ∘SL u = u

Unfold the definition of a bounded partial isometry.

theorem ContinuousLinearMap.IsPartialIsometry.comp_adjoint_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] {u : E →L[𝕜] F} (hu : u.IsPartialIsometry) : u ∘SL ContinuousLinearMap.adjoint u ∘SL u = u

The defining equation u u† u = u of a bounded partial isometry.

@[simp]

theorem ContinuousLinearMap.IsPartialIsometry.apply_adjoint_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] {u : E →L[𝕜] F} (hu : u.IsPartialIsometry) (x : E) : u ((ContinuousLinearMap.adjoint u) (u x)) = u x

The defining equation u u† u = u of a bounded partial isometry, applied to a vector.

theorem ContinuousLinearMap.IsPartialIsometry.apply_adjoint_apply_of_mem_range {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] {u : E →L[𝕜] F} (hu : u.IsPartialIsometry) {y : F} (hy : y ∈ Set.range ⇑u) : u ((ContinuousLinearMap.adjoint u) y) = y

A bounded partial isometry u satisfies u u† y = y on its range.

theorem ContinuousLinearMap.IsPartialIsometry.adjoint_comp_comp_comp_of_mapsTo {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] {u : E →L[𝕜] F} (hu : u.IsPartialIsometry) (S : F →L[𝕜] F) {T : F →L[𝕜] F} (hT : Set.MapsTo (⇑T) (Set.range ⇑u) (Set.range ⇑u)) : ContinuousLinearMap.adjoint u ∘SL (S ∘SL T) ∘SL u = (ContinuousLinearMap.adjoint u ∘SL S ∘SL u) ∘SL ContinuousLinearMap.adjoint u ∘SL T ∘SL u

Compression u† T u along a bounded partial isometry u is multiplicative when the right factor preserves the range of u.

theorem ContinuousLinearMap.isPartialIsometry_iff_starMul {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {u : E →L[𝕜] E} : u.IsPartialIsometry ↔ TauCeti.IsPartialIsometry u

A bounded partial isometry is a partial isometry in the star monoid of endomorphisms.

theorem ContinuousLinearMap.IsPartialIsometry.adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] {u : E →L[𝕜] F} (hu : u.IsPartialIsometry) : (ContinuousLinearMap.adjoint u).IsPartialIsometry

The adjoint of a bounded partial isometry is a partial isometry.

@[simp]

theorem ContinuousLinearMap.isPartialIsometry_adjoint_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] {u : E →L[𝕜] F} : (adjoint u).IsPartialIsometry ↔ u.IsPartialIsometry

A bounded operator is a partial isometry iff its adjoint is.

theorem ContinuousLinearMap.isPartialIsometry_iff_adjoint_apply_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] {u : E →L[𝕜] F} : u.IsPartialIsometry ↔ ∀ x ∈ (↑u).kerᗮ, (adjoint u) (u x) = x

A bounded operator is a partial isometry iff u† u restricts to the identity on the initial space (ker u)ᗮ.

theorem ContinuousLinearMap.IsPartialIsometry.adjoint_apply_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] {u : E →L[𝕜] F} (hu : u.IsPartialIsometry) {x : E} (hx : x ∈ (↑u).kerᗮ) : (ContinuousLinearMap.adjoint u) (u x) = x

A bounded partial isometry u satisfies u† u x = x on its initial space (ker u)ᗮ.

theorem ContinuousLinearMap.IsPartialIsometry.adjoint_comp_self_eq_starProjection {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] {u : E →L[𝕜] F} (hu : u.IsPartialIsometry) : ContinuousLinearMap.adjoint u ∘SL u = (↑u).kerᗮ.starProjection

The initial projection u† u of a bounded partial isometry is the orthogonal projection onto its initial space (ker u)ᗮ.

theorem ContinuousLinearMap.isPartialIsometry_iff_isStarProjection_adjoint_comp_self {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] {u : E →L[𝕜] F} : u.IsPartialIsometry ↔ IsStarProjection (adjoint u ∘SL u)

A bounded operator is a partial isometry iff u† u is a star projection.

theorem ContinuousLinearMap.IsPartialIsometry.isStarProjection_adjoint_comp_self {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] {u : E →L[𝕜] F} (hu : u.IsPartialIsometry) : IsStarProjection (ContinuousLinearMap.adjoint u ∘SL u)

The initial projection u† u of a bounded partial isometry is a star projection.

theorem ContinuousLinearMap.IsPartialIsometry.isStarProjection_comp_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] {u : E →L[𝕜] F} (hu : u.IsPartialIsometry) : IsStarProjection (u ∘SL ContinuousLinearMap.adjoint u)

The final projection u u† of a bounded partial isometry is a star projection.

theorem ContinuousLinearMap.isPartialIsometry_iff_norm_map {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] {u : E →L[𝕜] F} : u.IsPartialIsometry ↔ ∀ x ∈ (↑u).kerᗮ, ‖u x‖ = ‖x‖

Geometric characterization of partial isometries. A bounded operator is a partial isometry iff it preserves norms on the orthogonal complement of its kernel.

theorem ContinuousLinearMap.IsPartialIsometry.norm_map {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] {u : E →L[𝕜] F} (hu : u.IsPartialIsometry) {x : E} (hx : x ∈ (↑u).kerᗮ) : ‖u x‖ = ‖x‖

A bounded partial isometry preserves norms on its initial space (ker u)ᗮ.

theorem ContinuousLinearMap.IsPartialIsometry.comp_adjoint_eq_starProjection {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] {u : E →L[𝕜] F} (hu : u.IsPartialIsometry) : u ∘SL ContinuousLinearMap.adjoint u = (↑u).range.topologicalClosure.starProjection

The final projection u u† of a bounded partial isometry is the orthogonal projection onto its final space, the closure of its range.

theorem ContinuousLinearMap.IsPartialIsometry.isClosed_range {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] {u : E →L[𝕜] F} (hu : u.IsPartialIsometry) : IsClosed ↑(↑u).range

A bounded partial isometry has closed range.

theorem LinearIsometry.isPartialIsometry_toContinuousLinearMap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (f : E →ₗᵢ[𝕜] F) : f.toContinuousLinearMap.IsPartialIsometry

A linear isometry between complete inner product spaces is a bounded partial isometry.

theorem LinearIsometry.apply_adjoint_apply_of_mem_range {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (f : E →ₗᵢ[𝕜] F) {y : F} (hy : y ∈ Set.range ⇑f) : f ((ContinuousLinearMap.adjoint f.toContinuousLinearMap) y) = y

A linear isometry f between complete inner product spaces satisfies f f† y = y on its range.

def LinearMap.IsPartialIsometry {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (u : E →ₗ[𝕜] F) : Prop

A linear map u : E →ₗ[𝕜] F between finite-dimensional inner product spaces is a partial isometry when u u† u = u.

theorem LinearMap.isPartialIsometry_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {u : E →ₗ[𝕜] F} : u.IsPartialIsometry ↔ u ∘ₗ adjoint u ∘ₗ u = u

Unfold the definition of a finite-dimensional partial isometry.

theorem LinearMap.IsPartialIsometry.comp_adjoint_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {u : E →ₗ[𝕜] F} (hu : u.IsPartialIsometry) : u ∘ₗ LinearMap.adjoint u ∘ₗ u = u

The defining equation u u† u = u of a finite-dimensional partial isometry.

theorem LinearMap.adjoint_comp_eq_zero_of_comp_adjoint_add_eq_id {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {L : Type u_4} [NormedAddCommGroup L] [InnerProductSpace 𝕜 L] [FiniteDimensional 𝕜 L] (F₀ : L →ₗ[𝕜] F) (F₁ : E →ₗ[𝕜] F) (hF₁ : F₁.IsPartialIsometry) (hF : F₀ ∘ₗ adjoint F₀ + F₁ ∘ₗ adjoint F₁ = id) : adjoint F₀ ∘ₗ F₁ = 0

Complementary partial-isometry blocks have orthogonal ranges. If F₁ is a partial isometry and F₀F₀⋆ + F₁F₁⋆ = 1, then F₀⋆F₁ = 0. No isometry or injectivity hypothesis is needed for F₀.

theorem LinearMap.isPartialIsometry_toContinuousLinearMap_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {u : E →ₗ[𝕜] F} : have this := ⋯; have this_1 := ⋯; (toContinuousLinearMap u).IsPartialIsometry ↔ u.IsPartialIsometry

A finite-dimensional linear map is a partial isometry iff the corresponding bounded operator is one.

theorem LinearMap.isPartialIsometry_iff_starMul {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {u : E →ₗ[𝕜] E} : u.IsPartialIsometry ↔ TauCeti.IsPartialIsometry u

A finite-dimensional partial isometry is a partial isometry in the star monoid of endomorphisms.

theorem LinearMap.IsPartialIsometry.adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {u : E →ₗ[𝕜] F} (hu : u.IsPartialIsometry) : (LinearMap.adjoint u).IsPartialIsometry

The adjoint of a finite-dimensional partial isometry is a partial isometry.

@[simp]

theorem LinearMap.isPartialIsometry_adjoint_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {u : E →ₗ[𝕜] F} : (adjoint u).IsPartialIsometry ↔ u.IsPartialIsometry

A finite-dimensional linear map is a partial isometry iff its adjoint is.

theorem LinearMap.isPartialIsometry_iff_isStarProjection_adjoint_comp_self {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {u : E →ₗ[𝕜] F} : u.IsPartialIsometry ↔ IsStarProjection (adjoint u ∘ₗ u)

A finite-dimensional linear map is a partial isometry iff u† u is a star projection.

theorem LinearMap.IsPartialIsometry.isStarProjection_adjoint_comp_self {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {u : E →ₗ[𝕜] F} (hu : u.IsPartialIsometry) : IsStarProjection (LinearMap.adjoint u ∘ₗ u)

The initial projection u† u of a finite-dimensional partial isometry is a star projection.

theorem LinearMap.isPartialIsometry_iff_norm_map {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {u : E →ₗ[𝕜] F} : u.IsPartialIsometry ↔ ∀ x ∈ u.kerᗮ, ‖u x‖ = ‖x‖

Geometric characterization of partial isometries. A linear map between finite-dimensional inner product spaces is a partial isometry iff it preserves norms on the orthogonal complement of its kernel.

theorem LinearIsometry.isPartialIsometry_toLinearMap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (f : E →ₗᵢ[𝕜] F) : f.IsPartialIsometry

A linear isometry between finite-dimensional inner product spaces is a partial isometry.

theorem Submodule.exists_star_mul_self_eq_starProjection_and_starProjection_mul_eq_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (K : Submodule 𝕜 E) [FiniteDimensional 𝕜 ↥K] (hK : ↑(Module.finrank 𝕜 ↥K) ≤ Module.rank 𝕜 ↥Kᗮ) : ∃ (u : E →L[𝕜] E), star u * u = K.starProjection ∧ K.starProjection * u = 0

If the orthogonal complement of a finite-dimensional subspace K has dimension at least Module.finrank 𝕜 K, some operator u maps K isometrically into Kᗮ and vanishes on Kᗮ: star u * u = K.starProjection and K.starProjection * u = 0.