The orthogonal projection

Given a nonempty subspace K of an inner product space E such that K admits an orthogonal projection, this file constructs K.orthogonalProjection : E →L[𝕜] K, the orthogonal projection of E onto K. This map satisfies: for any point u in E, the point v = K.orthogonalProjection u in K minimizes the distance ‖u - v‖ to u.

This file also defines K.starProjection : E →L[𝕜] E which is the orthogonal projection of E onto K but as a map from E to E instead of E to K.

Basic API for orthogonalProjection and starProjection is developed.

References

The orthogonal projection construction is adapted from

• [Clément & Martin, The Lax-Milgram Theorem. A detailed proof to be formalized in Coq]
• [Clément & Martin, A Coq formal proof of the Lax–Milgram theorem]

The Coq code is available at the following address: http://www.lri.fr/~sboldo/elfic/index.html

class Submodule.HasOrthogonalProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) : Prop

A subspace K : Submodule 𝕜 E has an orthogonal projection if every vector v : E admits an orthogonal projection to K.

• exists_orthogonal (v : E) : ∃ w ∈ K, v - w ∈ Kᗮ

@[instance 100]

instance Submodule.HasOrthogonalProjection.ofCompleteSpace {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [CompleteSpace ↥K] : K.HasOrthogonalProjection

instance Submodule.instHasOrthogonalProjectionOrthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] : Kᗮ.HasOrthogonalProjection

instance Submodule.HasOrthogonalProjection.map_linearIsometryEquiv {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] {E' : Type u_4} [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E') : (map (↑f.toLinearEquiv) K).HasOrthogonalProjection

instance Submodule.HasOrthogonalProjection.map_linearIsometryEquiv' {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] {E' : Type u_4} [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E') : (map f.toLinearIsometry K).HasOrthogonalProjection

instance Submodule.instHasOrthogonalProjectionTop {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : ⊤.HasOrthogonalProjection

def Submodule.orthogonalProjectionFn {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] (v : E) : E

The orthogonal projection onto a complete subspace, as an unbundled function. This definition is only intended for use in setting up the bundled version orthogonalProjection and should not be used once that is defined.

Equations

• K.orthogonalProjectionFn v = ⋯.choose

theorem Submodule.orthogonalProjectionFn_mem {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] (v : E) : K.orthogonalProjectionFn v ∈ K

The unbundled orthogonal projection is in the given subspace. This lemma is only intended for use in setting up the bundled version and should not be used once that is defined.

theorem Submodule.orthogonalProjectionFn_inner_eq_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] (v w : E) : w ∈ K → inner 𝕜 (v - K.orthogonalProjectionFn v) w = 0

The characterization of the unbundled orthogonal projection. This lemma is only intended for use in setting up the bundled version and should not be used once that is defined.

theorem Submodule.eq_orthogonalProjectionFn_of_mem_of_inner_eq_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] {u v : E} (hvm : v ∈ K) (hvo : ∀ w ∈ K, inner 𝕜 (u - v) w = 0) : K.orthogonalProjectionFn u = v

The unbundled orthogonal projection is the unique point in K with the orthogonality property. This lemma is only intended for use in setting up the bundled version and should not be used once that is defined.

theorem Submodule.orthogonalProjectionFn_norm_sq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] (v : E) : ‖v‖ * ‖v‖ = ‖v - K.orthogonalProjectionFn v‖ * ‖v - K.orthogonalProjectionFn v‖ + ‖K.orthogonalProjectionFn v‖ * ‖K.orthogonalProjectionFn v‖

def Submodule.orthogonalProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] : E →L[𝕜] ↥K

The orthogonal projection onto a complete subspace.

Equations

• K.orthogonalProjection = { toFun := fun (v : E) => ⟨K.orthogonalProjectionFn v, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯

@[simp]

theorem Submodule.orthogonalProjectionFn_eq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] (v : E) : K.orthogonalProjectionFn v = ↑(K.orthogonalProjection v)

def Submodule.starProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] : E →L[𝕜] E

The orthogonal projection onto a subspace as a map from the full space to itself, as opposed to Submodule.orthogonalProjection, which maps into the subtype. This version is important as it satisfies IsStarProjection.

Equations

• U.starProjection = U.subtypeL.comp U.orthogonalProjection

theorem Submodule.starProjection_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (v : E) : U.starProjection v = ↑(U.orthogonalProjection v)

@[simp]

theorem Submodule.coe_orthogonalProjection_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (v : E) : ↑(U.orthogonalProjection v) = U.starProjection v

@[simp]

theorem Submodule.starProjection_apply_mem {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (x : E) : U.starProjection x ∈ U

@[simp]

theorem Submodule.starProjection_inner_eq_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] (v w : E) : w ∈ K → inner 𝕜 (v - K.starProjection v) w = 0

The characterization of the orthogonal projection.

@[deprecated Submodule.starProjection_inner_eq_zero (since := "2025-07-07")]

theorem Submodule.orthogonalProjection_inner_eq_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] (v w : E) : w ∈ K → inner 𝕜 (v - K.starProjection v) w = 0

Alias of Submodule.starProjection_inner_eq_zero.

---

The characterization of the orthogonal projection.

@[simp]

theorem Submodule.sub_starProjection_mem_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] (v : E) : v - K.starProjection v ∈ Kᗮ

The difference of v from its orthogonal projection onto K is in Kᗮ.

@[deprecated Submodule.sub_starProjection_mem_orthogonal (since := "2025-07-07")]

theorem Submodule.sub_orthogonalProjection_mem_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] (v : E) : v - K.starProjection v ∈ Kᗮ

Alias of Submodule.sub_starProjection_mem_orthogonal.

---

The difference of v from its orthogonal projection onto K is in Kᗮ.

theorem Submodule.eq_starProjection_of_mem_of_inner_eq_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] {u v : E} (hvm : v ∈ K) (hvo : ∀ w ∈ K, inner 𝕜 (u - v) w = 0) : K.starProjection u = v

The orthogonal projection is the unique point in K with the orthogonality property.

@[deprecated Submodule.eq_starProjection_of_mem_of_inner_eq_zero (since := "2025-07-07")]

theorem Submodule.eq_orthogonalProjection_of_mem_of_inner_eq_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] {u v : E} (hvm : v ∈ K) (hvo : ∀ w ∈ K, inner 𝕜 (u - v) w = 0) : K.starProjection u = v

Alias of Submodule.eq_starProjection_of_mem_of_inner_eq_zero.

---

The orthogonal projection is the unique point in K with the orthogonality property.

theorem Submodule.eq_starProjection_of_mem_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] {u v : E} (hv : v ∈ K) (hvo : u - v ∈ Kᗮ) : K.starProjection u = v

A point in K with the orthogonality property (here characterized in terms of Kᗮ) must be the orthogonal projection.

@[deprecated Submodule.eq_starProjection_of_mem_orthogonal (since := "2025-07-07")]

theorem Submodule.eq_orthogonalProjection_of_mem_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] {u v : E} (hv : v ∈ K) (hvo : u - v ∈ Kᗮ) : K.starProjection u = v

Alias of Submodule.eq_starProjection_of_mem_orthogonal.

---

A point in K with the orthogonality property (here characterized in terms of Kᗮ) must be the orthogonal projection.

theorem Submodule.eq_starProjection_of_mem_orthogonal' {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] {u v z : E} (hv : v ∈ K) (hz : z ∈ Kᗮ) (hu : u = v + z) : K.starProjection u = v

A point in K with the orthogonality property (here characterized in terms of Kᗮ) must be the orthogonal projection.

@[deprecated Submodule.eq_starProjection_of_mem_orthogonal' (since := "2025-07-07")]

theorem Submodule.eq_orthogonalProjection_of_mem_orthogonal' {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] {u v z : E} (hv : v ∈ K) (hz : z ∈ Kᗮ) (hu : u = v + z) : K.starProjection u = v

Alias of Submodule.eq_starProjection_of_mem_orthogonal'.

---

A point in K with the orthogonality property (here characterized in terms of Kᗮ) must be the orthogonal projection.

@[simp]

theorem Submodule.starProjection_orthogonal_val {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] (u : E) : Kᗮ.starProjection u = u - K.starProjection u

@[deprecated Submodule.starProjection_orthogonal_val (since := "2025-07-07")]

theorem Submodule.orthogonalProjection_orthogonal_val {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] (u : E) : Kᗮ.starProjection u = u - K.starProjection u

Alias of Submodule.starProjection_orthogonal_val.

theorem Submodule.orthogonalProjection_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] (u : E) : Kᗮ.orthogonalProjection u = ⟨u - K.starProjection u, ⋯⟩

theorem Submodule.starProjection_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] : Uᗮ.starProjection = ContinuousLinearMap.id 𝕜 E - U.starProjection

theorem Submodule.starProjection_orthogonal' {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] : Uᗮ.starProjection = 1 - U.starProjection

theorem Submodule.starProjection_minimal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] (y : E) : ‖y - U.starProjection y‖ = ⨅ (x : ↥U), ‖y - ↑x‖

The orthogonal projection of y on U minimizes the distance ‖y - x‖ for x ∈ U.

@[deprecated Submodule.starProjection_minimal (since := "2025-07-07")]

theorem Submodule.orthogonalProjection_minimal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] (y : E) : ‖y - U.starProjection y‖ = ⨅ (x : ↥U), ‖y - ↑x‖

Alias of Submodule.starProjection_minimal.

---

The orthogonal projection of y on U minimizes the distance ‖y - x‖ for x ∈ U.

@[deprecated "As there are no subtypes causing dependent type issues, there is no need for this result as `simp` will suffice" (since := "12-07-2025")]

theorem Submodule.eq_starProjection_of_eq_submodule {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] {K' : Submodule 𝕜 E} [K'.HasOrthogonalProjection] (h : K = K') (u : E) : K.starProjection u = K'.starProjection u

The orthogonal projections onto equal subspaces are coerced back to the same point in E.

@[deprecated Submodule.eq_starProjection_of_eq_submodule (since := "2025-07-07")]

theorem Submodule.eq_orthogonalProjection_of_eq_submodule {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] {K' : Submodule 𝕜 E} [K'.HasOrthogonalProjection] (h : K = K') (u : E) : K.starProjection u = K'.starProjection u

Alias of Submodule.eq_starProjection_of_eq_submodule.

---

The orthogonal projections onto equal subspaces are coerced back to the same point in E.

@[simp]

theorem Submodule.orthogonalProjection_mem_subspace_eq_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] (v : ↥K) : K.orthogonalProjection ↑v = v

The orthogonal projection sends elements of K to themselves.

@[simp]

theorem Submodule.starProjection_mem_subspace_eq_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] (v : ↥K) : K.starProjection ↑v = ↑v

theorem Submodule.starProjection_eq_self_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] {v : E} : K.starProjection v = v ↔ v ∈ K

A point equals its orthogonal projection if and only if it lies in the subspace.

@[deprecated Submodule.starProjection_eq_self_iff (since := "2025-07-07")]

theorem Submodule.orthogonalProjection_eq_self_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] {v : E} : K.starProjection v = v ↔ v ∈ K

Alias of Submodule.starProjection_eq_self_iff.

---

A point equals its orthogonal projection if and only if it lies in the subspace.

@[simp]

theorem Submodule.isIdempotentElem_starProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] : IsIdempotentElem K.starProjection

@[simp]

theorem Submodule.range_starProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] : LinearMap.range U.starProjection = U

theorem Submodule.starProjection_top {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : ⊤.starProjection = ContinuousLinearMap.id 𝕜 E

theorem Submodule.starProjection_top' {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : ⊤.starProjection = 1

@[simp]

theorem Submodule.orthogonalProjection_eq_zero_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] {v : E} : K.orthogonalProjection v = 0 ↔ v ∈ Kᗮ

@[simp]

theorem Submodule.ker_orthogonalProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] : LinearMap.ker K.orthogonalProjection = Kᗮ

@[simp]

theorem Submodule.ker_starProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] : LinearMap.ker U.starProjection = Uᗮ

theorem LinearIsometry.map_starProjection {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_4} {E' : Type u_5} [NormedAddCommGroup E] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 E'] (f : E →ₗᵢ[𝕜] E') (p : Submodule 𝕜 E) [p.HasOrthogonalProjection] [(Submodule.map f.toLinearMap p).HasOrthogonalProjection] (x : E) : f (p.starProjection x) = (Submodule.map f.toLinearMap p).starProjection (f x)

@[deprecated LinearIsometry.map_starProjection (since := "2025-07-07")]

theorem LinearIsometry.map_orthogonalProjection {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_4} {E' : Type u_5} [NormedAddCommGroup E] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 E'] (f : E →ₗᵢ[𝕜] E') (p : Submodule 𝕜 E) [p.HasOrthogonalProjection] [(Submodule.map f.toLinearMap p).HasOrthogonalProjection] (x : E) : f (p.starProjection x) = (Submodule.map f.toLinearMap p).starProjection (f x)

Alias of LinearIsometry.map_starProjection.

theorem LinearIsometry.map_starProjection' {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_4} {E' : Type u_5} [NormedAddCommGroup E] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 E'] (f : E →ₗᵢ[𝕜] E') (p : Submodule 𝕜 E) [p.HasOrthogonalProjection] [(Submodule.map f p).HasOrthogonalProjection] (x : E) : f (p.starProjection x) = (Submodule.map f p).starProjection (f x)

@[deprecated LinearIsometry.map_starProjection' (since := "2025-07-07")]

theorem LinearIsometry.map_orthogonalProjection' {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_4} {E' : Type u_5} [NormedAddCommGroup E] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 E'] (f : E →ₗᵢ[𝕜] E') (p : Submodule 𝕜 E) [p.HasOrthogonalProjection] [(Submodule.map f p).HasOrthogonalProjection] (x : E) : f (p.starProjection x) = (Submodule.map f p).starProjection (f x)

Alias of LinearIsometry.map_starProjection'.

theorem Submodule.starProjection_map_apply {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_4} {E' : Type u_5} [NormedAddCommGroup E] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E') (p : Submodule 𝕜 E) [p.HasOrthogonalProjection] (x : E') : (map (↑f.toLinearEquiv) p).starProjection x = f (p.starProjection (f.symm x))

Orthogonal projection onto the Submodule.map of a subspace.

@[deprecated Submodule.starProjection_map_apply (since := "2025-07-07")]

theorem Submodule.orthogonalProjection_map_apply {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_4} {E' : Type u_5} [NormedAddCommGroup E] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E') (p : Submodule 𝕜 E) [p.HasOrthogonalProjection] (x : E') : (map (↑f.toLinearEquiv) p).starProjection x = f (p.starProjection (f.symm x))

Alias of Submodule.starProjection_map_apply.

---

Orthogonal projection onto the Submodule.map of a subspace.

@[simp]

theorem Submodule.orthogonalProjection_bot {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : ⊥.orthogonalProjection = 0

The orthogonal projection onto the trivial submodule is the zero map.

@[simp]

theorem Submodule.starProjection_bot {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : ⊥.starProjection = 0

theorem Submodule.orthogonalProjection_norm_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] : ‖K.orthogonalProjection‖ ≤ 1

The orthogonal projection has norm ≤ 1.

theorem Submodule.starProjection_norm_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] : ‖K.starProjection‖ ≤ 1

theorem Submodule.norm_orthogonalProjection_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] {v : E} (hv : v ∈ K) : ‖K.orthogonalProjection v‖ = ‖v‖

theorem Submodule.norm_starProjection_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] {v : E} (hv : v ∈ K) : ‖K.starProjection v‖ = ‖v‖

theorem Submodule.norm_orthogonalProjection_apply_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] (v : E) : ‖K.orthogonalProjection v‖ ≤ ‖v‖

The orthogonal projection onto a closed subspace is norm non-increasing.

theorem Submodule.norm_starProjection_apply_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] (v : E) : ‖K.starProjection v‖ ≤ ‖v‖

theorem Submodule.lipschitzWith_orthogonalProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] : LipschitzWith 1 ⇑K.orthogonalProjection

The orthogonal projection onto a closed subspace is a 1-Lipschitz map.

theorem Submodule.lipschitzWith_starProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] : LipschitzWith 1 ⇑K.starProjection

theorem Submodule.norm_orthogonalProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] (hK : K ≠ ⊥) : ‖K.orthogonalProjection‖ = 1

The operator norm of the orthogonal projection onto a nontrivial subspace is 1.

theorem Submodule.norm_starProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] (hK : K ≠ ⊥) : ‖K.starProjection‖ = 1

theorem Submodule.smul_starProjection_singleton (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {v : E} (w : E) : ↑(‖v‖ ^ 2) • (span 𝕜 {v}).starProjection w = inner 𝕜 v w • v

@[deprecated Submodule.smul_starProjection_singleton (since := "2025-07-07")]

theorem Submodule.smul_orthogonalProjection_singleton (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {v : E} (w : E) : ↑(‖v‖ ^ 2) • (span 𝕜 {v}).starProjection w = inner 𝕜 v w • v

Alias of Submodule.smul_starProjection_singleton.

theorem Submodule.starProjection_singleton (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {v : E} (w : E) : (span 𝕜 {v}).starProjection w = (inner 𝕜 v w / ↑(‖v‖ ^ 2)) • v

Formula for orthogonal projection onto a single vector.

@[deprecated Submodule.starProjection_singleton (since := "2025-07-07")]

theorem Submodule.orthogonalProjection_singleton (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {v : E} (w : E) : (span 𝕜 {v}).starProjection w = (inner 𝕜 v w / ↑(‖v‖ ^ 2)) • v

Alias of Submodule.starProjection_singleton.

---

Formula for orthogonal projection onto a single vector.

theorem Submodule.starProjection_unit_singleton (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {v : E} (hv : ‖v‖ = 1) (w : E) : (span 𝕜 {v}).starProjection w = inner 𝕜 v w • v

Formula for orthogonal projection onto a single unit vector.

@[deprecated Submodule.starProjection_unit_singleton (since := "2025-07-07")]

theorem Submodule.orthogonalProjection_unit_singleton (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {v : E} (hv : ‖v‖ = 1) (w : E) : (span 𝕜 {v}).starProjection w = inner 𝕜 v w • v

Alias of Submodule.starProjection_unit_singleton.

---

Formula for orthogonal projection onto a single unit vector.

theorem Submodule.exists_add_mem_mem_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] (v : E) : ∃ y ∈ K, ∃ z ∈ Kᗮ, v = y + z

If K is complete, any v in E can be expressed as a sum of elements of K and Kᗮ.

theorem Submodule.orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] {v : E} (hv : v ∈ Kᗮ) : K.orthogonalProjection v = 0

The orthogonal projection onto K of an element of Kᗮ is zero.

theorem Submodule.IsOrtho.orthogonalProjection_comp_subtypeL {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U V : Submodule 𝕜 E} [U.HasOrthogonalProjection] (h : U ⟂ V) : U.orthogonalProjection.comp V.subtypeL = 0

The projection into U from an orthogonal submodule V is the zero map.

theorem Submodule.IsOrtho.starProjection_comp_starProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U V : Submodule 𝕜 E} [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] (h : U ⟂ V) : U.starProjection.comp V.starProjection = 0

theorem Submodule.orthogonalProjection_comp_subtypeL_eq_zero_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U V : Submodule 𝕜 E} [U.HasOrthogonalProjection] : U.orthogonalProjection.comp V.subtypeL = 0 ↔ U ⟂ V

The projection into U from V is the zero map if and only if U and V are orthogonal.

theorem Submodule.starProjection_comp_starProjection_eq_zero_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U V : Submodule 𝕜 E} [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.starProjection.comp V.starProjection = 0 ↔ U ⟂ V

U.starProjection ∘ V.starProjection = 0 iff U and V are pairwise orthogonal.

theorem Submodule.orthogonalProjection_orthogonal_apply_eq_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [Kᗮ.HasOrthogonalProjection] {v : E} (hv : v ∈ K) : Kᗮ.orthogonalProjection v = 0

The orthogonal projection onto Kᗮ of an element of K is zero.

@[deprecated Submodule.orthogonalProjection_orthogonal_apply_eq_zero (since := "22-07-2025")]

theorem Submodule.orthogonalProjection_mem_subspace_orthogonal_precomplement_eq_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [Kᗮ.HasOrthogonalProjection] {v : E} (hv : v ∈ K) : Kᗮ.orthogonalProjection v = 0

Alias of Submodule.orthogonalProjection_orthogonal_apply_eq_zero.

---

The orthogonal projection onto Kᗮ of an element of K is zero.

theorem Submodule.starProjection_orthogonal_apply_eq_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [Kᗮ.HasOrthogonalProjection] {v : E} (hv : v ∈ K) : Kᗮ.starProjection v = 0

theorem Submodule.orthogonalProjection_starProjection_of_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U V : Submodule 𝕜 E} [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] (h : U ≤ V) (x : E) : U.orthogonalProjection (V.starProjection x) = U.orthogonalProjection x

If U ≤ V, then projecting on V and then on U is the same as projecting on U.

@[deprecated Submodule.orthogonalProjection_starProjection_of_le (since := "2025-07-07")]

theorem Submodule.orthogonalProjection_orthogonalProjection_of_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U V : Submodule 𝕜 E} [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] (h : U ≤ V) (x : E) : U.orthogonalProjection (V.starProjection x) = U.orthogonalProjection x

Alias of Submodule.orthogonalProjection_starProjection_of_le.

---

If U ≤ V, then projecting on V and then on U is the same as projecting on U.

theorem Submodule.starProjection_comp_starProjection_of_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U V : Submodule 𝕜 E} [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] (h : U ≤ V) : U.starProjection.comp V.starProjection = U.starProjection

theorem ContinuousLinearMap.IsIdempotentElem.hasOrthogonalProjection_range {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {p : E →L[𝕜] E} (hp : IsIdempotentElem p) : (LinearMap.range p).HasOrthogonalProjection

theorem Submodule.orthogonalProjection_orthogonalComplement_singleton_eq_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (v : E) : (span 𝕜 {v})ᗮ.orthogonalProjection v = 0

The orthogonal projection onto (𝕜 ∙ v)ᗮ of v is zero.

theorem Submodule.starProjection_orthogonalComplement_singleton_eq_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (v : E) : (span 𝕜 {v})ᗮ.starProjection v = 0

theorem Submodule.starProjection_add_starProjection_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] (w : E) : K.starProjection w + Kᗮ.starProjection w = w

If the orthogonal projection to K is well-defined, then a vector splits as the sum of its orthogonal projections onto a complete submodule K and onto the orthogonal complement of K.

@[deprecated Submodule.starProjection_add_starProjection_orthogonal (since := "2025-07-07")]

theorem Submodule.orthogonalProjection_add_orthogonalProjection_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] (w : E) : K.starProjection w + Kᗮ.starProjection w = w

Alias of Submodule.starProjection_add_starProjection_orthogonal.

---

If the orthogonal projection to K is well-defined, then a vector splits as the sum of its orthogonal projections onto a complete submodule K and onto the orthogonal complement of K.

theorem Submodule.norm_sq_eq_add_norm_sq_projection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (S : Submodule 𝕜 E) [S.HasOrthogonalProjection] : ‖x‖ ^ 2 = ‖S.orthogonalProjection x‖ ^ 2 + ‖Sᗮ.orthogonalProjection x‖ ^ 2

The Pythagorean theorem, for an orthogonal projection.

theorem Submodule.norm_sq_eq_add_norm_sq_starProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (S : Submodule 𝕜 E) [S.HasOrthogonalProjection] : ‖x‖ ^ 2 = ‖S.starProjection x‖ ^ 2 + ‖Sᗮ.starProjection x‖ ^ 2

theorem Submodule.mem_iff_norm_starProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (v : E) : v ∈ U ↔ ‖U.starProjection v‖ = ‖v‖

theorem Submodule.id_eq_sum_starProjection_self_orthogonalComplement {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] : ContinuousLinearMap.id 𝕜 E = K.starProjection + Kᗮ.starProjection

In a complete space E, the projection maps onto a complete subspace K and its orthogonal complement sum to the identity.

@[deprecated Submodule.id_eq_sum_starProjection_self_orthogonalComplement (since := "2025-07-07")]

theorem Submodule.id_eq_sum_orthogonalProjection_self_orthogonalComplement {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] : ContinuousLinearMap.id 𝕜 E = K.starProjection + Kᗮ.starProjection

Alias of Submodule.id_eq_sum_starProjection_self_orthogonalComplement.

---

In a complete space E, the projection maps onto a complete subspace K and its orthogonal complement sum to the identity.

@[simp]

theorem Submodule.inner_orthogonalProjection_eq_of_mem_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] (u : ↥K) (v : E) : inner 𝕜 (K.orthogonalProjection v) u = inner 𝕜 v ↑u

@[simp]

theorem Submodule.inner_orthogonalProjection_eq_of_mem_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] (u : ↥K) (v : E) : inner 𝕜 u (K.orthogonalProjection v) = inner 𝕜 (↑u) v

theorem Submodule.inner_starProjection_left_eq_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] (u v : E) : inner 𝕜 (K.starProjection u) v = inner 𝕜 u (K.starProjection v)

The orthogonal projection is self-adjoint.

@[deprecated Submodule.inner_starProjection_left_eq_right (since := "2025-07-07")]

theorem Submodule.inner_orthogonalProjection_left_eq_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] (u v : E) : inner 𝕜 (K.starProjection u) v = inner 𝕜 u (K.starProjection v)

Alias of Submodule.inner_starProjection_left_eq_right.

---

The orthogonal projection is self-adjoint.

theorem Submodule.starProjection_isSymmetric {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] : (↑K.starProjection).IsSymmetric

The orthogonal projection is symmetric.

@[deprecated Submodule.starProjection_isSymmetric (since := "2025-07-07")]

theorem Submodule.orthogonalProjection_isSymmetric {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] : (↑K.starProjection).IsSymmetric

Alias of Submodule.starProjection_isSymmetric.

---

The orthogonal projection is symmetric.

theorem Submodule.starProjection_apply_eq_zero_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] {v : E} : K.starProjection v = 0 ↔ v ∈ Kᗮ

theorem Submodule.re_inner_starProjection_eq_normSq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] (v : E) : RCLike.re (inner 𝕜 (K.starProjection v) v) = ‖K.orthogonalProjection v‖ ^ 2

@[deprecated Submodule.re_inner_starProjection_eq_normSq (since := "2025-07-07")]

theorem Submodule.re_inner_orthogonalProjection_eq_normSq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] (v : E) : RCLike.re (inner 𝕜 (K.starProjection v) v) = ‖K.orthogonalProjection v‖ ^ 2

Alias of Submodule.re_inner_starProjection_eq_normSq.

theorem Submodule.re_inner_starProjection_nonneg {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] (v : E) : 0 ≤ RCLike.re (inner 𝕜 (K.starProjection v) v)

@[deprecated Submodule.re_inner_starProjection_nonneg (since := "2025-07-07")]

theorem Submodule.re_inner_orthogonalProjection_nonneg {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] (v : E) : 0 ≤ RCLike.re (inner 𝕜 (K.starProjection v) v)

Alias of Submodule.re_inner_starProjection_nonneg.