Orthogonal projection in affine spaces

This file defines orthogonal projection onto an affine subspace, and reflection of a point in an affine subspace.

Main definitions

• EuclideanGeometry.orthogonalProjection is the orthogonal projection of a point onto an affine subspace.

• EuclideanGeometry.reflection is the reflection of a point in an affine subspace.

def EuclideanGeometry.orthogonalProjection {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace 𝕜 P) [Nonempty ↥s] [s.direction.HasOrthogonalProjection] : P →ᴬ[𝕜] ↥s

The orthogonal projection of a point onto a nonempty affine subspace.

Equations

• One or more equations did not get rendered due to their size.

theorem EuclideanGeometry.orthogonalProjection_apply {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace 𝕜 P) [Nonempty ↥s] [s.direction.HasOrthogonalProjection] {p : P} : (orthogonalProjection s) p = s.direction.orthogonalProjection (p -ᵥ ↑(Classical.arbitrary ↥s)) +ᵥ Classical.arbitrary ↥s

theorem EuclideanGeometry.orthogonalProjection_apply' {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace 𝕜 P) [Nonempty ↥s] [s.direction.HasOrthogonalProjection] {p : P} : ↑((orthogonalProjection s) p) = ↑(s.direction.orthogonalProjection (p -ᵥ ↑(Classical.arbitrary ↥s))) +ᵥ ↑(Classical.arbitrary ↥s)

theorem EuclideanGeometry.orthogonalProjection_apply_mem {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace 𝕜 P) [Nonempty ↥s] [s.direction.HasOrthogonalProjection] {p x : P} (hx : x ∈ s) : ↑((orthogonalProjection s) p) = ↑(s.direction.orthogonalProjection (p -ᵥ x)) +ᵥ x

theorem EuclideanGeometry.orthogonalProjection_congr {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s₁ s₂ : AffineSubspace 𝕜 P} {p₁ p₂ : P} [Nonempty ↥s₁] [s₁.direction.HasOrthogonalProjection] (h : s₁ = s₂) (hp : p₁ = p₂) : ↑((orthogonalProjection s₁) p₁) = ↑((orthogonalProjection s₂) p₂)

Since both instance arguments are propositions, allow simp to rewrite them alongside the s argument.

Note that without the coercion to P, the LHS and RHS would have different types.

@[simp]

theorem EuclideanGeometry.orthogonalProjection_linear {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace 𝕜 P} [Nonempty ↥s] [s.direction.HasOrthogonalProjection] : (↑(orthogonalProjection s)).linear = ↑s.direction.orthogonalProjection

The linear map corresponding to orthogonalProjection.

@[simp]

theorem EuclideanGeometry.orthogonalProjection_contLinear {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace 𝕜 P} [Nonempty ↥s] [s.direction.HasOrthogonalProjection] : (orthogonalProjection s).contLinear = s.direction.orthogonalProjection

The continuous linear map corresponding to orthogonalProjection.

theorem EuclideanGeometry.orthogonalProjection_mem {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace 𝕜 P} [Nonempty ↥s] [s.direction.HasOrthogonalProjection] (p : P) : ↑((orthogonalProjection s) p) ∈ s

The orthogonalProjection lies in the given subspace.

theorem EuclideanGeometry.orthogonalProjection_mem_orthogonal {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace 𝕜 P) [Nonempty ↥s] [s.direction.HasOrthogonalProjection] (p : P) : ↑((orthogonalProjection s) p) ∈ AffineSubspace.mk' p s.directionᗮ

The orthogonalProjection lies in the orthogonal subspace.

theorem EuclideanGeometry.inter_eq_singleton_orthogonalProjection {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace 𝕜 P} [Nonempty ↥s] [s.direction.HasOrthogonalProjection] (p : P) : ↑s ∩ ↑(AffineSubspace.mk' p s.directionᗮ) = {↑((orthogonalProjection s) p)}

The intersection of the subspace and the orthogonal subspace through the given point is the orthogonalProjection of that point onto the subspace.

theorem EuclideanGeometry.orthogonalProjection_vsub_mem_direction {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace 𝕜 P} [Nonempty ↥s] [s.direction.HasOrthogonalProjection] {p₁ : P} (p₂ : P) (hp₁ : p₁ ∈ s) : ↑((orthogonalProjection s) p₂ -ᵥ ⟨p₁, hp₁⟩) ∈ s.direction

Subtracting a point in the given subspace from the orthogonalProjection produces a result in the direction of the given subspace.

theorem EuclideanGeometry.vsub_orthogonalProjection_mem_direction {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace 𝕜 P} [Nonempty ↥s] [s.direction.HasOrthogonalProjection] {p₁ : P} (p₂ : P) (hp₁ : p₁ ∈ s) : ↑(⟨p₁, hp₁⟩ -ᵥ (orthogonalProjection s) p₂) ∈ s.direction

Subtracting the orthogonalProjection from a point in the given subspace produces a result in the direction of the given subspace.

theorem EuclideanGeometry.orthogonalProjection_eq_self_iff {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace 𝕜 P} [Nonempty ↥s] [s.direction.HasOrthogonalProjection] {p : P} : ↑((orthogonalProjection s) p) = p ↔ p ∈ s

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

@[simp]

theorem EuclideanGeometry.orthogonalProjection_mem_subspace_eq_self {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace 𝕜 P} [Nonempty ↥s] [s.direction.HasOrthogonalProjection] (p : ↥s) : (orthogonalProjection s) ↑p = p

theorem EuclideanGeometry.orthogonalProjection_orthogonalProjection {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace 𝕜 P) [Nonempty ↥s] [s.direction.HasOrthogonalProjection] (p : P) : (orthogonalProjection s) ↑((orthogonalProjection s) p) = (orthogonalProjection s) p

Orthogonal projection is idempotent.

theorem EuclideanGeometry.eq_orthogonalProjection_of_eq_subspace {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s s' : AffineSubspace 𝕜 P} [Nonempty ↥s] [Nonempty ↥s'] [s.direction.HasOrthogonalProjection] [s'.direction.HasOrthogonalProjection] (h : s = s') (p : P) : ↑((orthogonalProjection s) p) = ↑((orthogonalProjection s') p)

@[simp]

theorem EuclideanGeometry.orthogonalProjection_affineSpan_singleton {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (p₁ p₂ : P) : ↑((orthogonalProjection (affineSpan 𝕜 {p₁})) p₂) = p₁

theorem EuclideanGeometry.orthogonalProjection_vsub_mem_direction_orthogonal {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace 𝕜 P) [Nonempty ↥s] [s.direction.HasOrthogonalProjection] (p : P) : ↑((orthogonalProjection s) p) -ᵥ p ∈ s.directionᗮ

Subtracting p from its orthogonalProjection produces a result in the orthogonal direction.

theorem EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace 𝕜 P) [Nonempty ↥s] [s.direction.HasOrthogonalProjection] (p : P) : p -ᵥ ↑((orthogonalProjection s) p) ∈ s.directionᗮ

Subtracting the orthogonalProjection from p produces a result in the orthogonal direction.

theorem EuclideanGeometry.orthogonalProjection_vsub_orthogonalProjection {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace 𝕜 P) [Nonempty ↥s] [s.direction.HasOrthogonalProjection] (p : P) : s.direction.orthogonalProjection (p -ᵥ ↑((orthogonalProjection s) p)) = 0

Subtracting the orthogonalProjection from p produces a result in the kernel of the linear part of the orthogonal projection.

theorem EuclideanGeometry.coe_orthogonalProjection_eq_iff_mem {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace 𝕜 P} [Nonempty ↥s] [s.direction.HasOrthogonalProjection] {p q : P} : ↑((orthogonalProjection s) p) = q ↔ q ∈ s ∧ p -ᵥ q ∈ s.directionᗮ

The characteristic property of the orthogonal projection, for a point given in the underlying space. This form is typically more convenient to use than inter_eq_singleton_orthogonalProjection.

theorem EuclideanGeometry.orthogonalProjection_eq_iff_mem {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace 𝕜 P} [Nonempty ↥s] [s.direction.HasOrthogonalProjection] {p : P} {q : ↥s} : (orthogonalProjection s) p = q ↔ p -ᵥ ↑q ∈ s.directionᗮ

The characteristic property of the orthogonal projection, for a point given in the relevant subspace. This form is typically more convenient to use than inter_eq_singleton_orthogonalProjection.

theorem EuclideanGeometry.orthogonalProjection_eq_orthogonalProjection_iff_vsub_mem {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace 𝕜 P} [Nonempty ↥s] [s.direction.HasOrthogonalProjection] {p q : P} : (orthogonalProjection s) p = (orthogonalProjection s) q ↔ p -ᵥ q ∈ s.directionᗮ

A condition for two points to have the same orthogonal projection onto a given subspace.

theorem EuclideanGeometry.orthogonalProjection_sup_of_orthogonalProjection_eq {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s₁ s₂ : AffineSubspace 𝕜 P} [Nonempty ↥s₁] [Nonempty ↥s₂] [s₁.direction.HasOrthogonalProjection] [s₂.direction.HasOrthogonalProjection] {p : P} (h : ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection s₂) p)) [(s₁ ⊔ s₂).direction.HasOrthogonalProjection] : ↑((orthogonalProjection (s₁ ⊔ s₂)) p) = ↑((orthogonalProjection s₁) p)

If the orthogonal projections of a point onto two subspaces are equal, so is the projection onto their supremum.

theorem EuclideanGeometry.orthogonalProjection_vadd_eq_self {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace 𝕜 P} [Nonempty ↥s] [s.direction.HasOrthogonalProjection] {p : P} (hp : p ∈ s) {v : V} (hv : v ∈ s.directionᗮ) : (orthogonalProjection s) (v +ᵥ p) = ⟨p, hp⟩

Adding a vector to a point in the given subspace, then taking the orthogonal projection, produces the original point if the vector was in the orthogonal direction.

theorem EuclideanGeometry.orthogonalProjection_vadd_smul_vsub_orthogonalProjection {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace 𝕜 P} [Nonempty ↥s] [s.direction.HasOrthogonalProjection] {p₁ : P} (p₂ : P) (r : 𝕜) (hp : p₁ ∈ s) : (orthogonalProjection s) (r • (p₂ -ᵥ ↑((orthogonalProjection s) p₂)) +ᵥ p₁) = ⟨p₁, hp⟩

Adding a vector to a point in the given subspace, then taking the orthogonal projection, produces the original point if the vector is a multiple of the result of subtracting a point's orthogonal projection from that point.

theorem EuclideanGeometry.orthogonalProjection_orthogonalProjection_of_le {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s₁ s₂ : AffineSubspace 𝕜 P} [Nonempty ↥s₁] [Nonempty ↥s₂] [s₁.direction.HasOrthogonalProjection] [s₂.direction.HasOrthogonalProjection] (h : s₁ ≤ s₂) (p : P) : (orthogonalProjection s₁) ↑((orthogonalProjection s₂) p) = (orthogonalProjection s₁) p

theorem EuclideanGeometry.dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace 𝕜 P} [Nonempty ↥s] [s.direction.HasOrthogonalProjection] {p₁ : P} (p₂ : P) (hp₁ : p₁ ∈ s) : dist p₁ p₂ * dist p₁ p₂ = dist p₁ ↑((orthogonalProjection s) p₂) * dist p₁ ↑((orthogonalProjection s) p₂) + dist p₂ ↑((orthogonalProjection s) p₂) * dist p₂ ↑((orthogonalProjection s) p₂)

The square of the distance from a point in s to p₂ equals the sum of the squares of the distances of the two points to the orthogonalProjection.

theorem EuclideanGeometry.dist_orthogonalProjection_eq_infDist {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace 𝕜 P) [Nonempty ↥s] [s.direction.HasOrthogonalProjection] (p : P) : dist p ↑((orthogonalProjection s) p) = Metric.infDist p ↑s

The distance between a point and its orthogonal projection to a subspace equals the distance to that subspace as given by Metric.infDist. This is not a simp lemma since the simplest form depends on the context (if any calculations are to be done with the distance, the version with the orthogonal projection gives access to more lemmas about orthogonal projections that may be useful).

theorem EuclideanGeometry.dist_orthogonalProjection_eq_infNndist {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace 𝕜 P) [Nonempty ↥s] [s.direction.HasOrthogonalProjection] (p : P) : nndist p ↑((orthogonalProjection s) p) = Metric.infNndist p ↑s

The nonnegative distance between a point and its orthogonal projection to a subspace equals the distance to that subspace as given by Metric.infNndist. This is not a simp lemma since the simplest form depends on the context (if any calculations are to be done with the distance, the version with the orthogonal projection gives access to more lemmas about orthogonal projections that may be useful).

theorem EuclideanGeometry.dist_sq_smul_orthogonal_vadd_smul_orthogonal_vadd {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace 𝕜 P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (r₁ r₂ : 𝕜) {v : V} (hv : v ∈ s.directionᗮ) : dist (r₁ • v +ᵥ p₁) (r₂ • v +ᵥ p₂) * dist (r₁ • v +ᵥ p₁) (r₂ • v +ᵥ p₂) = dist p₁ p₂ * dist p₁ p₂ + ‖r₁ - r₂‖ * ‖r₁ - r₂‖ * (‖v‖ * ‖v‖)

The square of the distance between two points constructed by adding multiples of the same orthogonal vector to points in the same subspace.

theorem EuclideanGeometry.dist_eq_iff_dist_orthogonalProjection_eq {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace 𝕜 P} [Nonempty ↥s] [s.direction.HasOrthogonalProjection] {p₁ p₂ : P} (p₃ : P) (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) : dist p₁ p₃ = dist p₂ p₃ ↔ dist p₁ ↑((orthogonalProjection s) p₃) = dist p₂ ↑((orthogonalProjection s) p₃)

p is equidistant from two points in s if and only if its orthogonalProjection is.

theorem EuclideanGeometry.dist_set_eq_iff_dist_orthogonalProjection_eq {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace 𝕜 P} [Nonempty ↥s] [s.direction.HasOrthogonalProjection] {ps : Set P} (hps : ps ⊆ ↑s) (p : P) : (ps.Pairwise fun (p₁ p₂ : P) => dist p₁ p = dist p₂ p) ↔ ps.Pairwise fun (p₁ p₂ : P) => dist p₁ ↑((orthogonalProjection s) p) = dist p₂ ↑((orthogonalProjection s) p)

p is equidistant from a set of points in s if and only if its orthogonalProjection is.

theorem EuclideanGeometry.exists_dist_eq_iff_exists_dist_orthogonalProjection_eq {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace 𝕜 P} [Nonempty ↥s] [s.direction.HasOrthogonalProjection] {ps : Set P} (hps : ps ⊆ ↑s) (p : P) : (∃ (r : ℝ), ∀ p₁ ∈ ps, dist p₁ p = r) ↔ ∃ (r : ℝ), ∀ p₁ ∈ ps, dist p₁ ↑((orthogonalProjection s) p) = r

There exists r such that p has distance r from all the points of a set of points in s if and only if there exists (possibly different) r such that its orthogonalProjection has that distance from all the points in that set.

def EuclideanGeometry.reflection {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace 𝕜 P) [Nonempty ↥s] [s.direction.HasOrthogonalProjection] : P ≃ᵃⁱ[𝕜] P

Reflection in an affine subspace, which is expected to be nonempty and complete. 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 an affine subspace, is a more general sense of the word that includes both those common cases.

Equations

• One or more equations did not get rendered due to their size.

theorem EuclideanGeometry.reflection_apply {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace 𝕜 P) [Nonempty ↥s] [s.direction.HasOrthogonalProjection] (p : P) : (reflection s) p = s.direction.reflection (p -ᵥ ↑(Classical.arbitrary ↥s)) +ᵥ ↑(Classical.arbitrary ↥s)

theorem EuclideanGeometry.reflection_apply_of_mem {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace 𝕜 P) [Nonempty ↥s] [s.direction.HasOrthogonalProjection] (p : P) {x : P} (hx : x ∈ s) : (reflection s) p = s.direction.reflection (p -ᵥ x) +ᵥ x

theorem EuclideanGeometry.reflection_apply' {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace 𝕜 P) [Nonempty ↥s] [s.direction.HasOrthogonalProjection] (p : P) : (reflection s) p = (↑((orthogonalProjection s) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s) p)

theorem EuclideanGeometry.eq_reflection_of_eq_subspace {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s s' : AffineSubspace 𝕜 P} [Nonempty ↥s] [Nonempty ↥s'] [s.direction.HasOrthogonalProjection] [s'.direction.HasOrthogonalProjection] (h : s = s') (p : P) : (reflection s) p = (reflection s') p

@[simp]

theorem EuclideanGeometry.reflection_reflection {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace 𝕜 P) [Nonempty ↥s] [s.direction.HasOrthogonalProjection] (p : P) : (reflection s) ((reflection s) p) = p

Reflecting twice in the same subspace.

@[simp]

theorem EuclideanGeometry.reflection_symm {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace 𝕜 P) [Nonempty ↥s] [s.direction.HasOrthogonalProjection] : (reflection s).symm = reflection s

Reflection is its own inverse.

theorem EuclideanGeometry.reflection_involutive {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace 𝕜 P) [Nonempty ↥s] [s.direction.HasOrthogonalProjection] : Function.Involutive ⇑(reflection s)

Reflection is involutive.

theorem EuclideanGeometry.reflection_eq_self_iff {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace 𝕜 P} [Nonempty ↥s] [s.direction.HasOrthogonalProjection] (p : P) : (reflection s) p = p ↔ p ∈ s

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

theorem EuclideanGeometry.reflection_eq_iff_orthogonalProjection_eq {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s₁ s₂ : AffineSubspace 𝕜 P) [Nonempty ↥s₁] [Nonempty ↥s₂] [s₁.direction.HasOrthogonalProjection] [s₂.direction.HasOrthogonalProjection] (p : P) : (reflection s₁) p = (reflection s₂) p ↔ ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection s₂) p)

Reflecting a point in two subspaces produces the same result if and only if the point has the same orthogonal projection in each of those subspaces.

theorem EuclideanGeometry.dist_reflection {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace 𝕜 P) [Nonempty ↥s] [s.direction.HasOrthogonalProjection] (p₁ p₂ : P) : dist p₁ ((reflection s) p₂) = dist ((reflection s) p₁) p₂

The distance between p₁ and the reflection of p₂ equals that between the reflection of p₁ and p₂.

theorem EuclideanGeometry.dist_reflection_eq_of_mem {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace 𝕜 P) [Nonempty ↥s] [s.direction.HasOrthogonalProjection] {p₁ : P} (hp₁ : p₁ ∈ s) (p₂ : P) : dist p₁ ((reflection s) p₂) = dist p₁ p₂

A point in the subspace is equidistant from another point and its reflection.

theorem EuclideanGeometry.reflection_mem_of_le_of_mem {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s₁ s₂ : AffineSubspace 𝕜 P} [Nonempty ↥s₁] [s₁.direction.HasOrthogonalProjection] (hle : s₁ ≤ s₂) {p : P} (hp : p ∈ s₂) : (reflection s₁) p ∈ s₂

The reflection of a point in a subspace is contained in any larger subspace containing both the point and the subspace reflected in.

theorem EuclideanGeometry.reflection_orthogonal_vadd {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace 𝕜 P} [Nonempty ↥s] [s.direction.HasOrthogonalProjection] {p : P} (hp : p ∈ s) {v : V} (hv : v ∈ s.directionᗮ) : (reflection s) (v +ᵥ p) = -v +ᵥ p

Reflecting an orthogonal vector plus a point in the subspace produces the negation of that vector plus the point.

theorem EuclideanGeometry.reflection_vadd_smul_vsub_orthogonalProjection {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace 𝕜 P} [Nonempty ↥s] [s.direction.HasOrthogonalProjection] {p₁ : P} (p₂ : P) (r : 𝕜) (hp₁ : p₁ ∈ s) : (reflection s) (r • (p₂ -ᵥ ↑((orthogonalProjection s) p₂)) +ᵥ p₁) = -(r • (p₂ -ᵥ ↑((orthogonalProjection s) p₂))) +ᵥ p₁

Reflecting a vector plus a point in the subspace produces the negation of that vector plus the point if the vector is a multiple of the result of subtracting a point's orthogonal projection from that point.

theorem EuclideanGeometry.dist_orthogonalProjection_eq_zero_iff {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace 𝕜 P} [Nonempty ↥s] [s.direction.HasOrthogonalProjection] {p : P} : dist p ↑((orthogonalProjection s) p) = 0 ↔ p ∈ s

The distance to a point's orthogonal projection is 0 iff it lies in the subspace.

theorem EuclideanGeometry.dist_orthogonalProjection_ne_zero_of_notMem {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace 𝕜 P} [Nonempty ↥s] [s.direction.HasOrthogonalProjection] {p : P} (hp : p ∉ s) : dist p ↑((orthogonalProjection s) p) ≠ 0

The distance between a point and its orthogonal projection is nonzero if it does not lie in the subspace.

@[deprecated EuclideanGeometry.dist_orthogonalProjection_ne_zero_of_notMem (since := "2025-05-23")]

theorem EuclideanGeometry.dist_orthogonalProjection_ne_zero_of_not_mem {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace 𝕜 P} [Nonempty ↥s] [s.direction.HasOrthogonalProjection] {p : P} (hp : p ∉ s) : dist p ↑((orthogonalProjection s) p) ≠ 0

Alias of EuclideanGeometry.dist_orthogonalProjection_ne_zero_of_notMem.

---

The distance between a point and its orthogonal projection is nonzero if it does not lie in the subspace.

def Affine.Simplex.orthogonalProjectionSpan {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Simplex 𝕜 P n) : P →ᴬ[𝕜] ↥(affineSpan 𝕜 (Set.range s.points))

The orthogonal projection of a point p onto the hyperplane spanned by the simplex's points.

Equations

• s.orthogonalProjectionSpan = EuclideanGeometry.orthogonalProjection (affineSpan 𝕜 (Set.range s.points))

theorem Affine.Simplex.orthogonalProjectionSpan_congr {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] {m n : ℕ} {s₁ : Simplex 𝕜 P m} {s₂ : Simplex 𝕜 P n} {p₁ p₂ : P} (h : Set.range s₁.points = Set.range s₂.points) (hp : p₁ = p₂) : ↑(s₁.orthogonalProjectionSpan p₁) = ↑(s₂.orthogonalProjectionSpan p₂)

@[simp]

theorem Affine.Simplex.orthogonalProjectionSpan_reindex {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] {m n : ℕ} (s : Simplex 𝕜 P m) (e : Fin (m + 1) ≃ Fin (n + 1)) (p : P) : ↑((s.reindex e).orthogonalProjectionSpan p) = ↑(s.orthogonalProjectionSpan p)

theorem Affine.Simplex.orthogonalProjection_vadd_smul_vsub_orthogonalProjection {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Simplex 𝕜 P n) {p₁ : P} (p₂ : P) (r : 𝕜) (hp : p₁ ∈ affineSpan 𝕜 (Set.range s.points)) : s.orthogonalProjectionSpan (r • (p₂ -ᵥ ↑(s.orthogonalProjectionSpan p₂)) +ᵥ p₁) = ⟨p₁, hp⟩

Adding a vector to a point in the given subspace, then taking the orthogonal projection, produces the original point if the vector is a multiple of the result of subtracting a point's orthogonal projection from that point.

theorem Affine.Simplex.coe_orthogonalProjection_vadd_smul_vsub_orthogonalProjection {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] {n : ℕ} {r₁ : 𝕜} (s : Simplex 𝕜 P n) {p p₁o : P} (hp₁o : p₁o ∈ affineSpan 𝕜 (Set.range s.points)) : ↑(s.orthogonalProjectionSpan (r₁ • (p -ᵥ ↑(s.orthogonalProjectionSpan p)) +ᵥ p₁o)) = p₁o

theorem Affine.Simplex.dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Simplex 𝕜 P n) {p₁ : P} (p₂ : P) (hp₁ : p₁ ∈ affineSpan 𝕜 (Set.range s.points)) : dist p₁ p₂ * dist p₁ p₂ = dist p₁ ↑(s.orthogonalProjectionSpan p₂) * dist p₁ ↑(s.orthogonalProjectionSpan p₂) + dist p₂ ↑(s.orthogonalProjectionSpan p₂) * dist p₂ ↑(s.orthogonalProjectionSpan p₂)

@[simp]

theorem Affine.Simplex.orthogonalProjectionSpan_eq_point {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : Simplex 𝕜 P 0) (p : P) : ↑(s.orthogonalProjectionSpan p) = s.points 0

theorem Affine.Simplex.orthogonalProjectionSpan_faceOpposite_eq_point_rev {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : Simplex 𝕜 P 1) (i : Fin 2) (p : P) : ↑((s.faceOpposite i).orthogonalProjectionSpan p) = s.points i.rev