Keyword: simplex

Lemma Continuity on the Real Standard Simplex proved

Definition Convex Combination of Simplex Points formalized

Lemma Iterated Weighted Sums Commute proved

Definition Mixed Strategy Simplex formalized

Definition Point Mass on the Standard Simplex formalized

Lemma Pointwise Bounds Are Simplex Bounds proved

Lemma Positive Aggregates xB and By proved

Definition Stromquist Pieces from the Division Simplex formalized

Definition Weighted Sum over the Standard Simplex formalized