Bauer's uniqueness at extreme points

bauer_extreme_point_uniqueness

Submitter: Kim Morrison.

Notes: If x is an extreme point of a compact convex set K in a Banach space and μ is a probability measure on K (μ Kᶜ = 0) with barycenter x = ∫ y ∂μ, then μ is the Dirac mass at x. The support hypothesis is the weaker μ Kᶜ = 0, making this a strengthening of the textbook statement (uniqueness among all ambient Borel probability measures on K, not only those supported on ext K). Not in Mathlib (no Choquet simplices / Bauer's theorem); no new definitions. Companion candidate from §88 of the Knill survey.

Source: H. Bauer, *Minimalstellen von Funktionen und Extremalpunkte*, Arch. Math. 9 (1958), 389–393; see also Phelps, *Lectures on Choquet's Theorem*. Knill, *Some fundamental theorems in mathematics*, §88.

Informal solution: Since x is extreme, it is not a nontrivial convex combination, and the barycenter map is injective at extreme points. Argument: suppose μ ≠ δ_x. Then μ is not concentrated at x, so there is a closed half-space / continuous affine functional separating part of the mass; split μ = t·μ₁ + (1−t)·μ₂ with distinct barycenters b₁ ≠ b₂ both in K whose convex combination is x, contradicting extremality of x. Hence μ({x}) = 1, i.e. μ = Measure.dirac x. (Uses that the barycenter ∫ y ∂μ is well defined — μ Kᶜ = 0 with K compact makes id integrable.)

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

Solved by

Not yet solved.