mathlib3 documentation

analysis.inner_product_space.orthogonal

Orthogonal complements of submodules #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

See also bilin_form.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.is_ortho, is denoted by U ⟂ V. Note this is not the same unicode symbol as ⊥ (has_bot).

source
def submodule.orthogonal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) :
submodule 𝕜 E

The subspace of vectors orthogonal to a given subspace.

Equations
Instances for ↥submodule.orthogonal
source
theorem submodule.mem_orthogonal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) (v : E) :
v ∈ Kᗮ ↔ ∀ (u : E), u ∈ K → has_inner.inner u v = 0

When a vector is in Kᗮ.

source
theorem submodule.mem_orthogonal' {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) (v : E) :
v ∈ Kᗮ ↔ ∀ (u : E), u ∈ K → has_inner.inner v u = 0

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

source
theorem submodule.inner_right_of_mem_orthogonal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} {u v : E} (hu : u ∈ K) (hv : v ∈ Kᗮ) :
has_inner.inner u v = 0

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

source
theorem submodule.inner_left_of_mem_orthogonal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} {u v : E} (hu : u ∈ K) (hv : v ∈ Kᗮ) :
has_inner.inner v u = 0

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

source
theorem submodule.mem_orthogonal_singleton_iff_inner_right {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {u v : E} :
v ∈ (submodule.span 𝕜 {u})ᗮ ↔ has_inner.inner u v = 0

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

source
theorem submodule.mem_orthogonal_singleton_iff_inner_left {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {u v : E} :
v ∈ (submodule.span 𝕜 {u})ᗮ ↔ has_inner.inner v u = 0

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

source
theorem submodule.sub_mem_orthogonal_of_inner_left {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} {x y : E} (h : ∀ (v : ↥K), has_inner.inner x ↑v = has_inner.inner y ↑v) :
x - y ∈ Kᗮ
source
theorem submodule.sub_mem_orthogonal_of_inner_right {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} {x y : E} (h : ∀ (v : ↥K), has_inner.inner ↑v x = has_inner.inner ↑v y) :
x - y ∈ Kᗮ
source
theorem submodule.inf_orthogonal_eq_bot {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) :
K ⊓ Kᗮ = ⊥

K and Kᗮ have trivial intersection.

source
theorem submodule.orthogonal_disjoint {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) :
disjoint K Kᗮ

K and Kᗮ have trivial intersection.

source
theorem submodule.orthogonal_eq_inter {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) :
Kᗮ = ⨅ (v : ↥K), linear_map.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.

source
theorem submodule.is_closed_orthogonal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) :
is_closed ↑Kᗮ

The orthogonal complement of any submodule K is closed.

source
@[protected, instance]
def submodule.orthogonal.complete_space {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) [complete_space E] :
complete_space ↥Kᗮ

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

source
theorem submodule.orthogonal_gc (𝕜 : Type u_1) (E : Type u_2) [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] :
galois_connection submodule.orthogonal submodule.orthogonal

orthogonal gives a galois_connection between submodule 𝕜 E and its order_dual.

source
theorem submodule.orthogonal_le {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {K₁ K₂ : submodule 𝕜 E} (h : K₁ ≤ K₂) :
K₂ᗮ ≤ K₁ᗮ

orthogonal reverses the ≤ ordering of two subspaces.

source
theorem submodule.orthogonal_orthogonal_monotone {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {K₁ K₂ : submodule 𝕜 E} (h : K₁ ≤ K₂) :
K₁ᗮᗮ ≤ K₂ᗮᗮ

orthogonal.orthogonal preserves the ≤ ordering of two subspaces.

source
theorem submodule.le_orthogonal_orthogonal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) :
K ≤ Kᗮᗮ

K is contained in Kᗮᗮ.

source
theorem submodule.inf_orthogonal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] (K₁ K₂ : submodule 𝕜 E) :
K₁ᗮ ⊓ K₂ᗮ = (K₁ ⊔ K₂)ᗮ

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

source
theorem submodule.infi_orthogonal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {ι : Type u_3} (K : ι → submodule 𝕜 E) :
(⨅ (i : ι), (K i)ᗮ) = (supr K)ᗮ

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

source
theorem submodule.Inf_orthogonal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] (s : set (submodule 𝕜 E)) :
(⨅ (K : submodule 𝕜 E) (H : K ∈ s), Kᗮ) = (has_Sup.Sup s)ᗮ

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

source
@[simp]
theorem submodule.top_orthogonal_eq_bot {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] :
⊤ᗮ = ⊥
source
@[simp]
theorem submodule.bot_orthogonal_eq_top {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] :
⊥ᗮ = ⊤
source
@[simp]
theorem submodule.orthogonal_eq_top_iff {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) :
Kᗮ = ⊤ ↔ K = ⊥
source
theorem submodule.orthogonal_family_self {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) :
orthogonal_family 𝕜 (λ (b : bool), ↥(cond b K Kᗮ)) (λ (b : bool), (cond b K Kᗮ).subtypeₗᵢ)
source
@[simp]
theorem bilin_form_of_real_inner_orthogonal {E : Type u_1} [normed_add_comm_group E] [inner_product_space ℝ E] (K : submodule ℝ E) :
bilin_form_of_real_inner.orthogonal K = Kᗮ

Orthogonality of submodules #

In this section we define submodule.is_ortho U V, with notation U ⟂ V.

The API roughly matches that of disjoint.

source
def submodule.is_ortho {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] (U V : submodule 𝕜 E) :
Prop

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

Equations
source
theorem submodule.is_ortho_iff_le {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {U V : submodule 𝕜 E} :
U ⟂ V ↔ U ≤ Vᗮ
source
@[symm]
theorem submodule.is_ortho.symm {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {U V : submodule 𝕜 E} (h : U ⟂ V) :
V ⟂ U
source
theorem submodule.is_ortho_comm {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {U V : submodule 𝕜 E} :
U ⟂ V ↔ V ⟂ U
source
theorem submodule.symmetric_is_ortho {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] :
symmetric submodule.is_ortho
source
theorem submodule.is_ortho.inner_eq {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {U V : submodule 𝕜 E} (h : U ⟂ V) {u v : E} (hu : u ∈ U) (hv : v ∈ V) :
has_inner.inner u v = 0
source
theorem submodule.is_ortho_iff_inner_eq {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {U V : submodule 𝕜 E} :
U ⟂ V ↔ ∀ (u : E), u ∈ U → ∀ (v : E), v ∈ V → has_inner.inner u v = 0
source
@[simp]
theorem submodule.is_ortho_bot_left {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {V : submodule 𝕜 E} :
⊥ ⟂ V
source
@[simp]
theorem submodule.is_ortho_bot_right {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {U : submodule 𝕜 E} :
U ⟂ ⊥
source
theorem submodule.is_ortho.mono_left {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {U₁ U₂ V : submodule 𝕜 E} (hU : U₂ ≤ U₁) (h : U₁ ⟂ V) :
U₂ ⟂ V
source
theorem submodule.is_ortho.mono_right {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {U V₁ V₂ : submodule 𝕜 E} (hV : V₂ ≤ V₁) (h : U ⟂ V₁) :
U ⟂ V₂
source
theorem submodule.is_ortho.mono {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {U₁ V₁ U₂ V₂ : submodule 𝕜 E} (hU : U₂ ≤ U₁) (hV : V₂ ≤ V₁) (h : U₁ ⟂ V₁) :
U₂ ⟂ V₂
source
@[simp]
theorem submodule.is_ortho_self {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {U : submodule 𝕜 E} :
U ⟂ U ↔ U = ⊥
source
@[simp]
theorem submodule.is_ortho_orthogonal_right {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] (U : submodule 𝕜 E) :
U ⟂ Uᗮ
source
@[simp]
theorem submodule.is_ortho_orthogonal_left {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] (U : submodule 𝕜 E) :
Uᗮ ⟂ U
source
theorem submodule.is_ortho.le {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {U V : submodule 𝕜 E} (h : U ⟂ V) :
U ≤ Vᗮ
source
theorem submodule.is_ortho.ge {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {U V : submodule 𝕜 E} (h : U ⟂ V) :
V ≤ Uᗮ
source
@[simp]
theorem submodule.is_ortho_top_right {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {U : submodule 𝕜 E} :
U ⟂ ⊤ ↔ U = ⊥
source
@[simp]
theorem submodule.is_ortho_top_left {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {V : submodule 𝕜 E} :
⊤ ⟂ V ↔ V = ⊥
source
theorem submodule.is_ortho.disjoint {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {U V : submodule 𝕜 E} (h : U ⟂ V) :
disjoint U V

Orthogonal submodules are disjoint.

source
@[simp]
theorem submodule.is_ortho_sup_left {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {U₁ U₂ V : submodule 𝕜 E} :
U₁ ⊔ U₂ ⟂ V ↔ U₁ ⟂ V ∧ U₂ ⟂ V
source
@[simp]
theorem submodule.is_ortho_sup_right {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {U V₁ V₂ : submodule 𝕜 E} :
U ⟂ V₁ ⊔ V₂ ↔ U ⟂ V₁ ∧ U ⟂ V₂
source
@[simp]
theorem submodule.is_ortho_Sup_left {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {U : set (submodule 𝕜 E)} {V : submodule 𝕜 E} :
has_Sup.Sup U ⟂ V ↔ ∀ (Uᵢ : submodule 𝕜 E), Uᵢ ∈ U → Uᵢ ⟂ V
source
@[simp]
theorem submodule.is_ortho_Sup_right {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {U : submodule 𝕜 E} {V : set (submodule 𝕜 E)} :
U ⟂ has_Sup.Sup V ↔ ∀ (Vᵢ : submodule 𝕜 E), Vᵢ ∈ V → U ⟂ Vᵢ
source
@[simp]
theorem submodule.is_ortho_supr_left {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {ι : Sort u_3} {U : ι → submodule 𝕜 E} {V : submodule 𝕜 E} :
supr U ⟂ V ↔ ∀ (i : ι), U i ⟂ V
source
@[simp]
theorem submodule.is_ortho_supr_right {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {ι : Sort u_3} {U : submodule 𝕜 E} {V : ι → submodule 𝕜 E} :
U ⟂ supr V ↔ ∀ (i : ι), U ⟂ V i
source
@[simp]
theorem submodule.is_ortho_span {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {s t : set E} :
submodule.span 𝕜 s ⟂ submodule.span 𝕜 t ↔ ∀ ⦃u : E⦄, u ∈ s → ∀ ⦃v : E⦄, v ∈ t → has_inner.inner u v = 0
source
theorem submodule.is_ortho.map {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] [normed_add_comm_group F] [inner_product_space 𝕜 F] (f : E →ₗᵢ[𝕜] F) {U V : submodule 𝕜 E} (h : U ⟂ V) :
submodule.map f U ⟂ submodule.map f V
source
theorem submodule.is_ortho.comap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] [normed_add_comm_group F] [inner_product_space 𝕜 F] (f : E →ₗᵢ[𝕜] F) {U V : submodule 𝕜 F} (h : U ⟂ V) :
submodule.comap f U ⟂ submodule.comap f V
source
@[simp]
theorem submodule.is_ortho.map_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] [normed_add_comm_group F] [inner_product_space 𝕜 F] (f : E ≃ₗᵢ[𝕜] F) {U V : submodule 𝕜 E} :
submodule.map f U ⟂ submodule.map f V ↔ U ⟂ V
source
@[simp]
theorem submodule.is_ortho.comap_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] [normed_add_comm_group F] [inner_product_space 𝕜 F] (f : E ≃ₗᵢ[𝕜] F) {U V : submodule 𝕜 F} :
submodule.comap f U ⟂ submodule.comap f V ↔ U ⟂ V
source
theorem orthogonal_family_iff_pairwise {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {ι : Type u_3} {V : ι → submodule 𝕜 E} :
orthogonal_family 𝕜 (λ (i : ι), ↥(V i)) (λ (i : ι), (V i).subtypeₗᵢ) ↔ pairwise (submodule.is_ortho on V)
source
theorem orthogonal_family.of_pairwise {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {ι : Type u_3} {V : ι → submodule 𝕜 E} :
pairwise (submodule.is_ortho on V) → orthogonal_family 𝕜 (λ (i : ι), ↥(V i)) (λ (i : ι), (V i).subtypeₗᵢ)

Alias of the reverse direction of orthogonal_family_iff_pairwise.

source
theorem orthogonal_family.pairwise {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {ι : Type u_3} {V : ι → submodule 𝕜 E} :
orthogonal_family 𝕜 (λ (i : ι), ↥(V i)) (λ (i : ι), (V i).subtypeₗᵢ) → pairwise (submodule.is_ortho on V)

Alias of the forward direction of orthogonal_family_iff_pairwise.

source
theorem orthogonal_family.is_ortho {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {ι : Type u_3} {V : ι → submodule 𝕜 E} (hV : orthogonal_family 𝕜 (λ (i : ι), ↥(V i)) (λ (i : ι), (V i).subtypeₗᵢ)) {i j : ι} (hij : i ≠ j) :
V i ⟂ V j

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