Volume of a simplex

This file provides lemmas related to the volume of a simplex.

Main statements

• Affine.Simplex.volume_eq: The volume of a $n$-simplex is equal to $h * b / n$, where $h$ is the height and $b$ is the volume of the face.

@[simp]

theorem Affine.Simplex.volume_eq_one {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : Simplex ℝ P 0) : s.volume = 1

@[simp]

theorem Affine.Simplex.volume_eq_dist {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : Simplex ℝ P 1) : s.volume = dist (s.points 0) (s.points 1)

theorem Affine.Simplex.volume_eq {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.volume = (↑n)⁻¹ * s.height i * (s.faceOpposite i).volume

@[simp]

theorem Affine.Simplex.volume_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).volume = s.volume

@[simp]

theorem Affine.Simplex.volume_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₂) : (s.map f.toAffineMap ⋯).volume = s.volume

@[simp]

theorem Affine.Simplex.volume_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) : (s.restrict S hS).volume = s.volume

@[simp]

theorem Affine.Simplex.volume_pos {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Simplex ℝ P n) : 0 < s.volume

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

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

Equations

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