Maximal Positive-Volume Simplex in a Compact Set

This establishes existence of a maximal-volume simplex in a compact set with nonempty interior.

Let $K\subseteq\mathbb R^n$ be compact and assume $\operatorname{int}(K)\ne\varnothing$. Then there exists a map $v:\operatorname{Fin}(n+1)\to\mathbb R^n$ such that:

1. Every vertex $v_i$ belongs to $K$.
2. The simplex edge matrix has positive determinant magnitude:

3. Every other $(n+1)$-tuple $w$ of points in $K$ has no larger determinant magnitude:

The declaration is exists_max_simplexEdgeMatrix_det_readable. It is the compactness and normalization step for selecting a nondegenerate maximal simplex.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

theorem exists_max_simplexEdgeMatrix_det {n : ℕ} {K : Set (EuclideanSpace ℝ (Fin n))}
    (hK : IsCompact K) (hint : (interior K).Nonempty) :
    ∃ v : Fin (n + 1) → EuclideanSpace ℝ (Fin n), (∀ i, v i ∈ K) ∧
      0 < |(simplexEdgeMatrix v).det| ∧
      ∀ w : Fin (n + 1) → EuclideanSpace ℝ (Fin n), (∀ i, w i ∈ K) →
        |(simplexEdgeMatrix w).det| ≤ |(simplexEdgeMatrix v).det|

Module navigation

Module: Analysis/Convex/Normalization.

Next: abs_simplexCoord_le_one_of_max.

Source excerpt, lines 31–36 · Frozen source 408915f.