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.

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

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.

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

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

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.

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

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