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.

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.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₁ : ∑ i ∈ s₁, w₁ i = 0) {ι₂ : Type u_4} {s₂ : Finset ι₂} {w₂ : ι₂ → ℝ} (p₂ : ι₂ → P) (h₂ : ∑ i ∈ s₂, w₂ i = 0) : inner ((s₁.weightedVSub p₁) w₁) ((s₂.weightedVSub p₂) w₂) = (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, 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₁ : ∑ i ∈ s, w₁ i = 1) (h₂ : ∑ i ∈ s, 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₂ = (-∑ i₁ ∈ s, ∑ i₂ ∈ s, (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) : dist (r • v +ᵥ p₁) p₂ * dist (r • v +ᵥ p₁) p₂ = inner v v * r * r + 2 * inner v (p₁ -ᵥ p₂) * r + inner (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) (hv : v ≠ 0) (r : ℝ) : dist (r • v +ᵥ p₁) p₂ = dist p₁ p₂ ↔ r = 0 ∨ r = -2 * inner v (p₁ -ᵥ p₂) / inner 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 ℝ ↥s.direction] (hd : Module.finrank ℝ ↥s.direction = 2) {c₁ c₂ 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 : Module.finrank ℝ V = 2) {c₁ c₂ 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).