Choquet's representation theorem

choquet_representation_theorem

Submitter: Kim Morrison.

Notes: In a Banach space, every point of a compact convex set K is the barycenter ∫ y ∂μ of a probability measure μ supported on the extreme points of K (μ (ext K)ᶜ = 0). A norm-compact set is metrizable, so the extreme points are Borel and Choquet's theorem proper applies; the literal 'supported on ext K' rendering is faithful. Mathlib has Krein–Milman (closure_convexHull_extremePoints) and Convex.integral_mem but not Choquet's theorem, and no measure-theoretic barycenter operator. No new definitions beyond Mathlib's Set.extremePoints, IsProbabilityMeasure, and the Bochner integral. Candidate from §88 of the Knill survey.

Source: G. Choquet, *Existence et unicité des représentations intégrales au moyen des points extrémaux dans les cônes convexes*, Séminaire Bourbaki (1956). Knill, *Some fundamental theorems in mathematics*, §88.

Informal solution: For metrizable compact convex K, build the representing measure by the classical Choquet argument: choose a strictly convex lower-semicontinuous function and maximize ∫ over probability measures with barycenter x; a maximizer is supported on the extreme points (a non-extreme support point would admit a dilation strictly increasing the integral). Concretely, take a strictly convex continuous f, let μ maximize ∫ f over the (weak-* compact, convex) set of probability measures with barycenter x; maximality in the Choquet ordering forces a maximal representing measure, which in the metrizable compact case can be chosen supported on ext K. Use Krein–Milman / Bauer's maximum principle and the Choquet ordering on measures.

theorem declaration uses `sorry`choquet [MeasurableSpace X] [BorelSpace X]
    (K : Set X) (hK_cpt : IsCompact K) (hK_cvx : Convex ℝ K)
    {x : X} (hx : x ∈ K) :
    ∃ μ : Measure X, IsProbabilityMeasure μ ∧
      μ (K.extremePoints ℝ)ᶜ = 0 ∧
      x = ∫ y, y ∂μ := byX:Type u_1inst✝⁴:NormedAddCommGroup Xinst✝³:NormedSpace ℝ Xinst✝²:CompleteSpace Xinst✝¹:MeasurableSpace Xinst✝:BorelSpace XK:Set XhK_cpt:IsCompact KhK_cvx:Convex ℝ Kx:Xhx:x ∈ K⊢ ∃ μ, IsProbabilityMeasure μ ∧ μ (Set.extremePoints ℝ K)ᶜ = 0 ∧ x = ∫ (y : X), y ∂μ
  sorryAll goals completed! 🐙

Solved by

• @GanjinZero with Seed Prover (ByteDance) on Jun 10, 2026