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

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

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.

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) :

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

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) :

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

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

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

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
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
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 and Kᗮ have trivial intersection.

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) :

K and Kᗮ have trivial intersection.

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ᗮ can be characterized as the intersection of the kernels of the operations of inner product with each of the elements of K.

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) :

The orthogonal complement of any submodule K is closed.

@[protected, instance]

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

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.

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.

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 is contained in Kᗮᗮ.

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.

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.

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.

@[simp]
@[simp]
@[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) :
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ₗᵢ)

Orthogonality of submodules #

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

The API roughly matches that of disjoint.

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
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
@[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
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
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) :
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
@[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} :
@[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} :
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
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₂
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₂
@[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 =
@[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
@[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
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
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
@[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} :
@[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} :
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) :

Orthogonal submodules are disjoint.

@[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
@[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₂
@[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
@[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ᵢ
@[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
@[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
@[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
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) :
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) :
@[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} :
@[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} :
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)
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.

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.

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.