Affine normalization of convex bodies

A convex body in an n-dimensional real affine space can be moved by an affine equivalence to a position between two balls whose radii depend only on the space. This is the normalization that lets estimates for convex sets be proved for sets of unit size and transferred back; in the regularity theory of the Monge–Ampère equation it is applied to the sections {y | u y < u x + ⟪p, y - x⟫ + h} of a convex function u.

The normalization comes from a simplex of maximal volume. Let K be a compact set whose affine span is the whole n-dimensional space, and choose n + 1 points of K spanning a simplex of maximal volume, where volume is measured by the absolute value of the determinant of the matrix of barycentric coordinates relative to a fixed affine basis (the determinant itself is the signed volume). Replacing the vertex b i by a point x multiplies this determinant by the barycentric coordinate b.coord i x (AffineBasis.det_toMatrix_update), so maximality of its absolute value forces |b.coord i x| ≤ 1 for every x ∈ K (IsCompact.exists_affineBasis_abs_coord_le_one).

In terms of the simplex Δ = convexHull (range b) with centroid c, the points whose barycentric coordinates are all at most 1 form the image of Δ under the homothety of ratio -n about c (AffineBasis.mem_image_homothety_convexHull_iff). Thus every compact spanning K contains the vertices of a simplex Δ and lies inside its homothetic image of ratio -n (IsCompact.exists_affineBasis_subset_image_homothety_convexHull); when K is convex it contains Δ itself. Mapping Δ to a fixed reference simplex by an affine equivalence then gives the normalization by balls (TauCeti.exists_affineEquiv_ball_subset_image_subset_ball).

John's theorem gives the sharper statement in which the simplex is replaced by the ellipsoid of maximal volume and the ratio -n by n, or by √n for centrally symmetric bodies. For the normalization, a ratio depending only on the dimension suffices.

Main statements

• IsCompact.exists_affineBasis_abs_coord_le_one: a compact set spanning a finite-dimensional real affine space contains an affine basis relative to which all its points have barycentric coordinates in [-1, 1];
• AffineBasis.mem_image_homothety_convexHull_iff: the image of the simplex of an affine basis under the homothety of ratio -n about its centroid is the set of points whose barycentric coordinates are at most 1;
• IsCompact.exists_affineBasis_subset_image_homothety_convexHull: a compact spanning set contains the vertices of a simplex and lies in the image of that simplex under the homothety of ratio -n about its centroid;
• TauCeti.exists_affineEquiv_ball_subset_image_subset_ball: in a finite-dimensional real normed space there is r > 0 such that every bounded convex set with nonempty interior is mapped by some affine equivalence to a set between the balls of radii r and 1 about 0.

References

• F. John, Extremum problems with inequalities as subsidiary conditions, Studies and Essays Presented to R. Courant on his 60th Birthday, Interscience, 1948, 187–204.
• C. E. Gutiérrez, The Monge–Ampère Equation, 2nd ed., Progress in Nonlinear Differential Equations and Their Applications 89, Birkhäuser, 2016, §1.8 (normalized convex sets).
• K. Ball, An elementary introduction to modern convex geometry, in Flavors of Geometry, MSRI Publications 31, Cambridge University Press, 1997, Lecture 3.

A simplex of maximal volume

theorem IsCompact.exists_affineBasis_abs_coord_le_one {ι : Type u_1} {V : Type u_2} {P : Type u_3} [Fintype ι] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] [PseudoMetricSpace P] [NormedAddTorsor V P] {K : Set P} (hK : IsCompact K) (hspan : affineSpan ℝ K = ⊤) (hι : Fintype.card ι = Module.finrank ℝ V + 1) : ∃ (b : AffineBasis ι ℝ P), (∀ (i : ι), b i ∈ K) ∧ ∀ x ∈ K, ∀ (i : ι), |(b.coord i) x| ≤ 1

Affine bases with bounded barycentric coordinates. A compact set K whose affine span is the whole finite-dimensional real affine space contains an affine basis b, indexed by any type with finrank + 1 elements, such that every point of K has all its barycentric coordinates relative to b in [-1, 1].

The homothetic image of a simplex

theorem AffineBasis.mem_image_homothety_convexHull_iff {ι : Type u_1} {k : Type u_2} {E : Type u_3} [Fintype ι] [Field k] [LinearOrder k] [IsStrictOrderedRing k] [AddCommGroup E] [Module k E] (b : AffineBasis ι k E) {x : E} : x ∈ ⇑(AffineMap.homothety (Finset.centroid k Finset.univ ⇑b) (-↑(Module.finrank k E))) '' (convexHull k) (Set.range ⇑b) ↔ ∀ (i : ι), (b.coord i) x ≤ 1

The image of the simplex spanned by an affine basis of an n-dimensional space under the homothety of ratio -n about its centroid is the set of points whose barycentric coordinates are all at most 1.

theorem IsCompact.exists_affineBasis_subset_image_homothety_convexHull {ι : Type u_1} {E : Type u_2} [Fintype ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} (hK : IsCompact K) (hspan : affineSpan ℝ K = ⊤) (hι : Fintype.card ι = Module.finrank ℝ E + 1) : ∃ (b : AffineBasis ι ℝ E), (∀ (i : ι), b i ∈ K) ∧ K ⊆ ⇑(AffineMap.homothety (Finset.centroid ℝ Finset.univ ⇑b) (-↑(Module.finrank ℝ E))) '' (convexHull ℝ) (Set.range ⇑b)

Affine normalization of compact sets. A compact set K whose affine span is the whole n-dimensional real normed space contains the vertices of a simplex Δ and lies in the image of Δ under the homothety of ratio -n about the centroid of Δ. When K is convex, it also contains Δ, by convexHull_min.

Normalization by balls

theorem TauCeti.exists_affineEquiv_ball_subset_image_subset_ball (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] : ∃ r > 0, ∀ (s : Set E), Convex ℝ s → Bornology.IsBounded s → (interior s).Nonempty → ∃ (T : E ≃ᵃ[ℝ] E), Metric.ball 0 r ⊆ ⇑T '' s ∧ ⇑T '' s ⊆ Metric.ball 0 1

Normalization of convex bodies. In a finite-dimensional real normed space E there is a radius r > 0, depending only on E, such that every bounded convex set s with nonempty interior is mapped by some affine equivalence T to a set between the balls of radii r and 1 about 0.