PhyslibAlpha.Mathematics.Convex.Choquet.ExtremePointDecomposition

Given a metrizable topological space $S$, `Choquet.choquetMetric` provides a metric space structure on $S$ such that the topology induced by the metric coincides with the original topology of $S$.

The function maps a pair of points $x, y$ in the space $S$ to the real-valued distance $d(x, y)$ between them, as defined by the metric structure `choquetMetric`.

Let $S$ be a compact convex metrizable set. For any two points $x, y \in S$, if $x \neq y$, then the distance $d(x, y)$ between them is strictly positive, where $d$ denotes the metric defined on $S$ (represented by `cdist` in the formalization).

The distance function $f: S \times S \to \mathbb{R}$ defined by $f(x, y) = \text{cdist}(x, y)$ is continuous, where $\text{cdist}$ is the distance metric defined on the space $S$.

For any natural number $n$ and points $x, y \in S$, if the distance $d(x, y)$ satisfies $d(x, y) \geq \frac{1}{n+1}$, then $x \neq y$.

Let $S$ be a compact space. For any natural number $n$, the set of pairs $(x, y) \in S \times S$ such that $d(x, y) \geq \frac{1}{n+1}$ is compact, where $d$ denotes the distance function on $S$.

For a given natural number $n$, this defines the subspace of $S \times S$ consisting of pairs of points $(x, y)$ such that the distance $d(x, y)$ between them is at least $\frac{1}{n+1}$.

Let $S$ be a compact space equipped with a distance function $d$. For any natural number $n$, the subspace of $S \times S$ defined by the set of pairs $(x, y)$ such that $d(x, y) \geq \frac{1}{n+1}$ is a compact space.

For any natural number $n$, let $D_n \subseteq S \times S$ be the subspace consisting of pairs of points $(x, y)$ such that the distance between them satisfies $d(x, y) \geq \frac{1}{n+1}$. The projection map from $D_n$ to $S$ that sends a pair $(x, y)$ to its first component $x$ is continuous.

For any natural number $n$, let $D_n$ be the subspace of $S \times S$ consisting of pairs of points $(x, y)$ such that the distance $d(x, y) \geq \frac{1}{n+1}$. The projection map $\text{pr}_2 : D_n \to S$, which sends a pair $(x, y)$ to its second component $y$, is continuous.

For a given natural number $n$, the set consists of the midpoints $\frac{1}{2}x + \frac{1}{2}y$ of all pairs of points $(x, y) \in S \times S$ such that the distance between them satisfies $d(x, y) \geq \frac{1}{n+1}$.

Let $S$ be a compact convex set in a metrizable space. For any natural number $n$, the set of midpoints $\frac{1}{2}x + \frac{1}{2}y$ of all pairs of points $(x, y) \in S \times S$ such that the distance between them satisfies $d(x, y) \geq \frac{1}{n+1}$ is a closed set.

Let $S$ be a compact convex subset of a vector space $V$. The set of points in $S$ that are not extreme points is equal to the union $\bigcup_{n \in \mathbb{N}} M_n$, where $M_n$ is the set of midpoints $\frac{1}{2}y + \frac{1}{2}z$ of all pairs of points $(y, z) \in S \times S$ such that the distance between them satisfies $d(y, z) \geq \frac{1}{n+1}$.

Let $S$ be a compact convex subset of a vector space $V$ that is metrizable and whose points are separated by countably many continuous linear functionals. The set of extreme points of $S$ is a Borel measurable set.

For a natural number $n$, let $D_n$ be the subspace of $S \times S$ consisting of pairs of points $(x, y)$ such that their distance satisfies $d(x, y) \geq \frac{1}{n+1}$. This function maps such a pair $p = (x, y) \in D_n$ to its midpoint $\frac{1}{2}x + \frac{1}{2}y$ in $S$.

For any natural number $n$, let $D_n$ be the subspace of $S \times S$ consisting of pairs of points $(x, y)$ such that the distance between them satisfies $d(x, y) \geq \frac{1}{n+1}$. The function that maps each pair $(x, y) \in D_n$ to its midpoint $\frac{1}{2}x + \frac{1}{2}y \in S$ is continuous.

Let $S$ be a compact convex metrizable set. For any natural number $n$, let $D_n = \{ (x, y) \in S \times S \mid d(x, y) \geq \frac{1}{n+1} \}$ be the decomposition space and $M_n = \{ \frac{1}{2}x + \frac{1}{2}y \mid (x, y) \in D_n \}$ be the set of midpoints of pairs in $D_n$. If $\mu$ is a probability measure on $S$ such that $\mu(M_n) \neq 0$, then there exists a probability measure $\rho$ on $D_n$ whose pushforward under the midpoint map $m : D_n \to S$ (defined by $m(x, y) = \frac{1}{2}x + \frac{1}{2}y$) is equal to the conditional probability measure of $\mu$ restricted to $M_n$.

Let $S$ be a compact convex metrizable set. For any natural number $n$, let $D_n$ be the decomposition space consisting of pairs $(x, y) \in S \times S$ such that their distance $d(x, y) \geq \frac{1}{n+1}$. Given a probability measure $\rho$ on $D_n$, a continuous function $f: S \to \mathbb{R}$, and a continuous map $g: D_n \to S$, then the composition $f \circ g$ is integrable with respect to the measure $\rho$.

Let $S$ be a compact convex metrizable set. For a natural number $n$, let $D_n \subseteq S \times S$ be the decomposition space consisting of pairs $(x, y)$ such that the distance $d(x, y) \geq \frac{1}{n+1}$. Let $m: D_n \to S$ be the midpoint map defined by $m(x, y) = \frac{1}{2}x + \frac{1}{2}y$. If $\rho$ is a probability measure on $D_n$ and $\nu$ is a probability measure on $S$ such that $\nu$ is the pushforward of $\rho$ under $m$ (denoted $\nu = m_*\rho$), then for any continuous function $f: S \to \mathbb{R}$, the following integral identity holds: $$\int_S f(w) \, d\nu(w) = \int_{D_n} f(m(p)) \, d\rho(p)$$

Given a compact convex set $S$ and a natural number $n$, let $X_n \subseteq S \times S$ be the decomposition space consisting of pairs $(x, y)$ such that the distance $d(x, y) \geq \frac{1}{n+1}$. For a probability measure $\rho$ on $X_n$, the endpoint measure is the probability measure on $S$ obtained by distributing half of the mass of $\rho$ onto the first components and half onto the second components of the pairs. Formally, for any continuous function $f \in C(S, \mathbb{R})$, the integral with respect to this measure is given by: $$\int_S f \, d(\text{endpointMeasure}_n(\rho)) = \int_{X_n} \frac{1}{2} (f(x) + f(y)) \, d\rho(x, y)$$

Let $S$ be a compact convex set and $n$ be a natural number. Let $X_n \subseteq S \times S$ be the decomposition space consisting of pairs of points $(x, y)$ such that the distance $d(x, y) \geq \frac{1}{n+1}$. For any probability measure $\rho$ on $X_n$ and any continuous function $f \in C(S, \mathbb{R})$, the integral of $f$ with respect to the endpoint measure $\text{endpointMeasure}_n(\rho)$ is: $$\int_S f \, d(\text{endpointMeasure}_n(\rho)) = \int_{X_n} \frac{1}{2} (f(x) + f(y)) \, d\rho(x, y)$$

Let $S$ be a compact convex set. For a natural number $n$, let $T_n$ be the set of midpoints $\frac{1}{2}x + \frac{1}{2}y$ of pairs of points $(x, y) \in S \times S$ whose distance satisfies $d(x, y) \geq \frac{1}{n+1}$, and let $X_n$ be the space of all such pairs. Let $\mu$ be a probability measure on $S$ such that $\mu(T_n) \neq 0$, and let $\mu|_{T_n}$ denote the conditional probability measure of $\mu$ on $T_n$. Suppose $\rho$ is a probability measure on $X_n$ such that its pushforward under the midpoint map $m(x, y) = \frac{1}{2}x + \frac{1}{2}y$ is $\mu|_{T_n}$. Then the conditional measure $\mu|_{T_n}$ is less than or equal to the endpoint measure $\nu_\rho$ in the Choquet order, where $\nu_\rho$ is the probability measure on $S$ defined by the property that for any continuous function $f: S \to \mathbb{R}$: $$\int_S f \, d\nu_\rho = \int_{X_n} \frac{1}{2} (f(x) + f(y)) \, d\rho(x, y).$$

Let $S$ be a convex set. Let $\mu$ and $\eta$ be probability measures on $S$, and let $T \subseteq S$ be a measurable set such that $\mu(T) \neq 0$. Let $\mu|_T$ denote the conditional probability measure of $\mu$ on $T$, and let $\mu'$ be the probability measure obtained by replacing the mass of $\mu$ on $T$ with $\eta$. If $\mu|_T \le \eta$ in the Choquet order, then $\mu \le \mu'$ in the Choquet order. That is, if for every continuous convex function $f: S \to \mathbb{R}$ it holds that $$\int_S f \, d(\mu|_T) \le \int_S f \, d\eta,$$ then for every continuous convex function $f: S \to \mathbb{R}$, $$\int_S f \, d\mu \le \int_S f \, d\mu'.$$

Let $S$ be a topological space. Let $\mu$ and $\eta$ be probability measures on $S$, and let $T \subseteq S$ be a measurable set such that $\mu(T) \neq 0$. Let $\mu|_T$ denote the conditional probability measure of $\mu$ on $T$. Suppose $f: S \to \mathbb{R}$ is a continuous function such that the integral of $f$ with respect to the conditional measure $\mu|_T$ is strictly less than the integral of $f$ with respect to $\eta$: $$\int_S f(w) \, d(\mu|_T)(w) < \int_S f(w) \, d\eta(w).$$ Then the integral of $f$ with respect to $\mu$ is strictly less than the integral of $f$ with respect to the probability measure $\mu'$ obtained by replacing the mass of $\mu$ on $T$ with $\eta$: $$\int_S f(w) \, d\mu(w) < \int_S f(w) \, d\mu'(w).$$

Given a continuous linear functional $\ell: V \to \mathbb{R}$ and a compact convex set $S \subseteq V$, the function `squaredEvaluation` is the continuous real-valued function on $S$ defined by $x \mapsto (\ell(x))^2$.

Let $V$ be a real topological vector space and $S \subseteq V$ be a convex set. For any continuous linear functional $\ell: V \to \mathbb{R}$, the function $f: S \to \mathbb{R}$ defined by $f(x) = (\ell(x))^2$ is a convex function on $S$. That is, for all $x, y \in S$ and $t \in [0, 1]$, the inequality $(\ell(tx + (1-t)y))^2 \le t(\ell(x))^2 + (1-t)(\ell(y))^2$ holds.

Let $S$ be a compact convex set whose points are separated by a countable sequence of continuous linear functionals $\{\ell_i\}_{i \in \mathbb{N}}$. Let $D_n$ be the subspace of $S \times S$ consisting of pairs of points $(x, y)$ such that their distance $d(x, y)$ satisfies $d(x, y) \geq \frac{1}{n+1}$. For any probability measure $\rho$ on $D_n$, there exists an index $i$ such that the set of pairs $(x, y) \in D_n$ for which $\ell_i(x) \neq \ell_i(y)$ has non-zero measure with respect to $\rho$.

Let $S$ be a compact convex subset of a topological vector space $V$ whose points are separated by a countable sequence of continuous linear functionals $\{\ell_i\}_{i \in \mathbb{N}}$. For any natural number $n$, let $D_n = \{(x, y) \in S \times S \mid d(x, y) \geq \frac{1}{n+1} \}$ be the space of pairs of points in $S$ separated by a distance of at least $1/(n+1)$. For any probability measure $\rho$ on $D_n$, there exists an index $i$ such that the integral of the squared functional $\ell_i^2$ over the midpoints $\frac{x+y}{2}$ is strictly less than the integral of $\ell_i^2$ with respect to the endpoint measure $\mu_{\text{end}}$: $$\int_{D_n} \left( \ell_i \left( \frac{x+y}{2} \right) \right)^2 d\rho(x, y) < \int_S \ell_i(w)^2 d\mu_{\text{end}}(w)$$ where the endpoint measure $\mu_{\text{end}}$ is defined such that for any continuous function $f$, $\int_S f \, d\mu_{\text{end}} = \int_{D_n} \frac{1}{2}(f(x) + f(y)) \, d\rho(x, y)$.

Let $S$ be a compact convex subset of a topological vector space. Let $\mu$ be a probability measure on $S$ that is Choquet maximal at a point $x \in S$. For any natural number $n \in \mathbb{N}$, let $M_n$ be the set of midpoints $\frac{1}{2}a + \frac{1}{2}b$ of pairs of points $(a, b) \in S \times S$ whose distance satisfies $d(a, b) \geq \frac{1}{n+1}$. Then the measure of $M_n$ with respect to $\mu$ is zero, i.e., $\mu(M_n) = 0$.

Let $S$ be a compact convex subset of a topological vector space $V$ that is metrizable and whose points are separated by countably many continuous linear functionals. Let $x \in S$ be a point and $\mu$ be a probability measure on $S$. If $\mu$ is Choquet maximal at $x$ (meaning $\mu$ represents $x$ and is maximal with respect to the Choquet order), then $\mu$ is concentrated on the extreme points of $S$. That is, for $\mu$-almost every $y \in S$, $y$ is an extreme point of $S$.

Let $S$ be a compact convex subset of a topological vector space $V$. For every point $x \in S$, there exists a probability measure $\mu$ on $S$ that represents $x$ and is concentrated on the extreme points of $S$. That is, for every continuous linear functional $\ell \colon V \to \mathbb{R}$, we have $$\ell(x) = \int_S \ell(y) \, d\mu(y)$$ and $\mu$-almost every $y \in S$ is an extreme point of $S$.