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.

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.

@[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)) : 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.

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

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 : ℕ} [NeZero n] (s : Simplex ℝ P 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 : ℕ} [NeZero n] (s : Simplex ℝ P n) {i j : Fin (n + 1)} (hij : i ≠ j) (hn : 1 < n) : |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 : ℕ} [NeZero n] (s : Simplex ℝ P n) (i j : Fin (n + 1)) (hn : 1 < n) : -(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 : ℕ} [NeZero n] (s : Simplex ℝ P n) {i j : Fin (n + 1)} (hij : i ≠ j) (hn : 1 < n) : |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 : ℕ} [NeZero n] (s : Simplex ℝ P n) (i j : Fin (n + 1)) (hn : 1 < n) : -1 < inner ℝ (s.points i -ᵥ s.altitudeFoot i) (s.points j -ᵥ s.altitudeFoot j) / (s.height i * s.height j)