analysis.inner_product_space.projection

source

theorem exists_norm_eq_infi_of_complete_convex {F : Type u_3} [inner_product_space ℝ F] {K : set F} (ne : K.nonempty) (h₁ : is_complete K) (h₂ : convex ℝ K) (u : F) :

∃ (v : F) (H : v ∈ K), ∥u - v∥ = ⨅ (w : ↥K), ∥u - ↑w∥

Existence of minimizers Let u be a point in a real inner product space, and let K be a nonempty complete convex subset. Then there exists a (unique) v in K that minimizes the distance ∥u - v∥ to u.

source

theorem norm_eq_infi_iff_real_inner_le_zero {F : Type u_3} [inner_product_space ℝ F] {K : set F} (h : convex ℝ K) {u v : F} (hv : v ∈ K) :

(∥u - v∥ = ⨅ (w : ↥K), ∥u - ↑w∥) ↔ ∀ (w : F), w ∈ K → has_inner.inner (u - v) (w - v) ≤ 0

Characterization of minimizers for the projection on a convex set in a real inner product space.

source

theorem exists_norm_eq_infi_of_complete_subspace {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) (h : is_complete ↑K) (u : E) :

∃ (v : E) (H : v ∈ K), ∥u - v∥ = ⨅ (w : ↥↑K), ∥u - ↑w∥

Existence of projections on complete subspaces. Let u be a point in an inner product space, and let K be a nonempty complete subspace. Then there exists a (unique) v in K that minimizes the distance ∥u - v∥ to u. This point v is usually called the orthogonal projection of u onto K.

source

theorem norm_eq_infi_iff_real_inner_eq_zero {F : Type u_3} [inner_product_space ℝ F] (K : submodule ℝ F) {u v : F} (hv : v ∈ K) :

(∥u - v∥ = ⨅ (w : ↥↑K), ∥u - ↑w∥) ↔ ∀ (w : F), w ∈ K → has_inner.inner (u - v) w = 0

Characterization of minimizers in the projection on a subspace, in the real case. Let u be a point in a real inner product space, and let K be a nonempty subspace. Then point v minimizes the distance ∥u - v∥ over points in K if and only if for all w ∈ K, ⟪u - v, w⟫ = 0 (i.e., u - v is orthogonal to the subspace K). This is superceded by norm_eq_infi_iff_inner_eq_zero that gives the same conclusion over any is_R_or_C field.

source

theorem norm_eq_infi_iff_inner_eq_zero {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) {u v : E} (hv : v ∈ K) :

(∥u - v∥ = ⨅ (w : ↥K), ∥u - ↑w∥) ↔ ∀ (w : E), w ∈ K → has_inner.inner (u - v) w = 0

Characterization of minimizers in the projection on a subspace. Let u be a point in an inner product space, and let K be a nonempty subspace. Then point v minimizes the distance ∥u - v∥ over points in K if and only if for all w ∈ K, ⟪u - v, w⟫ = 0 (i.e., u - v is orthogonal to the subspace K)

source

noncomputable def orthogonal_projection_fn {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) [complete_space ↥K] (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 orthogonal_projection and should not be used once that is defined.

Equations

orthogonal_projection_fn K v = _.some

source

theorem orthogonal_projection_fn_mem {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} [complete_space ↥K] (v : E) :

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

source

theorem orthogonal_projection_fn_inner_eq_zero {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} [complete_space ↥K] (v w : E) (H : w ∈ K) :

has_inner.inner (v - orthogonal_projection_fn K 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.

source

theorem eq_orthogonal_projection_fn_of_mem_of_inner_eq_zero {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} [complete_space ↥K] {u v : E} (hvm : v ∈ K) (hvo : ∀ (w : E), w ∈ K → has_inner.inner (u - v) w = 0) :

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

source

theorem orthogonal_projection_fn_norm_sq {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) [complete_space ↥K] (v : E) :

∥v∥ * ∥v∥ = ∥v - orthogonal_projection_fn K v∥ * ∥v - orthogonal_projection_fn K v∥ + ∥orthogonal_projection_fn K v∥ * ∥orthogonal_projection_fn K v∥

source

noncomputable def orthogonal_projection {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) [complete_space ↥K] :

E →L[𝕜] ↥K

The orthogonal projection onto a complete subspace.

Equations

orthogonal_projection K = {to_fun := λ (v : E), ⟨orthogonal_projection_fn K v, _⟩, map_add' := _, map_smul' := _}.mk_continuous 1 _

source

@[simp]

theorem orthogonal_projection_fn_eq {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} [complete_space ↥K] (v : E) :

orthogonal_projection_fn K v = ↑(⇑(orthogonal_projection K) v)

source

@[simp]

theorem orthogonal_projection_inner_eq_zero {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} [complete_space ↥K] (v w : E) (H : w ∈ K) :

has_inner.inner (v - ↑(⇑(orthogonal_projection K) v)) w = 0

The characterization of the orthogonal projection.

source

@[simp]

theorem sub_orthogonal_projection_mem_orthogonal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} [complete_space ↥K] (v : E) :

v - ↑(⇑(orthogonal_projection K) v) ∈ Kᗮ

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

source

theorem eq_orthogonal_projection_of_mem_of_inner_eq_zero {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} [complete_space ↥K] {u v : E} (hvm : v ∈ K) (hvo : ∀ (w : E), w ∈ K → has_inner.inner (u - v) w = 0) :

↑(⇑(orthogonal_projection K) u) = v

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

source

theorem orthogonal_projection_minimal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {U : submodule 𝕜 E} [complete_space ↥U] (y : E) :

∥y - ↑(⇑(orthogonal_projection U) y)∥ = ⨅ (x : ↥U), ∥y - ↑x∥

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

source

theorem eq_orthogonal_projection_of_eq_submodule {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} [complete_space ↥K] {K' : submodule 𝕜 E} [complete_space ↥K'] (h : K = K') (u : E) :

↑(⇑(orthogonal_projection K) u) = ↑(⇑(orthogonal_projection K') u)

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

source

@[simp]

theorem orthogonal_projection_mem_subspace_eq_self {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} [complete_space ↥K] (v : ↥K) :

⇑(orthogonal_projection K) ↑v = v

The orthogonal projection sends elements of K to themselves.

source

theorem orthogonal_projection_eq_self_iff {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} [complete_space ↥K] {v : E} :

↑(⇑(orthogonal_projection K) v) = v ↔ v ∈ K

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

source

theorem linear_isometry.map_orthogonal_projection {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} {E' : Type u_3} [inner_product_space 𝕜 E] [inner_product_space 𝕜 E'] (f : E →ₗᵢ[𝕜] E') (p : submodule 𝕜 E) [complete_space ↥p] (x : E) :

⇑f ↑(⇑(orthogonal_projection p) x) = ↑(⇑(orthogonal_projection (submodule.map f.to_linear_map p)) (⇑f x))

source

theorem linear_isometry.map_orthogonal_projection' {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} {E' : Type u_3} [inner_product_space 𝕜 E] [inner_product_space 𝕜 E'] (f : E →ₗᵢ[𝕜] E') (p : submodule 𝕜 E) [complete_space ↥p] (x : E) :

⇑f ↑(⇑(orthogonal_projection p) x) = ↑(⇑(orthogonal_projection (submodule.map f p)) (⇑f x))

source

theorem orthogonal_projection_map_apply {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} {E' : Type u_3} [inner_product_space 𝕜 E] [inner_product_space 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E') (p : submodule 𝕜 E) [complete_space ↥p] (x : E') :

↑(⇑(orthogonal_projection (submodule.map ↑(f.to_linear_equiv) p)) x) = ⇑f ↑(⇑(orthogonal_projection p) (⇑(f.symm) x))

Orthogonal projection onto the submodule.map of a subspace.

source

@[simp]

theorem orthogonal_projection_bot {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] :

orthogonal_projection ⊥ = 0

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

source

theorem orthogonal_projection_norm_le {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) [complete_space ↥K] :

∥orthogonal_projection K∥ ≤ 1

The orthogonal projection has norm ≤ 1.

source

theorem smul_orthogonal_projection_singleton (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {v : E} (w : E) :

↑∥v∥ ^ 2 • ↑(⇑(orthogonal_projection (submodule.span 𝕜 {v})) w) = has_inner.inner v w • v

source

theorem orthogonal_projection_singleton (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {v : E} (w : E) :

↑(⇑(orthogonal_projection (submodule.span 𝕜 {v})) w) = (has_inner.inner v w / ↑∥v∥ ^ 2) • v

Formula for orthogonal projection onto a single vector.

source

theorem orthogonal_projection_unit_singleton (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {v : E} (hv : ∥v∥ = 1) (w : E) :

↑(⇑(orthogonal_projection (submodule.span 𝕜 {v})) w) = has_inner.inner v w • v

Formula for orthogonal projection onto a single unit vector.

source

noncomputable def reflection_linear_equiv {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) [complete_space ↥K] :

E ≃ₗ[𝕜] E

Auxiliary definition for reflection: the reflection as a linear equivalence.

Equations

reflection_linear_equiv K = linear_equiv.of_involutive (bit0 (K.subtype.comp (orthogonal_projection K).to_linear_map) - linear_map.id) _

source

noncomputable def reflection {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) [complete_space ↥K] :

E ≃ₗᵢ[𝕜] E

Reflection in a complete subspace of an inner product space. The word "reflection" is sometimes understood to mean specifically reflection in a codimension-one subspace, and sometimes more generally to cover operations such as reflection in a point. The definition here, of reflection in a subspace, is a more general sense of the word that includes both those common cases.

Equations

reflection K = {to_linear_equiv := {to_fun := (reflection_linear_equiv K).to_fun, map_add' := _, map_smul' := _, inv_fun := (reflection_linear_equiv K).inv_fun, left_inv := _, right_inv := _}, norm_map' := _}

source

theorem reflection_apply {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} [complete_space ↥K] (p : E) :

⇑(reflection K) p = bit0 ↑(⇑(orthogonal_projection K) p) - p

The result of reflecting.

source

@[simp]

theorem reflection_symm {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} [complete_space ↥K] :

(reflection K).symm = reflection K

Reflection is its own inverse.

source

@[simp]

theorem reflection_inv {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} [complete_space ↥K] :

(reflection K)⁻¹ = reflection K

Reflection is its own inverse.

source

@[simp]

theorem reflection_reflection {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) [complete_space ↥K] (p : E) :

⇑(reflection K) (⇑(reflection K) p) = p

Reflecting twice in the same subspace.

source

theorem reflection_involutive {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) [complete_space ↥K] :

function.involutive ⇑(reflection K)

Reflection is involutive.

source

@[simp]

theorem reflection_trans_reflection {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) [complete_space ↥K] :

(reflection K).trans (reflection K) = linear_isometry_equiv.refl 𝕜 E

Reflection is involutive.

source

@[simp]

theorem reflection_mul_reflection {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) [complete_space ↥K] :

reflection K * reflection K = 1

Reflection is involutive.

source

theorem reflection_eq_self_iff {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} [complete_space ↥K] (x : E) :

⇑(reflection K) x = x ↔ x ∈ K

A point is its own reflection if and only if it is in the subspace.

source

theorem reflection_mem_subspace_eq_self {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} [complete_space ↥K] {x : E} (hx : x ∈ K) :

⇑(reflection K) x = x

source

theorem reflection_map_apply {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} {E' : Type u_3} [inner_product_space 𝕜 E] [inner_product_space 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E') (K : submodule 𝕜 E) [complete_space ↥K] (x : E') :

⇑(reflection (submodule.map ↑(f.to_linear_equiv) K)) x = ⇑f (⇑(reflection K) (⇑(f.symm) x))

Reflection in the submodule.map of a subspace.

source

theorem reflection_map {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} {E' : Type u_3} [inner_product_space 𝕜 E] [inner_product_space 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E') (K : submodule 𝕜 E) [complete_space ↥K] :

reflection (submodule.map ↑(f.to_linear_equiv) K) = f.symm.trans ((reflection K).trans f)

Reflection in the submodule.map of a subspace.

source

@[simp]

theorem reflection_bot {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] :

reflection ⊥ = linear_isometry_equiv.neg 𝕜

Reflection through the trivial subspace {0} is just negation.

source

theorem submodule.sup_orthogonal_inf_of_complete_space {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K₁ K₂ : submodule 𝕜 E} (h : K₁ ≤ K₂) [complete_space ↥K₁] :

K₁ ⊔ K₁ᗮ ⊓ K₂ = K₂

If K₁ is complete and contained in K₂, K₁ and K₁ᗮ ⊓ K₂ span K₂.

source

theorem submodule.sup_orthogonal_of_complete_space {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} [complete_space ↥K] :

K ⊔ Kᗮ = ⊤

If K is complete, K and Kᗮ span the whole space.

source

theorem submodule.exists_sum_mem_mem_orthogonal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) [complete_space ↥K] (v : E) :

∃ (y : E) (H : y ∈ K) (z : E) (H : 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ᗮ.

source

@[simp]

theorem submodule.orthogonal_orthogonal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) [complete_space ↥K] :

Kᗮ ᗮ = K

If K is complete, then the orthogonal complement of its orthogonal complement is itself.

source

theorem submodule.orthogonal_orthogonal_eq_closure {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) [complete_space E] :

Kᗮ ᗮ = K.topological_closure

source

theorem submodule.is_compl_orthogonal_of_complete_space {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} [complete_space ↥K] :

is_compl K Kᗮ

If K is complete, K and Kᗮ are complements of each other.

source

@[simp]

theorem submodule.orthogonal_eq_bot_iff {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} [complete_space ↥↑K] :

Kᗮ = ⊥ ↔ K = ⊤

source

theorem eq_orthogonal_projection_of_mem_orthogonal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} [complete_space ↥K] {u v : E} (hv : v ∈ K) (hvo : u - v ∈ Kᗮ) :

↑(⇑(orthogonal_projection K) u) = v

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

source

theorem eq_orthogonal_projection_of_mem_orthogonal' {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} [complete_space ↥K] {u v z : E} (hv : v ∈ K) (hz : z ∈ Kᗮ) (hu : u = v + z) :

↑(⇑(orthogonal_projection K) u) = v

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

source

theorem orthogonal_projection_mem_subspace_orthogonal_complement_eq_zero {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} [complete_space ↥K] {v : E} (hv : v ∈ Kᗮ) :

⇑(orthogonal_projection K) v = 0

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

source

theorem reflection_mem_subspace_orthogonal_complement_eq_neg {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} [complete_space ↥K] {v : E} (hv : v ∈ Kᗮ) :

⇑(reflection K) v = -v

The reflection in K of an element of Kᗮ is its negation.

source

theorem orthogonal_projection_mem_subspace_orthogonal_precomplement_eq_zero {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} [complete_space E] {v : E} (hv : v ∈ K) :

⇑(orthogonal_projection Kᗮ) v = 0

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

source

theorem orthogonal_projection_orthogonal_projection_of_le {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {U V : submodule 𝕜 E} [complete_space ↥U] [complete_space ↥V] (h : U ≤ V) (x : E) :

⇑(orthogonal_projection U) ↑(⇑(orthogonal_projection V) x) = ⇑(orthogonal_projection U) x

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

source

theorem orthogonal_projection_tendsto_closure_supr {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [complete_space E] {ι : Type u_3} [semilattice_sup ι] (U : ι → submodule 𝕜 E) [∀ (i : ι), complete_space ↥(U i)] (hU : monotone U) (x : E) :

filter.tendsto (λ (i : ι), ↑(⇑(orthogonal_projection (U i)) x)) filter.at_top (nhds ↑(⇑(orthogonal_projection (⨆ (i : ι), U i).topological_closure) x))

Given a monotone family U of complete submodules of E and a fixed x : E, the orthogonal projection of x on U i tends to the orthogonal projection of x on (⨆ i, U i).topological_closure along at_top.

source

theorem orthogonal_projection_tendsto_self {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [complete_space E] {ι : Type u_3} [semilattice_sup ι] (U : ι → submodule 𝕜 E) [∀ (t : ι), complete_space ↥(U t)] (hU : monotone U) (x : E) (hU' : ⊤ ≤ (⨆ (t : ι), U t).topological_closure) :

filter.tendsto (λ (t : ι), ↑(⇑(orthogonal_projection (U t)) x)) filter.at_top (nhds x)

Given a monotone family U of complete submodules of E with dense span supremum, and a fixed x : E, the orthogonal projection of x on U i tends to x along at_top.

source

theorem submodule.triorthogonal_eq_orthogonal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} [complete_space E] :

Kᗮ ᗮ ᗮ = Kᗮ

The orthogonal complement satisfies Kᗮᗮᗮ = Kᗮ.

source

theorem submodule.topological_closure_eq_top_iff {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} [complete_space E] :

K.topological_closure = ⊤ ↔ Kᗮ = ⊥

The closure of K is the full space iff Kᗮ is trivial.

source

theorem reflection_mem_subspace_orthogonal_precomplement_eq_neg {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K : submodule 𝕜 E} [complete_space E] {v : E} (hv : v ∈ K) :

⇑(reflection Kᗮ) v = -v

The reflection in Kᗮ of an element of K is its negation.

source

theorem orthogonal_projection_orthogonal_complement_singleton_eq_zero {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [complete_space E] (v : E) :

⇑(orthogonal_projection (submodule.span 𝕜 {v})ᗮ) v = 0

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

source

theorem reflection_orthogonal_complement_singleton_eq_neg {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [complete_space E] (v : E) :

⇑(reflection (submodule.span 𝕜 {v})ᗮ) v = -v

The reflection in (𝕜 ∙ v)ᗮ of v is -v.

source

theorem reflection_sub {F : Type u_3} [inner_product_space ℝ F] [complete_space F] {v w : F} (h : ∥v∥ = ∥w∥) :

⇑(reflection (submodule.span ℝ {v - w})ᗮ) v = w

source

theorem eq_sum_orthogonal_projection_self_orthogonal_complement {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) [complete_space E] [complete_space ↥K] (w : E) :

w = ↑(⇑(orthogonal_projection K) w) + ↑(⇑(orthogonal_projection Kᗮ) w)

In a complete space E, a vector splits as the sum of its orthogonal projections onto a complete submodule K and onto the orthogonal complement of K.

source

theorem norm_sq_eq_add_norm_sq_projection {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (x : E) (S : submodule 𝕜 E) [complete_space E] [complete_space ↥S] :

∥x∥ ^ 2 = ∥⇑(orthogonal_projection S) x∥ ^ 2 + ∥⇑(orthogonal_projection Sᗮ) x∥ ^ 2

The Pythagorean theorem, for an orthogonal projection.

source

theorem id_eq_sum_orthogonal_projection_self_orthogonal_complement {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) [complete_space E] [complete_space ↥K] :

continuous_linear_map.id 𝕜 E = K.subtypeL.comp (orthogonal_projection K) + Kᗮ.subtypeL.comp (orthogonal_projection Kᗮ)

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

source

@[simp]

theorem inner_orthogonal_projection_eq_of_mem_right {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) [complete_space ↥K] (u : ↥K) (v : E) :

has_inner.inner (⇑(orthogonal_projection K) v) u = has_inner.inner v ↑u

source

@[simp]

theorem inner_orthogonal_projection_eq_of_mem_left {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) [complete_space ↥K] (u : ↥K) (v : E) :

has_inner.inner u (⇑(orthogonal_projection K) v) = has_inner.inner ↑u v

source

theorem inner_orthogonal_projection_left_eq_right {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) [complete_space ↥K] (u v : E) :

has_inner.inner ↑(⇑(orthogonal_projection K) u) v = has_inner.inner u ↑(⇑(orthogonal_projection K) v)

The orthogonal projection is self-adjoint.

source

theorem orthogonal_projection_is_symmetric {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (K : submodule 𝕜 E) [complete_space ↥K] :

↑(K.subtypeL.comp (orthogonal_projection K)).is_symmetric

The orthogonal projection is symmetric.

source

theorem submodule.finrank_add_inf_finrank_orthogonal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K₁ K₂ : submodule 𝕜 E} [finite_dimensional 𝕜 ↥K₂] (h : K₁ ≤ K₂) :

finite_dimensional.finrank 𝕜 ↥K₁ + finite_dimensional.finrank 𝕜 ↥(K₁ᗮ ⊓ K₂) = finite_dimensional.finrank 𝕜 ↥K₂

Given a finite-dimensional subspace K₂, and a subspace K₁ containined in it, the dimensions of K₁ and the intersection of its orthogonal subspace with K₂ add to that of K₂.

source

theorem submodule.finrank_add_inf_finrank_orthogonal' {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {K₁ K₂ : submodule 𝕜 E} [finite_dimensional 𝕜 ↥K₂] (h : K₁ ≤ K₂) {n : ℕ} (h_dim : finite_dimensional.finrank 𝕜 ↥K₁ + n = finite_dimensional.finrank 𝕜 ↥K₂) :

finite_dimensional.finrank 𝕜 ↥(K₁ᗮ ⊓ K₂) = n

Given a finite-dimensional subspace K₂, and a subspace K₁ containined in it, the dimensions of K₁ and the intersection of its orthogonal subspace with K₂ add to that of K₂.

source

theorem submodule.finrank_add_finrank_orthogonal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [finite_dimensional 𝕜 E] (K : submodule 𝕜 E) :

finite_dimensional.finrank 𝕜 ↥K + finite_dimensional.finrank 𝕜 ↥Kᗮ = finite_dimensional.finrank 𝕜 E

Given a finite-dimensional space E and subspace K, the dimensions of K and Kᗮ add to that of E.

source

theorem submodule.finrank_add_finrank_orthogonal' {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [finite_dimensional 𝕜 E] {K : submodule 𝕜 E} {n : ℕ} (h_dim : finite_dimensional.finrank 𝕜 ↥K + n = finite_dimensional.finrank 𝕜 E) :

finite_dimensional.finrank 𝕜 ↥Kᗮ = n

Given a finite-dimensional space E and subspace K, the dimensions of K and Kᗮ add to that of E.

source

theorem finrank_orthogonal_span_singleton {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {n : ℕ} [fact (finite_dimensional.finrank 𝕜 E = n + 1)] {v : E} (hv : v ≠ 0) :

finite_dimensional.finrank 𝕜 ↥(submodule.span 𝕜 {v})ᗮ = n

In a finite-dimensional inner product space, the dimension of the orthogonal complement of the span of a nonzero vector is one less than the dimension of the space.

source

theorem linear_isometry_equiv.reflections_generate_dim_aux {F : Type u_3} [inner_product_space ℝ F] [finite_dimensional ℝ F] {n : ℕ} (φ : F ≃ₗᵢ[ℝ ] F) (hn : finite_dimensional.finrank ℝ ↥((continuous_linear_map.id ℝ F - ↑(φ.to_continuous_linear_equiv)).ker)ᗮ ≤ n) :

∃ (l : list F), l.length ≤ n ∧ φ = (list.map (λ (v : F), reflection (submodule.span ℝ {v})ᗮ) l).prod

An element φ of the orthogonal group of F can be factored as a product of reflections, and specifically at most as many reflections as the dimension of the complement of the fixed subspace of φ.

source

theorem linear_isometry_equiv.reflections_generate_dim {F : Type u_3} [inner_product_space ℝ F] [finite_dimensional ℝ F] (φ : F ≃ₗᵢ[ℝ ] F) :

∃ (l : list F), l.length ≤ finite_dimensional.finrank ℝ F ∧ φ = (list.map (λ (v : F), reflection (submodule.span ℝ {v})ᗮ) l).prod

The orthogonal group of F is generated by reflections; specifically each element φ of the orthogonal group is a product of at most as many reflections as the dimension of F.

Special case of the Cartan–Dieudonné theorem.

source

theorem linear_isometry_equiv.reflections_generate {F : Type u_3} [inner_product_space ℝ F] [finite_dimensional ℝ F] :

subgroup.closure (set.range (λ (v : F), reflection (submodule.span ℝ {v})ᗮ)) = ⊤

The orthogonal group of F is generated by reflections.

source

theorem orthogonal_family.is_internal_iff_of_is_complete {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {ι : Type u_4} [decidable_eq ι] {V : ι → submodule 𝕜 E} (hV : orthogonal_family 𝕜 (λ (i : ι), (V i).subtypeₗᵢ)) (hc : is_complete ↑(supr V)) :

direct_sum.is_internal V ↔ (supr V)ᗮ = ⊥

An orthogonal family of subspaces of E satisfies direct_sum.is_internal (that is, they provide an internal direct sum decomposition of E) if and only if their span has trivial orthogonal complement.

source

theorem orthogonal_family.is_internal_iff {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {ι : Type u_4} [decidable_eq ι] [finite_dimensional 𝕜 E] {V : ι → submodule 𝕜 E} (hV : orthogonal_family 𝕜 (λ (i : ι), (V i).subtypeₗᵢ)) :

direct_sum.is_internal V ↔ (supr V)ᗮ = ⊥

An orthogonal family of subspaces of E satisfies direct_sum.is_internal (that is, they provide an internal direct sum decomposition of E) if and only if their span has trivial orthogonal complement.

source

theorem maximal_orthonormal_iff_orthogonal_complement_eq_bot {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {v : set E} (hv : orthonormal 𝕜 coe) :

(∀ (u : set E), u ⊇ v → orthonormal 𝕜 coe → u = v) ↔ (submodule.span 𝕜 v)ᗮ = ⊥

An orthonormal set in an inner_product_space is maximal, if and only if the orthogonal complement of its span is empty.

source

theorem maximal_orthonormal_iff_basis_of_finite_dimensional {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {v : set E} [finite_dimensional 𝕜 E] (hv : orthonormal 𝕜 coe) :

(∀ (u : set E), u ⊇ v → orthonormal 𝕜 coe → u = v) ↔ ∃ (b : basis ↥v 𝕜 E), ⇑b = coe

An orthonormal set in a finite-dimensional inner_product_space is maximal, if and only if it is a basis.

mathlib documentation

The orthogonal projection #

References #

Orthogonal projection in inner product spaces #