Euclidean spaces

This file makes some definitions and proves very basic geometrical results about real inner product spaces and Euclidean affine spaces. Results about real inner product spaces that involve the norm and inner product but not angles generally go in Analysis.NormedSpace.InnerProduct. Results with longer proofs or more geometrical content generally go in separate files.

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.

Implementation notes

To declare P as the type of points in a Euclidean affine space with V as the type of vectors, use [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P]. This works better with outParam to make V implicit in most cases than having a separate type alias for Euclidean affine spaces.

Rather than requiring Euclidean affine spaces to be finite-dimensional (as in the definition on Wikipedia), this is specified only for those theorems that need it.

References

• https://en.wikipedia.org/wiki/Euclidean_space

Geometrical results on Euclidean affine spaces

This section develops some geometrical definitions and results on Euclidean affine spaces.

theorem EuclideanGeometry.dist_left_midpoint_eq_dist_right_midpoint {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p1 : P) (p2 : P) : dist p1 (midpoint ℝ p1 p2) = dist p2 (midpoint ℝ p1 p2)

The midpoint of the segment AB is the same distance from A as it is from B.

theorem EuclideanGeometry.inner_weightedVSub {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {ι₁ : Type u_3} {s₁ : Finset ι₁} {w₁ : ι₁ → ℝ} (p₁ : ι₁ → P) (h₁ : (Finset.sum s₁ fun (i : ι₁) => w₁ i) = 0) {ι₂ : Type u_4} {s₂ : Finset ι₂} {w₂ : ι₂ → ℝ} (p₂ : ι₂ → P) (h₂ : (Finset.sum s₂ fun (i : ι₂) => w₂ i) = 0) : ⟪(Finset.weightedVSub s₁ p₁) w₁, (Finset.weightedVSub s₂ p₂) w₂⟫_ℝ = (-Finset.sum s₁ fun (i₁ : ι₁) => Finset.sum s₂ fun (i₂ : ι₂) => w₁ i₁ * w₂ i₂ * (dist (p₁ i₁) (p₂ i₂) * dist (p₁ i₁) (p₂ i₂))) / 2

The inner product of two vectors given with weightedVSub, in terms of the pairwise distances.

theorem EuclideanGeometry.dist_affineCombination {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {ι : Type u_3} {s : Finset ι} {w₁ : ι → ℝ} {w₂ : ι → ℝ} (p : ι → P) (h₁ : (Finset.sum s fun (i : ι) => w₁ i) = 1) (h₂ : (Finset.sum s fun (i : ι) => w₂ i) = 1) : let_fun a₁ := (Finset.affineCombination ℝ s p) w₁; let_fun a₂ := (Finset.affineCombination ℝ s p) w₂; dist a₁ a₂ * dist a₁ a₂ = (-Finset.sum s fun (i₁ : ι) => Finset.sum s fun (i₂ : ι) => (w₁ - w₂) i₁ * (w₁ - w₂) i₂ * (dist (p i₁) (p i₂) * dist (p i₁) (p i₂))) / 2

The distance between two points given with affineCombination, in terms of the pairwise distances between the points in that combination.

theorem EuclideanGeometry.dist_smul_vadd_sq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (r : ℝ) (v : V) (p₁ : P) (p₂ : P) : dist (r • v +ᵥ p₁) p₂ * dist (r • v +ᵥ p₁) p₂ = ⟪v, v⟫_ℝ * r * r + 2 * ⟪v, p₁ -ᵥ p₂⟫_ℝ * r + ⟪p₁ -ᵥ p₂, p₁ -ᵥ p₂⟫_ℝ

The squared distance between points on a line (expressed as a multiple of a fixed vector added to a point) and another point, expressed as a quadratic.

theorem EuclideanGeometry.dist_smul_vadd_eq_dist {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {v : V} (p₁ : P) (p₂ : P) (hv : v ≠ 0) (r : ℝ) : dist (r • v +ᵥ p₁) p₂ = dist p₁ p₂ ↔ r = 0 ∨ r = -2 * ⟪v, p₁ -ᵥ p₂⟫_ℝ / ⟪v, v⟫_ℝ

The condition for two points on a line to be equidistant from another point.

theorem EuclideanGeometry.eq_of_dist_eq_of_dist_eq_of_mem_of_finrank_eq_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} [FiniteDimensional ℝ ↥(AffineSubspace.direction s)] (hd : FiniteDimensional.finrank ℝ ↥(AffineSubspace.direction s) = 2) {c₁ : P} {c₂ : P} {p₁ : P} {p₂ : P} {p : P} (hc₁s : c₁ ∈ s) (hc₂s : c₂ ∈ s) (hp₁s : p₁ ∈ s) (hp₂s : p₂ ∈ s) (hps : p ∈ s) {r₁ : ℝ} {r₂ : ℝ} (hc : c₁ ≠ c₂) (hp : p₁ ≠ p₂) (hp₁c₁ : dist p₁ c₁ = r₁) (hp₂c₁ : dist p₂ c₁ = r₁) (hpc₁ : dist p c₁ = r₁) (hp₁c₂ : dist p₁ c₂ = r₂) (hp₂c₂ : dist p₂ c₂ = r₂) (hpc₂ : dist p c₂ = r₂) : p = p₁ ∨ p = p₂

Distances r₁ r₂ of p from two different points c₁ c₂ determine at most two points p₁ p₂ in a two-dimensional subspace containing those points (two circles intersect in at most two points).

theorem EuclideanGeometry.eq_of_dist_eq_of_dist_eq_of_finrank_eq_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [FiniteDimensional ℝ V] (hd : FiniteDimensional.finrank ℝ V = 2) {c₁ : P} {c₂ : P} {p₁ : P} {p₂ : P} {p : P} {r₁ : ℝ} {r₂ : ℝ} (hc : c₁ ≠ c₂) (hp : p₁ ≠ p₂) (hp₁c₁ : dist p₁ c₁ = r₁) (hp₂c₁ : dist p₂ c₁ = r₁) (hpc₁ : dist p c₁ = r₁) (hp₁c₂ : dist p₁ c₂ = r₂) (hp₂c₂ : dist p₂ c₂ = r₂) (hpc₂ : dist p c₂ = r₂) : p = p₁ ∨ p = p₂

Distances r₁ r₂ of p from two different points c₁ c₂ determine at most two points p₁ p₂ in two-dimensional space (two circles intersect in at most two points).

def EuclideanGeometry.orthogonalProjectionFn {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace ℝ P) [Nonempty ↥s] [HasOrthogonalProjection (AffineSubspace.direction s)] (p : P) : P

The orthogonal projection of a point onto a nonempty affine subspace, whose direction is complete, as an unbundled function. This definition is only intended for use in setting up the bundled version orthogonalProjection and should not be used once that is defined.

Equations

• EuclideanGeometry.orthogonalProjectionFn s p = Classical.choose (_ : ∃ (p_1 : P), ↑s ∩ ↑(AffineSubspace.mk' p (AffineSubspace.direction s)ᗮ) = {p_1})

theorem EuclideanGeometry.inter_eq_singleton_orthogonalProjectionFn {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} [Nonempty ↥s] [HasOrthogonalProjection (AffineSubspace.direction s)] (p : P) : ↑s ∩ ↑(AffineSubspace.mk' p (AffineSubspace.direction s)ᗮ) = {EuclideanGeometry.orthogonalProjectionFn s p}

The intersection of the subspace and the orthogonal subspace through the given point is the orthogonalProjectionFn of that point onto the subspace. This lemma is only intended for use in setting up the bundled version and should not be used once that is defined.

theorem EuclideanGeometry.orthogonalProjectionFn_mem {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} [Nonempty ↥s] [HasOrthogonalProjection (AffineSubspace.direction s)] (p : P) : EuclideanGeometry.orthogonalProjectionFn s p ∈ s

The orthogonalProjectionFn lies 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.

theorem EuclideanGeometry.orthogonalProjectionFn_mem_orthogonal {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} [Nonempty ↥s] [HasOrthogonalProjection (AffineSubspace.direction s)] (p : P) : EuclideanGeometry.orthogonalProjectionFn s p ∈ AffineSubspace.mk' p (AffineSubspace.direction s)ᗮ

The orthogonalProjectionFn lies in the orthogonal subspace. This lemma is only intended for use in setting up the bundled version and should not be used once that is defined.

theorem EuclideanGeometry.orthogonalProjectionFn_vsub_mem_direction_orthogonal {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} [Nonempty ↥s] [HasOrthogonalProjection (AffineSubspace.direction s)] (p : P) : EuclideanGeometry.orthogonalProjectionFn s p -ᵥ p ∈ (AffineSubspace.direction s)ᗮ

Subtracting p from its orthogonalProjectionFn produces a result in the orthogonal direction. This lemma is only intended for use in setting up the bundled version and should not be used once that is defined.

def EuclideanGeometry.orthogonalProjection {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace ℝ P) [Nonempty ↥s] [HasOrthogonalProjection (AffineSubspace.direction s)] : P →ᵃ[ℝ] ↥s

The orthogonal projection of a point onto a nonempty affine subspace, whose direction is complete. The corresponding linear map (mapping a vector to the difference between the projections of two points whose difference is that vector) is the orthogonalProjection for real inner product spaces, onto the direction of the affine subspace being projected onto.

Equations

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

@[simp]

theorem EuclideanGeometry.orthogonalProjectionFn_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} [Nonempty ↥s] [HasOrthogonalProjection (AffineSubspace.direction s)] (p : P) : EuclideanGeometry.orthogonalProjectionFn s p = ↑((EuclideanGeometry.orthogonalProjection s) p)

@[simp]

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

The linear map corresponding to orthogonalProjection.

theorem EuclideanGeometry.inter_eq_singleton_orthogonalProjection {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} [Nonempty ↥s] [HasOrthogonalProjection (AffineSubspace.direction s)] (p : P) : ↑s ∩ ↑(AffineSubspace.mk' p (AffineSubspace.direction s)ᗮ) = {↑((EuclideanGeometry.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_mem {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} [Nonempty ↥s] [HasOrthogonalProjection (AffineSubspace.direction s)] (p : P) : ↑((EuclideanGeometry.orthogonalProjection s) p) ∈ s

The orthogonalProjection lies in the given subspace.

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

The orthogonalProjection lies in the orthogonal subspace.

theorem EuclideanGeometry.orthogonalProjection_vsub_mem_direction {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} [Nonempty ↥s] [HasOrthogonalProjection (AffineSubspace.direction s)] {p1 : P} (p2 : P) (hp1 : p1 ∈ s) : ↑((EuclideanGeometry.orthogonalProjection s) p2 -ᵥ { val := p1, property := hp1 }) ∈ AffineSubspace.direction s

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 {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} [Nonempty ↥s] [HasOrthogonalProjection (AffineSubspace.direction s)] {p1 : P} (p2 : P) (hp1 : p1 ∈ s) : ↑({ val := p1, property := hp1 } -ᵥ (EuclideanGeometry.orthogonalProjection s) p2) ∈ AffineSubspace.direction s

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 {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} [Nonempty ↥s] [HasOrthogonalProjection (AffineSubspace.direction s)] {p : P} : ↑((EuclideanGeometry.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 {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} [Nonempty ↥s] [HasOrthogonalProjection (AffineSubspace.direction s)] (p : ↥s) : (EuclideanGeometry.orthogonalProjection s) ↑p = p

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

Orthogonal projection is idempotent.

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

theorem EuclideanGeometry.dist_orthogonalProjection_eq_zero_iff {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} [Nonempty ↥s] [HasOrthogonalProjection (AffineSubspace.direction s)] {p : P} : dist p ↑((EuclideanGeometry.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_not_mem {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} [Nonempty ↥s] [HasOrthogonalProjection (AffineSubspace.direction s)] {p : P} (hp : p ∉ s) : dist p ↑((EuclideanGeometry.orthogonalProjection s) p) ≠ 0

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

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

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

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

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

theorem EuclideanGeometry.orthogonalProjection_vsub_orthogonalProjection {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace ℝ P) [Nonempty ↥s] [HasOrthogonalProjection (AffineSubspace.direction s)] (p : P) : (orthogonalProjection (AffineSubspace.direction s)) (p -ᵥ ↑((EuclideanGeometry.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.orthogonalProjection_vadd_eq_self {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} [Nonempty ↥s] [HasOrthogonalProjection (AffineSubspace.direction s)] {p : P} (hp : p ∈ s) {v : V} (hv : v ∈ (AffineSubspace.direction s)ᗮ) : (EuclideanGeometry.orthogonalProjection s) (v +ᵥ p) = { val := p, property := 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 {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} [Nonempty ↥s] [HasOrthogonalProjection (AffineSubspace.direction s)] {p1 : P} (p2 : P) (r : ℝ) (hp : p1 ∈ s) : (EuclideanGeometry.orthogonalProjection s) (r • (p2 -ᵥ ↑((EuclideanGeometry.orthogonalProjection s) p2)) +ᵥ p1) = { val := p1, property := 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.dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} [Nonempty ↥s] [HasOrthogonalProjection (AffineSubspace.direction s)] {p1 : P} (p2 : P) (hp1 : p1 ∈ s) : dist p1 p2 * dist p1 p2 = dist p1 ↑((EuclideanGeometry.orthogonalProjection s) p2) * dist p1 ↑((EuclideanGeometry.orthogonalProjection s) p2) + dist p2 ↑((EuclideanGeometry.orthogonalProjection s) p2) * dist p2 ↑((EuclideanGeometry.orthogonalProjection s) p2)

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

theorem EuclideanGeometry.dist_sq_smul_orthogonal_vadd_smul_orthogonal_vadd {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} {p1 : P} {p2 : P} (hp1 : p1 ∈ s) (hp2 : p2 ∈ s) (r1 : ℝ) (r2 : ℝ) {v : V} (hv : v ∈ (AffineSubspace.direction s)ᗮ) : dist (r1 • v +ᵥ p1) (r2 • v +ᵥ p2) * dist (r1 • v +ᵥ p1) (r2 • v +ᵥ p2) = dist p1 p2 * dist p1 p2 + (r1 - r2) * (r1 - r2) * (‖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.

def EuclideanGeometry.reflection {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace ℝ P) [Nonempty ↥s] [HasOrthogonalProjection (AffineSubspace.direction s)] : 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 {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace ℝ P) [Nonempty ↥s] [HasOrthogonalProjection (AffineSubspace.direction s)] (p : P) : (EuclideanGeometry.reflection s) p = ↑((EuclideanGeometry.orthogonalProjection s) p) -ᵥ p +ᵥ ↑((EuclideanGeometry.orthogonalProjection s) p)

The result of reflecting.

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

@[simp]

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

Reflecting twice in the same subspace.

@[simp]

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

Reflection is its own inverse.

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

Reflection is involutive.

theorem EuclideanGeometry.reflection_eq_self_iff {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} [Nonempty ↥s] [HasOrthogonalProjection (AffineSubspace.direction s)] (p : P) : (EuclideanGeometry.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 {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s₁ : AffineSubspace ℝ P) (s₂ : AffineSubspace ℝ P) [Nonempty ↥s₁] [Nonempty ↥s₂] [HasOrthogonalProjection (AffineSubspace.direction s₁)] [HasOrthogonalProjection (AffineSubspace.direction s₂)] (p : P) : (EuclideanGeometry.reflection s₁) p = (EuclideanGeometry.reflection s₂) p ↔ ↑((EuclideanGeometry.orthogonalProjection s₁) p) = ↑((EuclideanGeometry.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 {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace ℝ P) [Nonempty ↥s] [HasOrthogonalProjection (AffineSubspace.direction s)] (p₁ : P) (p₂ : P) : dist p₁ ((EuclideanGeometry.reflection s) p₂) = dist ((EuclideanGeometry.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 {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace ℝ P) [Nonempty ↥s] [HasOrthogonalProjection (AffineSubspace.direction s)] {p₁ : P} (hp₁ : p₁ ∈ s) (p₂ : P) : dist p₁ ((EuclideanGeometry.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 {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s₁ : AffineSubspace ℝ P} {s₂ : AffineSubspace ℝ P} [Nonempty ↥s₁] [HasOrthogonalProjection (AffineSubspace.direction s₁)] (hle : s₁ ≤ s₂) {p : P} (hp : p ∈ s₂) : (EuclideanGeometry.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 {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} [Nonempty ↥s] [HasOrthogonalProjection (AffineSubspace.direction s)] {p : P} (hp : p ∈ s) {v : V} (hv : v ∈ (AffineSubspace.direction s)ᗮ) : (EuclideanGeometry.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 {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} [Nonempty ↥s] [HasOrthogonalProjection (AffineSubspace.direction s)] {p₁ : P} (p₂ : P) (r : ℝ) (hp₁ : p₁ ∈ s) : (EuclideanGeometry.reflection s) (r • (p₂ -ᵥ ↑((EuclideanGeometry.orthogonalProjection s) p₂)) +ᵥ p₁) = -(r • (p₂ -ᵥ ↑((EuclideanGeometry.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.