Choquet theory

TheoremChoquet representation for compact sets#✓fully proved

Let \(E\) be a second-countable real Banach space with its Borel σ-algebra and let \(K \subseteq E\) be compact. For every \(x \in K\) there is a probability measure \(\mu\) on \(E\) such that the set \(\operatorname{ext} K\) of extreme points of \(K\) has \(\mu(\operatorname{ext} K) = 1\), the identity map \(y \mapsto y\) is Bochner integrable for \(\mu\), and \(\int_E y \, d\mu(y) = x\).

Neither convexity nor nonemptiness of \(K\) is assumed; Choquet's theorem for nonempty compact convex sets is the special case.

public theorem choquet_representation_of_isCompact
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
    [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E]
    {K : Set E} (hKCompact : IsCompact K) {x : E} (hx : x ∈ K) :
    ∃ (μ : ProbabilityMeasure E),
      (μ : Measure E) (Set.extremePoints ℝ K) = 1 ∧
        Integrable (fun y : E => y) (μ : Measure E) ∧
          MeasureTheory.integral (μ : Measure E) (fun y : E => y) = x

Used by 1

Used byChoquet's theorem

TheoremChoquet's theorem#✓fully proved

Let \(E\) be a second-countable real Banach space with its Borel σ-algebra and let \(K \subseteq E\) be a nonempty compact convex set. For every \(x \in K\) there is a probability measure \(\mu\) on \(E\) such that the set \(\operatorname{ext} K\) of extreme points of \(K\) has \(\mu(\operatorname{ext} K) = 1\), the identity map \(y \mapsto y\) is Bochner integrable for \(\mu\), and \(\int_E y \, d\mu(y) = x\).

public theorem choquet_representation
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
    [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E]
    {K : Set E} (hKCompact : IsCompact K) (hKConvex : Convex ℝ K)
    (hKNonempty : K.Nonempty)
    {x : E} (hx : x ∈ K) :
    ∃ (μ : ProbabilityMeasure E),
      (μ : Measure E) (Set.extremePoints ℝ K) = 1 ∧
        Integrable (fun y : E => y) (μ : Measure E) ∧
          MeasureTheory.integral (μ : Measure E) (fun y : E => y) = x

Sources

• G. Choquet, Seminaire Bourbaki 1956 and Lectures 1962; Bishop-de Leeuw and Choquet-Bishop-de Leeuw integral representation; Phelps, Lectures on Choquet's Theorem, 1966; Lean states compact-source specialization in second-countable real Banach space with ProbabilityMeasure carried by extremePoints and Bochner integral barycenter.

Uses 1

Proof usesChoquet representation for compact sets

TheoremChoquet's representation theorem in Banach spaces#●ready to prove

Let \(X\) be a real Banach space with its Borel σ-algebra and let \(K \subseteq X\) be compact and convex. For every \(x \in K\) there is a probability measure \(\mu\) on \(X\) such that the complement of the set of extreme points of \(K\) has \(\mu\)-measure \(0\) and the barycenter \(\int y \, d\mu(y)\) (a Bochner integral) equals \(x\).

public theorem_wanted 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 ∂μ

Sources

• 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. Problem choquet_representation_theorem of the lean-eval benchmark.

TheoremBauer's uniqueness theorem at extreme points#●ready to prove

Let \(X\) be a real Banach space with its Borel σ-algebra, let \(K \subseteq X\) be compact and convex, and let \(x\) be an extreme point of \(K\). If \(\mu\) is a probability measure on \(X\) with \(\mu(X \setminus K) = 0\) whose barycenter \(\int y \, d\mu(y)\) (a Bochner integral) equals \(x\), then \(\mu\) is the Dirac measure at \(x\).

public theorem_wanted 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

Sources

• 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. Problem bauer_extreme_point_uniqueness of the lean-eval benchmark.

2 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.