Volumes of polytopes

TheoremVolume of the cross-polytope#✓fully proved

For every integer \(n \ge 1\), the cross-polytope \(\{x \in \mathbb{R}^n : |x_1| + \dots + |x_n| \le 1\}\) in the Euclidean space \(\mathbb{R}^n\) has volume \(2^n / n!\).

theorem volume_coordinateCrossPolytope (n : ℕ) (hn : 0 < n) :
    volume {x : EuclideanSpace ℝ (Fin n) | ∑ i, |x i| ≤ 1} =
      (2 : ℝ≥0∞) ^ n / (n.factorial : ℝ≥0∞)

Sources

optimizationproblems constants/25a.md, line 44 (the polar-volume identity).

TheoremVolume of the coordinate cube#✓fully proved

For every \(n \in \mathbb{N}\), the coordinate cube \([-1, 1]^n\) in the Euclidean space \(\mathbb{R}^n\) has volume \(2^n\).

theorem volume_coordinateCube (n : ℕ) :
    volume (ConvexCovering.coordinateCube n) = (2 : ℝ≥0∞) ^ n

Sources

optimizationproblems constants/25a.md, line 44 (the cube-volume identity).

Uses 2

Statement usesCoordinate cube

Proof usesThe coordinate cube as an absolute-value box

TheoremDeterminant formula for the area of a triangle#✓fully proved

Write \(x = (x_1, x_2)\) for the coordinates of a point \(x\) of the Euclidean plane \(\mathbb{R}^2\). For all points \(a, b, c\) in \(\mathbb{R}^2\), the Lebesgue measure (area) of the convex hull of \(\{a, b, c\}\), as a real number, equals \(\frac{1}{2}\,\lvert (b_1 - a_1)(c_2 - a_2) - (b_2 - a_2)(c_1 - a_1) \rvert\).

theorem _root_.MeasureTheory.toReal_volume_convexHull_triangle
    (a b c : EuclideanSpace ℝ (Fin 2)) :
    (volume (convexHull ℝ
      ({a, b, c} : Set (EuclideanSpace ℝ (Fin 2))))).toReal =
      |(b - a).ofLp 0 * (c - a).ofLp 1 - (b - a).ofLp 1 * (c - a).ofLp 0| / 2

Used by 1

Used byMonsky's theorem

TheoremArea of the unit square#✓fully proved

The closed unit square \(\{x \in \mathbb{R}^2 : 0 \le x_1 \le 1 \text{ and } 0 \le x_2 \le 1\}\) in the Euclidean plane has Lebesgue measure (area) \(1\).

theorem _root_.MeasureTheory.volume_unitSquare :
    volume {x : EuclideanSpace ℝ (Fin 2) | ∀ i, 0 ≤ x.ofLp i ∧ x.ofLp i ≤ 1} = 1

Used by 1

Used byMonsky's theorem

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.