Altitudes of a simplex

This file defines the altitudes of a simplex and their feet.

Main definitions

• altitude is the line that passes through a vertex of a simplex and is orthogonal to the opposite face.

• altitudeFoot is the orthogonal projection of a vertex of a simplex onto the opposite face.

• height is the distance between a vertex of a simplex and its altitudeFoot.

References

• https://en.wikipedia.org/wiki/Altitude_(triangle)

noncomputable def Affine.Simplex.altitude {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Simplex ℝ P n) (i : Fin (n + 1)) : AffineSubspace ℝ P

An altitude of a simplex is the line that passes through a vertex and is orthogonal to the opposite face.

Equations

• s.altitude i = AffineSubspace.mk' (s.points i) (affineSpan ℝ (s.points '' {i}ᶜ)).directionᗮ ⊓ affineSpan ℝ (Set.range s.points)

theorem Affine.Simplex.altitude_def {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Simplex ℝ P n) (i : Fin (n + 1)) : s.altitude i = AffineSubspace.mk' (s.points i) (affineSpan ℝ (s.points '' {i}ᶜ)).directionᗮ ⊓ affineSpan ℝ (Set.range s.points)

The definition of an altitude.

@[simp]

theorem Affine.Simplex.altitude_reindex {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {m n : ℕ} (s : Simplex ℝ P n) (e : Fin (n + 1) ≃ Fin (m + 1)) : (s.reindex e).altitude = s.altitude ∘ ⇑e.symm

theorem Affine.Simplex.mem_altitude {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Simplex ℝ P n) (i : Fin (n + 1)) : s.points i ∈ s.altitude i

A vertex lies in the corresponding altitude.

theorem Affine.Simplex.direction_altitude {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Simplex ℝ P n) (i : Fin (n + 1)) : (s.altitude i).direction = (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)

The direction of an altitude.

theorem Affine.Simplex.vectorSpan_isOrtho_altitude_direction {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Simplex ℝ P n) (i : Fin (n + 1)) : vectorSpan ℝ (s.points '' {i}ᶜ) ⟂ (s.altitude i).direction

The vector span of the opposite face lies in the direction orthogonal to an altitude.

theorem Affine.Simplex.altitude_map {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {V₂ : Type u_3} {P₂ : Type u_4} [NormedAddCommGroup V₂] [InnerProductSpace ℝ V₂] [MetricSpace P₂] [NormedAddTorsor V₂ P₂] {n : ℕ} (s : Simplex ℝ P n) (f : P →ᵃⁱ[ℝ] P₂) (i : Fin (n + 1)) : (s.map f.toAffineMap ⋯).altitude i = AffineSubspace.map f.toAffineMap (s.altitude i)

@[simp]

theorem Affine.Simplex.map_altitude_restrict {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Simplex ℝ P n) (S : AffineSubspace ℝ P) (hS : affineSpan ℝ (Set.range s.points) ≤ S) (i : Fin (n + 1)) : AffineSubspace.map S.subtype ((s.restrict S hS).altitude i) = s.altitude i

theorem Affine.Simplex.altitude_restrict_eq_comap_subtype {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Simplex ℝ P n) (S : AffineSubspace ℝ P) (hS : affineSpan ℝ (Set.range s.points) ≤ S) (i : Fin (n + 1)) : (s.restrict S hS).altitude i = AffineSubspace.comap S.subtype (s.altitude i)

instance Affine.Simplex.finiteDimensional_direction_altitude {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Simplex ℝ P n) (i : Fin (n + 1)) : FiniteDimensional ℝ ↥(s.altitude i).direction

An altitude is finite-dimensional.

@[simp]

theorem Affine.Simplex.finrank_direction_altitude {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) : Module.finrank ℝ ↥(s.altitude i).direction = 1

An altitude is one-dimensional (i.e., a line).

theorem Affine.Simplex.affineSpan_pair_eq_altitude_iff {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) (p : P) : line[ℝ, p, s.points i] = s.altitude i ↔ p ≠ s.points i ∧ p ∈ affineSpan ℝ (Set.range s.points) ∧ p -ᵥ s.points i ∈ (affineSpan ℝ (s.points '' {i}ᶜ)).directionᗮ

A line through a vertex is the altitude through that vertex if and only if it is orthogonal to the opposite face.

noncomputable def Affine.Simplex.altitudeFoot {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) : P

The foot of an altitude is the orthogonal projection of a vertex of a simplex onto the opposite face.

Equations

• s.altitudeFoot i = ↑((s.faceOpposite i).orthogonalProjectionSpan (s.points i))

@[simp]

theorem Affine.Simplex.altitudeFoot_reindex {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {m n : ℕ} [NeZero m] [NeZero n] (s : Simplex ℝ P n) (e : Fin (n + 1) ≃ Fin (m + 1)) : (s.reindex e).altitudeFoot = s.altitudeFoot ∘ ⇑e.symm

@[simp]

theorem Affine.Simplex.altitudeFoot_map {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {V₂ : Type u_3} {P₂ : Type u_4} [NormedAddCommGroup V₂] [InnerProductSpace ℝ V₂] [MetricSpace P₂] [NormedAddTorsor V₂ P₂] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (f : P →ᵃⁱ[ℝ] P₂) (i : Fin (n + 1)) : (s.map f.toAffineMap ⋯).altitudeFoot i = f (s.altitudeFoot i)

@[simp]

theorem Affine.Simplex.altitudeFoot_restrict {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (S : AffineSubspace ℝ P) (hS : affineSpan ℝ (Set.range s.points) ≤ S) (i : Fin (n + 1)) : ↑((s.restrict S hS).altitudeFoot i) = s.altitudeFoot i

@[simp]

theorem Affine.Simplex.ne_altitudeFoot {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) : s.points i ≠ s.altitudeFoot i

@[simp]

theorem Affine.Simplex.altitudeFoot_mem_affineSpan_image_compl {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) : s.altitudeFoot i ∈ affineSpan ℝ (s.points '' {i}ᶜ)

theorem Affine.Simplex.altitudeFoot_mem_affineSpan_faceOpposite {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) : s.altitudeFoot i ∈ affineSpan ℝ (Set.range (s.faceOpposite i).points)

theorem Affine.Simplex.altitudeFoot_mem_affineSpan {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) : s.altitudeFoot i ∈ affineSpan ℝ (Set.range s.points)

theorem Affine.Simplex.affineSpan_pair_altitudeFoot_eq_altitude {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) : line[ℝ, s.altitudeFoot i, s.points i] = s.altitude i

theorem Affine.Simplex.altitudeFoot_mem_altitude {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) : s.altitudeFoot i ∈ s.altitude i

@[simp]

theorem Affine.Simplex.altitudeFoot_eq_point_rev {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : Simplex ℝ P 1) (i : Fin 2) : s.altitudeFoot i = s.points i.rev

theorem Affine.Simplex.affineSubspaceMk'_lineMap_altitudeFoot_eq_shift {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) (x : ℝ) : AffineSubspace.mk' ((AffineMap.lineMap (s.points i) (s.altitudeFoot i)) x) (s.altitude i).directionᗮ ⊓ affineSpan ℝ (Set.range s.points) = (affineSpan ℝ (s.points '' {i}ᶜ)).shift (s.points i) x

Through a point on the altitude of a simplex, draw the perpendicular plane and restrict it to the affine span of the simplex. This is the same as shifting the base towards the vertex.

theorem Affine.Simplex.closedInterior_inter_affineSubspaceMk'_lineMap_altitudeFoot {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) (x : ℝ) : s.closedInterior ∩ ↑(AffineSubspace.mk' ((AffineMap.lineMap (s.points i) (s.altitudeFoot i)) x) (s.altitude i).directionᗮ) = s.closedInterior ∩ ↑((affineSpan ℝ (s.points '' {i}ᶜ)).shift (s.points i) x)

Through a point on the altitude of a simplex, draw the perpendicular plane and find the cross section with the closed interior. This is the same as the cross section between the shifted base and the closed interior.

noncomputable def Affine.Simplex.height {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) : ℝ

The height of a vertex of a simplex is the distance between it and the foot of the altitude from that vertex.

Equations

• s.height i = dist (s.points i) (s.altitudeFoot i)

@[simp]

theorem Affine.Simplex.height_reindex {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {m n : ℕ} [NeZero m] [NeZero n] (s : Simplex ℝ P n) (e : Fin (n + 1) ≃ Fin (m + 1)) : (s.reindex e).height = s.height ∘ ⇑e.symm

@[simp]

theorem Affine.Simplex.height_map {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {V₂ : Type u_3} {P₂ : Type u_4} [NormedAddCommGroup V₂] [InnerProductSpace ℝ V₂] [MetricSpace P₂] [NormedAddTorsor V₂ P₂] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (f : P →ᵃⁱ[ℝ] P₂) (i : Fin (n + 1)) : (s.map f.toAffineMap ⋯).height i = s.height i

@[simp]

theorem Affine.Simplex.height_restrict {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (S : AffineSubspace ℝ P) (hS : affineSpan ℝ (Set.range s.points) ≤ S) (i : Fin (n + 1)) : (s.restrict S hS).height i = s.height i

@[simp]

theorem Affine.Simplex.height_pos {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) : 0 < s.height i

def Affine.Simplex.evalHeight : Mathlib.Meta.Positivity.PositivityExt

Extension for the positivity tactic: the height of a simplex is always positive.

Equations

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

@[simp]

theorem Affine.Simplex.height_eq_dist {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : Simplex ℝ P 1) (i : Fin 2) : s.height i = dist (s.points 0) (s.points 1)

The height of a 1-dimensional simplex equals to the distance between the two vertices.

theorem Affine.Simplex.inner_vsub_altitudeFoot_vsub_altitudeFoot_eq_zero {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Simplex ℝ P n) {i j : Fin (n + 1)} (h : i ≠ j) : have this := ⋯; inner ℝ (s.points j -ᵥ s.altitudeFoot i) (s.points i -ᵥ s.altitudeFoot i) = 0

Altitudes are perpendicular to the faces containing their foot.

theorem Affine.Simplex.inner_vsub_vsub_altitudeFoot_eq_height_sq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Simplex ℝ P n) [NeZero n] {i j : Fin (n + 1)} (h : i ≠ j) : inner ℝ (s.points i -ᵥ s.points j) (s.points i -ᵥ s.altitudeFoot i) = s.height i ^ 2

The inner product of an edge from j to i and the vector from the foot of i to i is the square of the height.

theorem Affine.Simplex.abs_inner_vsub_altitudeFoot_lt_mul {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Simplex ℝ P n) [n.AtLeastTwo] {i j : Fin (n + 1)} (hij : i ≠ j) : |inner ℝ (s.points i -ᵥ s.altitudeFoot i) (s.points j -ᵥ s.altitudeFoot j)| < s.height i * s.height j

The inner product of two distinct altitudes has absolute value strictly less than the product of their lengths.

Equivalently, neither vector is a multiple of the other; the angle between them is not 0 or π.

theorem Affine.Simplex.neg_mul_lt_inner_vsub_altitudeFoot {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Simplex ℝ P n) [n.AtLeastTwo] (i j : Fin (n + 1)) : -(s.height i * s.height j) < inner ℝ (s.points i -ᵥ s.altitudeFoot i) (s.points j -ᵥ s.altitudeFoot j)

The inner product of two altitudes has value strictly greater than the negated product of their lengths.

theorem Affine.Simplex.abs_inner_vsub_altitudeFoot_div_lt_one {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Simplex ℝ P n) [n.AtLeastTwo] {i j : Fin (n + 1)} (hij : i ≠ j) : |inner ℝ (s.points i -ᵥ s.altitudeFoot i) (s.points j -ᵥ s.altitudeFoot j) / (s.height i * s.height j)| < 1

theorem Affine.Simplex.neg_one_lt_inner_vsub_altitudeFoot_div {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [n.AtLeastTwo] (s : Simplex ℝ P n) (i j : Fin (n + 1)) : -1 < inner ℝ (s.points i -ᵥ s.altitudeFoot i) (s.points j -ᵥ s.altitudeFoot j) / (s.height i * s.height j)