QuantumInfo.ForMathlib.Minimax

Let $\beta$ be a topological space and $\alpha$ be a topological space equipped with a linear order such that all lower rays $(-\infty, a]$ are closed (a closed-interval-of-comparison topology). Let $s \subseteq \beta$ be a non-empty compact set. If a function $f: \beta \to \alpha$ is lower semicontinuous on $s$, then there exists some $x \in s$ such that $f(x)$ is the minimum value of $f$ on $s$.

Let $\mathbf{k}$ be a semiring equipped with a partial order, and let $E$ and $\beta$ be modules over $\mathbf{k}$ where $\beta$ is also an ordered additive monoid satisfying the property that scalar multiplication by positive elements is monotonic ($PosSMulMono$). If $f: E \to \beta$ is a $\mathbf{k}$-linear map and $s \subseteq E$ is a convex set, then $f$ is quasilinear on $s$.

Let $\mathbf{k}$ be a semiring with a partial order, and let $E$ and $\beta$ be modules over $\mathbf{k}$ that are also additive commutative monoids. Suppose $\beta$ is an ordered additive monoid where scalar multiplication by positive elements is monotonic. Let $s \subseteq E$ be a convex set. For any $\mathbf{k}$-linear map $f: E \to \beta$, the restriction of $f$ to $s$ is quasiconvex.

Let $\mathbf{k}$ be a ordered semiring, and let $E$ and $\beta$ be modules over $\mathbf{k}$ such that $\beta$ is an ordered additive monoid with covariant scalar multiplication. If $f: E \to \beta$ is a linear map and $s \subseteq E$ is a convex set, then $f$ is quasiconcave on $s$.

Let $M$ and $N$ be real normed additive commutative groups that are also modules over $\mathbb{R}$, with $M$ being finite-dimensional. Let $f: N \to L(\mathbb{R}; L(M; \mathbb{R}))$ be a continuous linear map (representing a family of continuous linear functionals). Then the evaluation map $(x, y) \mapsto f(x)(y)$ from $N \times M$ to $\mathbb{R}$ is continuous.

Let $M$ be a finite-dimensional real normed topological vector space and $N$ be a real normed topological vector space. Let $f: N \to L(M, \mathbb{R})$ be a continuous bilinear form (represented as a continuous linear map from $N$ to the dual space of $M$). Given two sets $S \subseteq M$ and $T \subseteq N$ such that: 1. $S$ and $T$ are compact, 2. $S$ and $T$ are convex, 3. $S$ and $T$ are nonempty, then the following equality holds: $$\inf_{x \in T} \sup_{y \in S} f(x, y) = \sup_{y \in S} \inf_{x \in T} f(x, y)$$

Let $M$ be a finite-dimensional real normed topological vector space. Let $f: M \times M \to \mathbb{R}$ be a bilinear form on $M$. Let $S$ and $T$ be subsets of $M$ such that: 1. $S$ and $T$ are compact, 2. $S$ and $T$ are convex, 3. $S$ and $T$ are nonempty, then the following equality holds: $$\inf_{x \in T} \sup_{y \in S} f(x, y) = \sup_{y \in S} \inf_{x \in T} f(x, y)$$

Let $M$ be a finite-dimensional real normed additive commutative group (a finite-dimensional real Banach space) with continuous addition and scalar multiplication. Let $f: M \times M \to \mathbb{R}$ be a bilinear form on $M$. Let $S$ and $T$ be subsets of $M$ such that both $S$ and $T$ are compact, convex, and nonempty. Then the supremum of the infimum equals the infimum of the supremum: $$\sup_{x \in S} \inf_{y \in T} f(x, y) = \inf_{y \in T} \sup_{x \in S} f(x, y)$$