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)

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.

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.

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) : affineSpan ℝ {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.

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

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)) : affineSpan ℝ {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

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)

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.