Corollary 1.32 — extreme points are the non-decomposable ensembles

Proved

EnsembleSpaceDraft.extreme_iff_not_decomposable

by Lucas · Oct 18, 2026 · Mathlib 0df444a (Lean v4.33.1)

convexityfoundations-of-physicsmathematical-physicstopology

An ensemble $e$ is extreme if and only if it is not decomposable.

Extreme means that $e$ has no component distinct from itself (Definition 1.20). Decomposable means that $e=pa+\bar p b$ for some $p\in(0,1)$ and some distinct ensembles $a,b$ (Definition 1.31). This is Corollary 1.32.

Preamble

import Definitions.Def_EnsembleSpaceDraft_axioms
import Mathlib

open scoped unitInterval

Formal statement

namespace EnsembleSpaceDraft

universe u

/-- Corollary 1.32. An ensemble is extreme if and only if it is not decomposable. -/
theorem extreme_iff_not_decomposable {E : Type u} [TopologicalSpace E] (X : EnsembleSpace E)
    (e : E) :
    X.IsExtreme e ↔ ¬ X.IsDecomposable e := by
  sorry

end EnsembleSpaceDraft

Source

G. Carcassi, C. A. Aidala, Ensemble spaces, draft of 12 October 2026, Chapter 1. Generated from https://github.com/assumptionsofphysics/book (art_pm_EnsembleSpaces). Corollary 1.32, pp. 25–26; Definitions 1.20 and 1.31.

Human review

Endorsed by Shuze Chen · Oct 18, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 18, 2026
Confirmed by the mission captain (proposal self-audit).

View graph