Simplex Coordinates Bounded by Maximality

This is an auxiliary geometric statement for affine normalization of a convex body.

Let $n\in\mathbb N$, let $K\subseteq \operatorname{EuclideanSpace}(\mathbb R,\operatorname{Fin}(n))$, and let $v_0,\ldots,v_n\in K$. Write $M=\operatorname{simplexEdgeMatrix}(v)$ and assume:

1. $\det M\ne 0$.
2. For every $w_0,\ldots,w_n\in K$, $|\det(\operatorname{simplexEdgeMatrix}(w))|\le |\det M|$.

Then every $y\in K$ has simplex coordinates $c=M^{-1}(y-v_0)$ satisfying

The declaration abs_simplexCoord_le_one_of_max_readable is a reusable box bound for coordinates relative to a maximal-volume nondegenerate simplex. No convexity of $K$ is assumed explicitly.

Original Lean declaration header

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

theorem abs_simplexCoord_le_one_of_max {n : ℕ} {K : Set (EuclideanSpace ℝ (Fin n))}
    {v : Fin (n + 1) → EuclideanSpace ℝ (Fin n)} (hv : ∀ i, v i ∈ K)
    (hdet : (simplexEdgeMatrix v).det ≠ 0)
    (hmax : ∀ w : Fin (n + 1) → EuclideanSpace ℝ (Fin n), (∀ i, w i ∈ K) →
      |(simplexEdgeMatrix w).det| ≤ |(simplexEdgeMatrix v).det|)
    {y : EuclideanSpace ℝ (Fin n)} (hy : y ∈ K) :
    (∀ j, |((simplexEdgeMatrix v)⁻¹ *ᵥ (y - v 0 : EuclideanSpace ℝ (Fin n)).ofLp) j| ≤ 1) ∧
      |1 - ∑ j, ((simplexEdgeMatrix v)⁻¹ *ᵥ (y - v 0 : EuclideanSpace ℝ (Fin n)).ofLp) j| ≤ 1

Module navigation

Module: Analysis/Convex/Normalization.

Previous: exists_max_simplexEdgeMatrix_det · Next: closedBall_subset_stdSimplex_and_box_subset_closedBall.

Source excerpt, lines 176–183 · Frozen source 408915f.