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

Equations

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

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 : E} {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 : E} {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 : E} {v : E} :

v ∈ (Submodule.span 𝕜 {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 : E} {v : E} :

v ∈ (Submodule.span 𝕜 {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 : E} {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 : E} {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), LinearMap.ker ((innerSL 𝕜) ↑v)

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.

Equations

⋯ = ⋯

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

GaloisConnection Submodule.orthogonal Submodule.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₁ : Submodule 𝕜 E} {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₁ : Submodule 𝕜 E} {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₁ : Submodule 𝕜 E) (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 = ⊥

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 bilinFormOfRealInner_orthogonal {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : Submodule ℝ E) :

K.orthogonalBilin bilinFormOfRealInner = Kᗮ

Orthogonality of submodules #

In this section we define Submodule.IsOrtho U V, with notation 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 : Submodule 𝕜 E) (V : Submodule 𝕜 E) :

The proposition that two submodules are orthogonal. Has notation U ⟂ V.

Equations

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

Instances For

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

U ⟂ V ↔ U ≤ Vᗮ

theorem Submodule.IsOrtho.symm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} {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 : Submodule 𝕜 E} {V : Submodule 𝕜 E} :

U ⟂ V ↔ V ⟂ U

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

Symmetric Submodule.IsOrtho

theorem Submodule.IsOrtho.inner_eq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} {V : Submodule 𝕜 E} (h : U ⟂ V) {u : E} {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 : Submodule 𝕜 E} {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₁ : Submodule 𝕜 E} {U₂ : Submodule 𝕜 E} {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 : Submodule 𝕜 E} {V₁ : Submodule 𝕜 E} {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₁ : Submodule 𝕜 E} {V₁ : Submodule 𝕜 E} {U₂ : Submodule 𝕜 E} {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 : Submodule 𝕜 E} {V : Submodule 𝕜 E} (h : U ⟂ V) :

theorem Submodule.IsOrtho.ge {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} {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 : Submodule 𝕜 E} {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₁ : Submodule 𝕜 E} {U₂ : Submodule 𝕜 E} {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 : Submodule 𝕜 E} {V₁ : Submodule 𝕜 E} {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 : Set E} {t : Set E} :

Submodule.span 𝕜 s ⟂ Submodule.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 : Submodule 𝕜 E} {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 : Submodule 𝕜 F} {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 : Submodule 𝕜 E} {V : Submodule 𝕜 E} :

Submodule.map f U ⟂ Submodule.map f 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 : Submodule 𝕜 F} {V : Submodule 𝕜 F} :

Submodule.comap f U ⟂ Submodule.comap f 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 ((fun (x1 x2 : Submodule 𝕜 E) => x1 ⟂ x2) on V)

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

Pairwise ((fun (x1 x2 : Submodule 𝕜 E) => x1 ⟂ x2) on 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 ((fun (x1 x2 : Submodule 𝕜 E) => x1 ⟂ x2) on 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.