Convex geometry

Convex sets and convex bodies in Euclidean space: Helly-type and Radon-type theorems, partitions, sections, valuations and linear optimization over polyhedra.

TheoremIsoperimetric inequality#●ready to prove

Let \(g\) be a continuous, \(1\)-periodic, Lipschitz map from \(\mathbb{R}\) to the Euclidean plane \(\mathbb{R}^2\) that is injective on \([0, 1)\), so that its image \(C = g(\mathbb{R})\) is a simple closed curve, and suppose \(C\) has finite one-dimensional Hausdorff measure. Let \(U \subseteq \mathbb{R}^2\) be a bounded, connected open set whose boundary is \(C\). Let \(L\) be the one-dimensional Hausdorff measure of \(C\) (its length) and \(A\) the Lebesgue measure of \(U\) (its area). Then \(4 \pi A \le L^2\), and \(4 \pi A = L^2\) if and only if \(C\) is a circle, that is, \(C = \{x : \lVert x - c \rVert = r\}\) for some point \(c \in \mathbb{R}^2\) and some real \(r > 0\).

MetaMathlibExt.isoperimetric_inequality · 19 lines 
theorem_wanted isoperimetric_inequality
    {g : ℝ → EuclideanSpace ℝ (Fin 2)}
    {U : Set (EuclideanSpace ℝ (Fin 2))}
    {L A : ℝ}
    (hg_cont : Continuous g)
    (hg_closed : Function.Periodic g 1)
    (hg_lip : ∃ K, LipschitzWith K g)
    (hg_rect : MeasureTheory.Measure.hausdorffMeasure 1 (Set.range g) ≠ ⊤)
    (hg_simple : Set.InjOn g (Set.Ico (0 : ℝ) 1))
    (hL : L = (MeasureTheory.Measure.hausdorffMeasure 1 (Set.range g)).toReal)
    (hA : A = (MeasureTheory.volume U).toReal)
    (hU_open : IsOpen U)
    (hU_conn : IsConnected U)
    (hU_bdd : Bornology.IsBounded U)
    (hU_front : frontier U = Set.range g) :
    4 * Real.pi * A ≤ L ^ 2 ∧
      (4 * Real.pi * A = L ^ 2 ↔
        ∃ c : EuclideanSpace ℝ (Fin 2), ∃ r : ℝ, 0 < r ∧
          Set.range g = Metric.sphere c r)
Sources
  • https://en.wikipedia.org/wiki/Isoperimetric_inequality.

TheoremJung's theorem#✓fully proved

Let \(n \ge 1\) and let \(s\) be a bounded subset of the Euclidean space \(\mathbb{R}^n\) with diameter \(\operatorname{diam} s\). Then there is a point \(c \in \mathbb{R}^n\) such that \(s\) is contained in the closed ball with center \(c\) and radius \(\sqrt{n / (2(n + 1))} \cdot \operatorname{diam} s\).

theorem jung
    {n : ℕ} (hn : 0 < n)
    (s : Set (EuclideanSpace ℝ (Fin n)))
    (hs : Bornology.IsBounded s) :
    ∃ c : EuclideanSpace ℝ (Fin n),
      s ⊆ Metric.closedBall c (Real.sqrt ((n : ℝ) / (2 * ((n : ℝ) + 1))) * Metric.diam s)
Sources
  • H. Jung, Über die kleinste Kugel, die eine räumliche Figur einschließt, J. Reine Angew. Math. 123 (1901) 241–257 original theorem; D. Gale sharp Euclidean formulation; standard modern reference M. Berger, Geometry I & II.
Uses 1
Proof usesConvex hull of a compact set is compact

TheoremKirchberger's theorem#✓fully proved

Let \(A\) and \(B\) be finite sets of points in \(\mathbb{R}^d\). Then \(A\) and \(B\) are strictly separated by a hyperplane, that is, there are a nonzero vector \(w \in \mathbb{R}^d\) and a real number \(\beta\) with \(\langle w, a \rangle < \beta\) for all \(a \in A\) and \(\beta < \langle w, c \rangle\) for all \(c \in B\), if and only if for every set \(C \subseteq A \cup B\) of at most \(d + 2\) points, the sets \(A \cap C\) and \(B \cap C\) are strictly separated by a hyperplane in the same sense.

Proof: The reverse implication applies Helly's theorem to tagged strict half-spaces in one higher dimension, following the route of Rademacher and Schoenberg (1950) from Kirchberger (1903).

theorem kirchberger :
    ∀ (d : ℕ) (A B : Finset (EuclideanSpace ℝ (Fin d))),
      (∃ w : EuclideanSpace ℝ (Fin d), ∃ b : ℝ,
        w ≠ 0 ∧ (∀ a ∈ A, inner ℝ w a < b) ∧ (∀ c ∈ B, b < inner ℝ w c)) ↔
      ∀ C : Finset (EuclideanSpace ℝ (Fin d)), C ⊆ A ∪ B → C.card ≤ d + 2 →
        ∃ w : EuclideanSpace ℝ (Fin d), ∃ b : ℝ,
          w ≠ 0 ∧ (∀ a ∈ A ∩ C, inner ℝ w a < b) ∧
            (∀ c ∈ B ∩ C, b < inner ℝ w c)
Sources
  • https://en.wikipedia.org/wiki/Kirchberger%27s_theorem.
  • Paul Kirchberger, "Über Tchebychefsche Annäherungsmethoden," Mathematische Annalen 57 (1903), 509–540, DOI 10.1007/BF01445182, https://doi.org/10.1007/BF01445182.

TheoremRado's centerpoint theorem#✓fully proved

Let \(n \ge 1\) and let \(p_1, \dots, p_n\) be points of \(\mathbb{R}^d\), not necessarily distinct. Then some point \(x\) in the convex hull of \(\{p_1, \dots, p_n\}\) has at least \(n/(d+1)\) of the points in every closed halfspace containing it: for all \(v \in \mathbb{R}^d\) and \(t \in \mathbb{R}\) with \(\langle v, x \rangle \le t\), the number of indices \(i\) with \(\langle v, p_i \rangle \le t\) is at least \(n/(d+1)\).

theorem rado_centerpoint
    {d n : ℕ} (hn : 0 < n)
    (p : Fin n → EuclideanSpace ℝ (Fin d)) :
    ∃ x ∈ convexHull ℝ (Set.range p),
      ∀ (v : EuclideanSpace ℝ (Fin d)) (t : ℝ),
        ⟪v, x⟫_ℝ ≤ t →
          n ≤ (d + 1) * Fintype.card {i : Fin n // ⟪v, p i⟫_ℝ ≤ t}
Sources
  • R. Rado, J. London Math. Soc. s1-21 (1946), 291-300, DOI 10.1112/jlms/s1-21.4.291.

TheoremTverberg's theorem#✓fully proved

Let \(d, r\) be natural numbers with \(r \ge 1\) and let \(N = (d+1)(r-1)+1\). For any points \(p_1, \dots, p_N\) of \(\mathbb{R}^d\), not necessarily distinct, there are pairwise disjoint sets \(P_1, \dots, P_r \subseteq \{1, \dots, N\}\) whose union is \(\{1, \dots, N\}\) and a point \(x \in \mathbb{R}^d\) that lies in the convex hull of \(\{p_i : i \in P_j\}\) for every \(j\).

theorem tverberg
    {d r : ℕ} (hr : 0 < r)
    (pts : Fin ((d + 1) * (r - 1) + 1) → EuclideanSpace ℝ (Fin d)) :
    ∃ (P : Fin r → Set (Fin ((d + 1) * (r - 1) + 1)))
      (x : EuclideanSpace ℝ (Fin d)),
      (∀ i₁ i₂, i₁ ≠ i₂ → Disjoint (P i₁) (P i₂)) ∧
      (⋃ j, P j) = Set.univ ∧
      ∀ j, x ∈ convexHull ℝ (pts '' P j)
Sources
  • H. Tverberg, J. London Math. Soc. s1-41 (1966), 123-128, DOI 10.1112/jlms/s1-41.1.123.
Uses 1
Proof usesColorful Carathéodory theorem in finite-dimensional inner product spaces

TheoremUlam's flat-sections problem in dimension three#●ready to prove

Let \(K \subseteq \mathbb{R}^3\) be a compact set homeomorphic to the closed unit ball. Suppose that for every nonzero continuous linear functional \(F : \mathbb{R}^3 \to \mathbb{R}\) and every real \(c\) such that the plane \(\{x : F(x) = c\}\) meets the interior of \(K\), the intersection of this plane with the boundary (frontier) of \(K\) is homeomorphic to the unit circle. Then \(K\) is convex.

Only planes meeting the interior of \(K\) are constrained: a supporting plane can meet the boundary in a single point, as the plane \(\{x : x_1 = 1\}\) does for the closed unit ball, so requiring a circle for every plane would make the hypothesis impossible. Allowing empty or one-point sections for the other planes would still exclude convex bodies such as the cube, whose face planes meet its boundary in a square.

theorem_wanted ulamFlatSectionsConvex :
    ∀ (K : Set (EuclideanSpace ℝ (Fin 3))),
      IsCompact K →
      Nonempty (K ≃ₜ Metric.closedBall
        (0 : EuclideanSpace ℝ (Fin 3)) 1) →
      (∀ (F : EuclideanSpace ℝ (Fin 3) →L[ℝ] ℝ) (c : ℝ), F ≠ 0 →
        (∃ x ∈ interior K, F x = c) →
        Nonempty (↥(frontier K ∩ {x | F x = c}) ≃ₜ
          Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1)) →
      Convex ℝ K
Sources
  • S. Ulam, Problem 68 of the Scottish Book, asking to prove that a manifold whose every hyperplane section of its boundary is a sphere is convex. Montejano gave a complete solution, settling the problem affirmatively: L. Montejano, "About a problem of Ulam concerning flat sections of manifolds", Comment. Math. Helv. 65 (1990), 462–473; see also Montejano, "Three old problems from the Polish school of mathematics", Bol. Soc. Mat. Mex. (3) 30 (2024).
4 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.