Documentation

Mathlib.Analysis.InnerProductSpace.Orthogonal

Orthogonal complements of submodules #

In this file, the orthogonal complement of a submodule K is defined, and basic API established. We make duplicates for Submodule and ClosedSubmodule. Some of the more subtle results about the orthogonal complement are delayed to Analysis.InnerProductSpace.Projection.

See also BilinForm.orthogonal for orthogonality with respect to a general bilinear form.

Notation #

The orthogonal complement of a submodule K is denoted by Kᗮ.

The proposition that two submodules are orthogonal, Submodule.IsOrtho, is denoted by U ⟂ V. Note this is not the same unicode symbol as ⊥ (Bot).

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

Submodule 𝕜 E

The subspace of vectors orthogonal to a given subspace, denoted Kᗮ.

Equations

Kᗮ = { carrier := {v : E | ∀ u ∈ K, inner 𝕜 u v = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

Instances For

def Submodule.«term_ᗮ» :

Lean.TrailingParserDescr

The subspace of vectors orthogonal to a given subspace, denoted Kᗮ.

Equations

Submodule.«term_ᗮ» = Lean.ParserDescr.trailingNode `Submodule.«term_ᗮ» 1200 0 (Lean.ParserDescr.symbol "ᗮ")

Instances For

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

v ∈ Kᗮ ↔ ∀ u ∈ K, inner 𝕜 u v = 0

When a vector is in Kᗮ.

theorem Submodule.mem_orthogonal' {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) (v : E) :

v ∈ Kᗮ ↔ ∀ u ∈ K, inner 𝕜 v u = 0

When a vector is in Kᗮ, with the inner product the other way round.

theorem Submodule.inner_right_of_mem_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} {u v : E} (hu : u ∈ K) (hv : v ∈ Kᗮ) :

inner 𝕜 u v = 0

A vector in K is orthogonal to one in Kᗮ.

theorem Submodule.inner_left_of_mem_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} {u v : E} (hu : u ∈ K) (hv : v ∈ Kᗮ) :

inner 𝕜 v u = 0

A vector in Kᗮ is orthogonal to one in K.

theorem Submodule.mem_orthogonal_singleton_iff_inner_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {u v : E} :

v ∈ (𝕜 ∙ u)ᗮ ↔ inner 𝕜 u v = 0

A vector is in (𝕜 ∙ u)ᗮ iff it is orthogonal to u.

theorem Submodule.mem_orthogonal_singleton_iff_inner_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {u v : E} :

v ∈ (𝕜 ∙ u)ᗮ ↔ inner 𝕜 v u = 0

A vector in (𝕜 ∙ u)ᗮ is orthogonal to u.

theorem Submodule.sub_mem_orthogonal_of_inner_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} {x y : E} (h : ∀ (v : ↥K), inner 𝕜 x ↑v = inner 𝕜 y ↑v) :

x - y ∈ Kᗮ

theorem Submodule.sub_mem_orthogonal_of_inner_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} {x y : E} (h : ∀ (v : ↥K), inner 𝕜 (↑v) x = inner 𝕜 (↑v) y) :

x - y ∈ Kᗮ

theorem Submodule.inf_orthogonal_eq_bot {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) :

K ⊓ Kᗮ = ⊥

K and Kᗮ have trivial intersection.

theorem Submodule.orthogonal_disjoint {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) :

Disjoint K Kᗮ

K and Kᗮ have trivial intersection.

theorem Submodule.orthogonal_eq_inter {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) :

Kᗮ = ⨅ (v : ↥K), (↑((innerSL 𝕜) ↑v)).ker

Kᗮ can be characterized as the intersection of the kernels of the operations of inner product with each of the elements of K.

theorem Submodule.isClosed_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) :

IsClosed ↑Kᗮ

The orthogonal complement of any submodule K is closed.

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

CompleteSpace ↥Kᗮ

In a complete space, the orthogonal complement of any submodule K is complete.

theorem Submodule.map_orthogonal {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (K : Submodule 𝕜 E) (f : E →ₗᵢ[𝕜] F) :

map f.toLinearMap Kᗮ = (map f.toLinearMap K)ᗮ ⊓ f.range

theorem Submodule.map_orthogonal_equiv {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (K : Submodule 𝕜 E) (f : E ≃ₗᵢ[𝕜] F) :

map (↑f.toLinearEquiv) Kᗮ = (map (↑f.toLinearEquiv) K)ᗮ

theorem Submodule.orthogonal_gc (𝕜 : Type u_1) (E : Type u_2) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] :

GaloisConnection orthogonal orthogonal

orthogonal gives a GaloisConnection between Submodule 𝕜 E and its OrderDual.

theorem Submodule.orthogonal_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K₁ K₂ : Submodule 𝕜 E} (h : K₁ ≤ K₂) :

K₂ᗮ ≤ K₁ᗮ

orthogonal reverses the ≤ ordering of two subspaces.

theorem Submodule.orthogonal_orthogonal_monotone {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K₁ K₂ : Submodule 𝕜 E} (h : K₁ ≤ K₂) :

K₁ᗮ ᗮ ≤ K₂ᗮ ᗮ

orthogonal.orthogonal preserves the ≤ ordering of two subspaces.

theorem Submodule.le_orthogonal_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) :

K is contained in Kᗮᗮ.

theorem Submodule.inf_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K₁ K₂ : Submodule 𝕜 E) :

K₁ᗮ ⊓ K₂ᗮ = (K₁ ⊔ K₂)ᗮ

The inf of two orthogonal subspaces equals the subspace orthogonal to the sup.

theorem Submodule.iInf_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} (K : ι → Submodule 𝕜 E) :

⨅ (i : ι), (K i)ᗮ = (iSup K)ᗮ

The inf of an indexed family of orthogonal subspaces equals the subspace orthogonal to the sup.

theorem Submodule.sInf_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (s : Set (Submodule 𝕜 E)) :

⨅ K ∈ s, Kᗮ = (sSup s)ᗮ

The inf of a set of orthogonal subspaces equals the subspace orthogonal to the sup.

@[simp]

theorem Submodule.top_orthogonal_eq_bot {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] :

@[simp]

theorem Submodule.bot_orthogonal_eq_top {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] :

@[simp]

theorem Submodule.orthogonal_eq_top_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) :

Kᗮ = ⊤ ↔ K = ⊥

@[simp]

theorem Submodule.orthogonal_closure {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) :

K.topologicalClosureᗮ = Kᗮ

The closure of a submodule has the same orthogonal complement and the submodule itself.

theorem Submodule.orthogonal_closure' {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) (x : E) :

(∀ y ∈ K, inner 𝕜 y x = 0) ↔ ∀ y ∈ K.topologicalClosure, inner 𝕜 y x = 0

theorem Submodule.orthogonalFamily_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) :

OrthogonalFamily 𝕜 (fun (b : Bool) => ↥(bif b then K else Kᗮ)) fun (b : Bool) => (bif b then K else Kᗮ).subtypeₗᵢ

@[simp]

theorem orthogonalBilin_innerₗ {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : Submodule ℝ E) :

K.orthogonalBilin (innerₗ E) = Kᗮ

@[deprecated orthogonalBilin_innerₗ (since := "2025-12-26")]

theorem bilinFormOfRealInner_orthogonal {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : Submodule ℝ E) :

K.orthogonalBilin (innerₗ E) = Kᗮ

Alias of orthogonalBilin_innerₗ.

Orthogonality of submodules #

In this section we define Submodule.IsOrtho U V, denoted as U ⟂ V.

The API roughly matches that of Disjoint.

def Submodule.IsOrtho {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) :

The proposition that two submodules are orthogonal, denoted as U ⟂ V.

Equations

(U ⟂ V) = (U ≤ Vᗮ)

Instances For

def Submodule.«term_⟂_» :

Lean.TrailingParserDescr

The proposition that two submodules are orthogonal, denoted as U ⟂ V.

Equations

Submodule.«term_⟂_» = Lean.ParserDescr.trailingNode `Submodule.«term_⟂_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⟂ ") (Lean.ParserDescr.cat `term 51))

Instances For

theorem Submodule.isOrtho_iff_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U V : Submodule 𝕜 E} :

U ⟂ V ↔ U ≤ Vᗮ

theorem Submodule.IsOrtho.symm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U V : Submodule 𝕜 E} (h : U ⟂ V) :

V ⟂ U

theorem Submodule.isOrtho_comm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U V : Submodule 𝕜 E} :

U ⟂ V ↔ V ⟂ U

theorem Submodule.symmetric_isOrtho {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] :

Symmetric IsOrtho

theorem Submodule.IsOrtho.inner_eq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U V : Submodule 𝕜 E} (h : U ⟂ V) {u v : E} (hu : u ∈ U) (hv : v ∈ V) :

inner 𝕜 u v = 0

theorem Submodule.isOrtho_iff_inner_eq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U V : Submodule 𝕜 E} :

U ⟂ V ↔ ∀ u ∈ U, ∀ v ∈ V, inner 𝕜 u v = 0

@[simp]

theorem Submodule.isOrtho_bot_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {V : Submodule 𝕜 E} :

@[simp]

theorem Submodule.isOrtho_bot_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} :

theorem Submodule.IsOrtho.mono_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U₁ U₂ V : Submodule 𝕜 E} (hU : U₂ ≤ U₁) (h : U₁ ⟂ V) :

U₂ ⟂ V

theorem Submodule.IsOrtho.mono_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U V₁ V₂ : Submodule 𝕜 E} (hV : V₂ ≤ V₁) (h : U ⟂ V₁) :

U ⟂ V₂

theorem Submodule.IsOrtho.mono {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U₁ V₁ U₂ V₂ : Submodule 𝕜 E} (hU : U₂ ≤ U₁) (hV : V₂ ≤ V₁) (h : U₁ ⟂ V₁) :

U₂ ⟂ V₂

@[simp]

theorem Submodule.isOrtho_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} :

U ⟂ U ↔ U = ⊥

@[simp]

theorem Submodule.isOrtho_orthogonal_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) :

@[simp]

theorem Submodule.isOrtho_orthogonal_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) :

theorem Submodule.IsOrtho.le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U V : Submodule 𝕜 E} (h : U ⟂ V) :

theorem Submodule.IsOrtho.ge {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U V : Submodule 𝕜 E} (h : U ⟂ V) :

@[simp]

theorem Submodule.isOrtho_top_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} :

U ⟂ ⊤ ↔ U = ⊥

@[simp]

theorem Submodule.isOrtho_top_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {V : Submodule 𝕜 E} :

⊤ ⟂ V ↔ V = ⊥

theorem Submodule.IsOrtho.disjoint {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U V : Submodule 𝕜 E} (h : U ⟂ V) :

Orthogonal submodules are disjoint.

@[simp]

theorem Submodule.isOrtho_sup_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U₁ U₂ V : Submodule 𝕜 E} :

U₁ ⊔ U₂ ⟂ V ↔ U₁ ⟂ V ∧ U₂ ⟂ V

@[simp]

theorem Submodule.isOrtho_sup_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U V₁ V₂ : Submodule 𝕜 E} :

U ⟂ V₁ ⊔ V₂ ↔ U ⟂ V₁ ∧ U ⟂ V₂

@[simp]

theorem Submodule.isOrtho_sSup_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Set (Submodule 𝕜 E)} {V : Submodule 𝕜 E} :

sSup U ⟂ V ↔ ∀ Uᵢ ∈ U, Uᵢ ⟂ V

@[simp]

theorem Submodule.isOrtho_sSup_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} {V : Set (Submodule 𝕜 E)} :

U ⟂ sSup V ↔ ∀ Vᵢ ∈ V, U ⟂ Vᵢ

@[simp]

theorem Submodule.isOrtho_iSup_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Sort u_4} {U : ι → Submodule 𝕜 E} {V : Submodule 𝕜 E} :

iSup U ⟂ V ↔ ∀ (i : ι), U i ⟂ V

@[simp]

theorem Submodule.isOrtho_iSup_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Sort u_4} {U : Submodule 𝕜 E} {V : ι → Submodule 𝕜 E} :

U ⟂ iSup V ↔ ∀ (i : ι), U ⟂ V i

@[simp]

theorem Submodule.isOrtho_span {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {s t : Set E} :

span 𝕜 s ⟂ span 𝕜 t ↔ ∀ ⦃u : E⦄, u ∈ s → ∀ ⦃v : E⦄, v ∈ t → inner 𝕜 u v = 0

theorem Submodule.IsOrtho.map {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (f : E →ₗᵢ[𝕜] F) {U V : Submodule 𝕜 E} (h : U ⟂ V) :

Submodule.map (↑f) U ⟂ Submodule.map (↑f) V

theorem Submodule.IsOrtho.comap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (f : E →ₗᵢ[𝕜] F) {U V : Submodule 𝕜 F} (h : U ⟂ V) :

Submodule.comap (↑f) U ⟂ Submodule.comap (↑f) V

@[simp]

theorem Submodule.IsOrtho.map_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (f : E ≃ₗᵢ[𝕜] F) {U V : Submodule 𝕜 E} :

Submodule.map (↑↑f.toContinuousLinearEquiv) U ⟂ Submodule.map (↑↑f.toContinuousLinearEquiv) V ↔ U ⟂ V

@[simp]

theorem Submodule.IsOrtho.comap_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (f : E ≃ₗᵢ[𝕜] F) {U V : Submodule 𝕜 F} :

Submodule.comap (↑↑f.toContinuousLinearEquiv) U ⟂ Submodule.comap (↑↑f.toContinuousLinearEquiv) V ↔ U ⟂ V

theorem orthogonalFamily_iff_pairwise {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {V : ι → Submodule 𝕜 E} :

(OrthogonalFamily 𝕜 (fun (i : ι) => ↥(V i)) fun (i : ι) => (V i).subtypeₗᵢ) ↔ Pairwise (Function.onFun (fun (x1 x2 : Submodule 𝕜 E) => x1 ⟂ x2) V)

theorem OrthogonalFamily.of_pairwise {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {V : ι → Submodule 𝕜 E} :

Pairwise (Function.onFun (fun (x1 x2 : Submodule 𝕜 E) => x1 ⟂ x2) V) → OrthogonalFamily 𝕜 (fun (i : ι) => ↥(V i)) fun (i : ι) => (V i).subtypeₗᵢ

Alias of the reverse direction of orthogonalFamily_iff_pairwise.

theorem OrthogonalFamily.pairwise {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {V : ι → Submodule 𝕜 E} :

(OrthogonalFamily 𝕜 (fun (i : ι) => ↥(V i)) fun (i : ι) => (V i).subtypeₗᵢ) → Pairwise (Function.onFun (fun (x1 x2 : Submodule 𝕜 E) => x1 ⟂ x2) V)

Alias of the forward direction of orthogonalFamily_iff_pairwise.

theorem OrthogonalFamily.isOrtho {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {V : ι → Submodule 𝕜 E} (hV : OrthogonalFamily 𝕜 (fun (i : ι) => ↥(V i)) fun (i : ι) => (V i).subtypeₗᵢ) {i j : ι} (hij : i ≠ j) :

V i ⟂ V j

Two submodules in an orthogonal family with different indices are orthogonal.

def ClosedSubmodule.orthogonal {𝕜 : Type u_4} {E : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : ClosedSubmodule 𝕜 E) :

ClosedSubmodule 𝕜 E

The closed subspace of vectors orthogonal to a given subspace, denoted Kᗮ.

Equations

Kᗮ = { toSubmodule := (↑K)ᗮ, isClosed' := ⋯ }

Instances For

def ClosedSubmodule.«term_ᗮ» :

Lean.TrailingParserDescr

The closed subspace of vectors orthogonal to a given subspace, denoted Kᗮ.

Equations

ClosedSubmodule.«term_ᗮ» = Lean.ParserDescr.trailingNode `ClosedSubmodule.«term_ᗮ» 1200 0 (Lean.ParserDescr.symbol "ᗮ")

Instances For

@[simp]

theorem ClosedSubmodule.orthogonal_toSubmodule_eq {𝕜 : Type u_4} {E : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : ClosedSubmodule 𝕜 E) :

↑Kᗮ = (↑K)ᗮ

theorem ClosedSubmodule.mem_orthogonal_iff {𝕜 : Type u_4} {E : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : ClosedSubmodule 𝕜 E) (v : E) :

v ∈ (↑K)ᗮ ↔ v ∈ Kᗮ

@[simp]

theorem ClosedSubmodule.mem_orthogonal {𝕜 : Type u_4} {E : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : ClosedSubmodule 𝕜 E) (v : E) :

v ∈ Kᗮ ↔ ∀ u ∈ K, inner 𝕜 u v = 0

When a vector is in Kᗮ.

theorem ClosedSubmodule.mem_orthogonal' {𝕜 : Type u_4} {E : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : ClosedSubmodule 𝕜 E) (v : E) :

v ∈ Kᗮ ↔ ∀ u ∈ K, inner 𝕜 v u = 0

When a vector is in Kᗮ, with the inner product the other way round.

theorem ClosedSubmodule.sub_mem_orthogonal_of_inner_left {𝕜 : Type u_4} {E : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : ClosedSubmodule 𝕜 E} {x y : E} (h : ∀ (v : ↥K), inner 𝕜 x ↑v = inner 𝕜 y ↑v) :

x - y ∈ Kᗮ

theorem ClosedSubmodule.sub_mem_orthogonal_of_inner_right {𝕜 : Type u_4} {E : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : ClosedSubmodule 𝕜 E} {x y : E} (h : ∀ (v : ↥K), inner 𝕜 (↑v) x = inner 𝕜 (↑v) y) :

x - y ∈ Kᗮ

theorem ClosedSubmodule.inf_orthogonal_eq_bot {𝕜 : Type u_4} {E : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : ClosedSubmodule 𝕜 E) :

K ⊓ Kᗮ = ⊥

K and Kᗮ have trivial intersection.

theorem ClosedSubmodule.orthogonal_disjoint {𝕜 : Type u_4} {E : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : ClosedSubmodule 𝕜 E) :

Disjoint K Kᗮ

K and Kᗮ have trivial intersection.

theorem ClosedSubmodule.orthogonal_eq_inter {𝕜 : Type u_4} {E : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : ClosedSubmodule 𝕜 E) :

↑Kᗮ = ⨅ (v : ↥K), (↑((innerSL 𝕜) ↑v)).ker

Kᗮ can be characterized as the intersection of the kernels of the operations of inner product with each of the elements of K.

theorem ClosedSubmodule.orthogonal_gc (𝕜 : Type u_4) (E : Type u_5) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] :

GaloisConnection orthogonal orthogonal

orthogonal gives a GaloisConnection between ClosedSubmodule 𝕜 E and its OrderDual.

theorem ClosedSubmodule.orthogonal_le {𝕜 : Type u_4} {E : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K₁ K₂ : ClosedSubmodule 𝕜 E} (h : K₁ ≤ K₂) :

K₂ᗮ ≤ K₁ᗮ

orthogonal reverses the ≤ ordering of two subspaces.

theorem ClosedSubmodule.orthogonal_orthogonal_monotone {𝕜 : Type u_4} {E : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K₁ K₂ : ClosedSubmodule 𝕜 E} (h : K₁ ≤ K₂) :

K₁ᗮ ᗮ ≤ K₂ᗮ ᗮ

orthogonal.orthogonal preserves the ≤ ordering of two subspaces.

theorem ClosedSubmodule.inf_orthogonal {𝕜 : Type u_4} {E : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K₁ K₂ : ClosedSubmodule 𝕜 E) :

K₁ᗮ ⊓ K₂ᗮ = (K₁ ⊔ K₂)ᗮ

The inf of two orthogonal subspaces equals the subspace orthogonal to the sup.

theorem ClosedSubmodule.iInf_orthogonal {𝕜 : Type u_4} {E : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_7} (K : ι → ClosedSubmodule 𝕜 E) :

⨅ (i : ι), (K i)ᗮ = (iSup K)ᗮ

The inf of an indexed family of orthogonal subspaces equals the subspace orthogonal to the sup.

theorem ClosedSubmodule.sInf_orthogonal {𝕜 : Type u_4} {E : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (s : Set (ClosedSubmodule 𝕜 E)) :

⨅ K ∈ s, Kᗮ = (sSup s)ᗮ

The inf of a set of orthogonal subspaces equals the subspace orthogonal to the sup.

@[simp]

theorem ClosedSubmodule.top_orthogonal_eq_bot {𝕜 : Type u_4} {E : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] :

@[simp]

theorem ClosedSubmodule.bot_orthogonal_eq_top {𝕜 : Type u_4} {E : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] :

@[simp]

theorem ClosedSubmodule.orthogonal_eq_top_iff {𝕜 : Type u_4} {E : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : ClosedSubmodule 𝕜 E) :

Kᗮ = ⊤ ↔ K = ⊥

@[simp]

theorem ClosedSubmodule.orthogonal_closure {𝕜 : Type u_4} {E : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) :

(↑K.closure)ᗮ = Kᗮ

The orthogonal complement of the closure of a submodule (as a Submodule) is equal to the orthogonal complement.

theorem ClosedSubmodule.orthogonal_closure' {𝕜 : Type u_4} {E : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) :

K.closureᗮ = { toSubmodule := Kᗮ, isClosed' := ⋯ }

The orthogonal complement of the closure of a submodule (as a ClosedSubmodule) is equal to the orthogonal complement.

theorem ClosedSubmodule.orthogonal_closure'' {𝕜 : Type u_4} {E : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) :

K.closureᗮ = Kᗮ.closure

The orthogonal complement of the closure of a submodule (as a ClosedSubmodule) is equal to the closure of the orthogonal complement.