QuantumInfo.ForMathlib.SionMinimax

Let $f: \alpha \times \beta \to \gamma$ be a function of two variables. For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, the image of $t \times s$ under the flipped function $\tilde{f}(y, x) = f(x, y)$ is equal to the image of $s \times t$ under the original function $f$. That is, $\{ f(x, y) \mid x \in s, y \in t \} = \{ \tilde{f}(y, x) \mid y \in t, x \in s \}$.

Let $\alpha$ be a conditionally complete lattice, and let $\iota$ and $\iota'$ be index types where $\iota$ is nonempty. Let $f : \iota \times \iota' \to \alpha$ be a function. Suppose that for every $j \in \iota'$, the set $\{f(i, j) \mid i \in \iota\}$ is bounded above, and for every $i \in \iota$, the set $\{f(i, j) \mid j \in \iota'\}$ is bounded below. Then the supremum of the infima is less than or equal to the infimum of the suprema: $$\sup_{i \in \iota} \inf_{j \in \iota'} f(i, j) \le \inf_{j \in \iota'} \sup_{i \in \iota} f(i, j)$$

Let $f, g: X \to \mathbb{R}$ (or any conditionally complete lattice) be two functions. If the range of $f$ is bounded above and the range of $g$ is bounded above, then the range of the function defined by $x \mapsto \max(f(x), g(x))$ is also bounded above.

Let $f, g: \iota \to \alpha$ be two functions into a conditionally complete linear order $\alpha$. If the ranges of $f$ and $g$ are both bounded below, then the range of their pointwise minimum, defined by $(f \wedge g)(x) = \min(f(x), g(x))$, is also bounded below.

Let $f: \iota \to \mathbb{R}$ (or any conditionally complete lattice) be a function and $S, T \subseteq \iota$ be sets such that the image $f(S)$ is bounded below. If the intersections $S \cap T$ and $S \setminus T$ are both non-empty, then the infimum of $f$ over $S$ is equal to the minimum of the infimum of $f$ over $S \cap T$ and the infimum of $f$ over $S \setminus T$: $$\inf_{i \in S} f(i) = \min \left( \inf_{i \in S \cap T} f(i), \inf_{i \in S \setminus T} f(i) \right)$$

Let $f: \iota \to \alpha$ be a function whose range is bounded below in a conditionally complete linear order $\alpha$. For any $a \in \alpha$, $a < \inf_{i \in \iota} f(i)$ if and only if there exists some $b \in \alpha$ such that $a < b$ and $b \le f(i)$ for all $i \in \iota$.

Let $f, g: \iota \to \alpha$ be two functions into a conditionally complete lattice $\alpha$. If the ranges of $f$ and $g$ are both bounded above, then the supremum of their pointwise supremum is equal to the supremum of the individual suprema. That is, $$\sup_{x} (f(x) \vee g(x)) = \left(\sup_{x} f(x)\right) \vee \left(\sup_{x} g(x)\right)$$ where $\vee$ denotes the join (supremum) operation in the lattice.

Let $f, g: \iota \to \alpha$ be two functions into a conditionally complete lattice $\alpha$. If the ranges of $f$ and $g$ are both bounded below, then the infimum of their pointwise minimum is equal to the minimum of their individual infima: $$\inf_{x} (f(x) \sqcap g(x)) = (\inf_{x} f(x)) \sqcap (\inf_{x} g(x))$$ where $\sqcap$ denotes the meet (infimum) operation and $\inf$ denotes the conditionally complete infimum.

Let $f: \iota \to \alpha$ be a function into a conditionally complete lattice $\alpha$ and let $a \in \alpha$ be an element. If the range of $f$ is bounded above, then the join of $a$ and the supremum of $f(x)$ is equal to the supremum of the pointwise join of $a$ and $f(x)$: $$a \vee \sup_{x \in \iota} f(x) = \sup_{x \in \iota} (a \vee f(x))$$ where $\vee$ (or $\sqcup$) denotes the join operation and $\sup$ (or $\bigsqcup$) denotes the conditionally complete supremum.

Let $f: \iota \to L$ be a function into a conditionally complete lattice $L$, and let $a \in L$ be an element. If the range of $f$ is bounded below, then the infimum of $a \sqcap f(x)$ over all $x$ is equal to the meet of $a$ and the infimum of $f(x)$ over all $x$: $$a \sqcap \inf_{x \in \iota} f(x) = \inf_{x \in \iota} (a \sqcap f(x))$$

Let $f, g: \iota \to L$ be functions into a conditionally complete lattice $L$. If the ranges of $f$ and $g$ are both bounded below, then the join (supremum) of their individual infima is less than or equal to the infimum of their pointwise join: $$\left( \inf_{i \in \iota} f(i) \right) \sqcup \left( \inf_{i \in \iota} g(i) \right) \leq \inf_{i \in \iota} (f(i) \sqcup g(i))$$ where $\sqcup$ denotes the join (supremum) operation and $\inf$ (or $\sqcap$) denotes the infimum (infimum) operation in the lattice.

Let $f, g: \iota \to \beta$ be functions where $\beta$ is a conditionally complete lattice. If the ranges of $f$ and $g$ are both bounded above, then the supremum of their pointwise infimum is less than or equal to the infimum of their individual suprema: $$\sup_{i \in \iota} (f(i) \sqcap g(i)) \le \left(\sup_{i \in \iota} f(i)\right) \sqcap \left(\sup_{i \in \iota} g(i)\right)$$ where $\sqcap$ denotes the infimum (meet) operation in the lattice.

Let $E$ be an additive commutative monoid and $\mathbf{k}$ be a semiring equipped with a partial order, such that $E$ is a $\mathbf{k}$-module (via a scalar multiplication $\cdot$). Let $s$ and $t$ be subsets of $E$, and $\beta$ be a type with a less-than-or-equal-to relation $\leq$. If $f: E \to \beta$ is a quasiconvex function on $s$ with respect to $\mathbf{k}$, $t$ is a subset of $s$ ($t \subseteq s$), and $t$ is a convex set, then $f$ is also quasiconvex on $t$.

Let $\mathbf{k}$ be a semiring with a partial order, $E$ be an additive commutative monoid with a scalar multiplication by $\mathbf{k}$, and $\beta$ be a semilattice-sup (a partially ordered set where any two elements $a, b$ have a least upper bound $a \sqcup b$). Let $s$ be a set in $E$ and $f: E \to \beta$ be a quasiconvex function on $s$. For any $x, y \in s$ and any $z$ belonging to the segment connecting $x$ and $y$, the value of the function at $z$ is less than or equal to the maximum (supremum) of the values at the endpoints, i.e., $f(z) \leq f(x) \sqcup f(y)$.

Let $E$ be an additive commutative monoid equipped with a scalar multiplication by a semiring $\mathbb{k}$, where $\mathbb{k}$ has a partial order. Let $s \subseteq E$ be a set and $f: E \to \beta$ be a function into a semilattice-inf $\beta$. If $f$ is quasiconcave on $s$, then for any points $x, y \in s$ and any point $z$ lying in the segment $[x, y]$, it holds that $f(x) \land f(y) \le f(z)$, where $\land$ denotes the infimum (meet) in $\beta$.

Let $S$ be a subset of a topological space $\alpha$, and let $g: \alpha \to \mathbb{R}$ be a real-valued function. If $g$ is lower semicontinuous on $S$ and $S$ is compact, then the image of $S$ under $g$, denoted by $g(S)$, is bounded below.

Let $X$ be a topological space and $S \subseteq X$ be a set. Let $f, g: X \to \mathbb{R}$ be real-valued functions. If $f$ and $g$ are both lower semicontinuous on $S$, then their pointwise maximum $x \mapsto \max(f(x), g(x))$ is also lower semicontinuous on $S$.

Let $f: \alpha \to \gamma$ be a function from a topological space $\alpha$ to a linearly ordered topological space $\gamma$, and let $s$ be a closed subset of $\alpha$. The function $f$ is lower semicontinuous on $s$ if and only if for every $y \in \gamma$, the set $s \cap \{x \mid f(x) \le y\}$ is closed.

Let $E$ be a topological vector space over the real numbers $\mathbb{R}$ (specifically, a type with an additive commutative group structure, a module structure over $\mathbb{R}$, and a topology such that addition and scalar multiplication are continuous). For any two points $a, b \in E$, the line segment connecting them, defined as $\text{segment } \mathbb{R} \ a \ b = \{ (1-t)a + tb \mid 0 \le t \le 1 \}$, is a connected set.

Let $M$ and $N$ be sets, and let $\alpha$ be a conditionally complete linear order. Let $f: M \times N \to \alpha$ be a function. Suppose $S \subseteq M$ and $T \subseteq N$ are subsets such that the set of values $f(S, T) = \{f(x, y) \mid x \in S, y \in T\}$ is bounded above and bounded below. Then the set of values $\{\inf_{x \in S} f(x, y) \mid y \in T\}$ is bounded above.

Let $M$ and $N$ be sets, and let $\alpha$ be a conditionally complete linear order. Let $f: M \times N \to \alpha$ be a function. Suppose $S \subseteq M$ and $T \subseteq N$ are subsets such that the set of values $f(S, T) = \{f(x, y) \mid x \in S, y \in T\}$ is bounded above and bounded below. Then the set of values $\{\sup_{x \in S} f(x, y) \mid y \in T\}$ is bounded below.

Let $\alpha$ be a conditionally complete lattice and $f: \beta \to \alpha$ be a function. For any subsets $s, t \subseteq \beta$ such that $s$ is non-empty, $s \subseteq t$, and the image $f(t)$ is bounded below, the infimum of $f$ over $t$ is less than or equal to the infimum of $f$ over $s$: $$\inf_{x \in t} f(x) \le \inf_{x \in s} f(x)$$

Let $X$ be a topological space and $Y$ be a preordered space with a top element $\top$. Let $S \subseteq X$ be a subset and $p$ be a decidable predicate on $X$. Suppose $f$ is a function that, for each $x$ satisfying $p(x)$, assigns a value in $Y$. Let $h$ be the function defined on $S$ such that $h(x) = f(x)$ if $p(x)$ is true, and $h(x) = \top$ otherwise. If the restriction of $f$ to the subtype $\{x \mid p(x)\}$ is lower semicontinuous on the set $\{x \in \text{subtype} \mid \text{val}(x) \in S\}$, and there exists a closed set $U \subseteq X$ such that $S \cap U = \{x \in S \mid p(x)\}$, then $h$ is lower semicontinuous on $S$.

Let $X$ and $Y$ be topological spaces and $Z$ be a preordered set. Let $f : X \to Y$ be a function and $g : Y \to Z$ be another function. Let $S \subseteq X$ and $T \subseteq Y$ such that the image of $S$ under $f$ is contained in $T$ ($f(S) \subseteq T$). If $g$ is lower semicontinuous on $T$ and $f$ is continuous on $S$, then the composition $g \circ f$ is lower semicontinuous on $S$.

Let $X$ and $Y$ be topological spaces and $Z$ be a preordered set. Let $f: X \to Y$ be a function and $g: Y \to Z$ be another function. Suppose $s \subseteq X$ and $t \subseteq Y$ are sets such that $f(s) \subseteq t$. If $g$ is upper semicontinuous on $t$ and $f$ is continuous on $s$, then the composition $g \circ f$ is upper semicontinuous on $s$.

Let $X$ be a topological space and $Y$ be a preordered space with a greatest element $\top$. Let $S \subseteq X$ be a set and $P$ be a predicate on $X$. Let $f: X \to Y$ be a function. Suppose that: 1. $f$ is lower semicontinuous on the set $S \cap \{x \mid P(x)\}$. 2. The set $S \cap \{x \mid P(x)\}$ is relatively closed in $S$, i.e., there exists a closed set $U \subseteq X$ such that $S \cap U = S \cap \{x \mid P(x)\}$. Then the function $g: X \to Y$ defined by $$g(x) = \begin{cases} f(x) & \text{if } P(x) \\ \top & \text{otherwise} \end{cases}$$ is lower semicontinuous on $S$.

Let $X$, $Y$, and $Z$ be topological spaces where $Y$ and $Z$ are equipped with a linear order, the order topology, and are densely ordered. Let $s \subseteq X$ be a set, $f: X \to Y$ be a function that is lower semicontinuous on $s$, and $g: Y \to Z$ be a monotone function that is left order continuous. Then the composite function $g \circ f$ is lower semicontinuous on $s$.

Let $X$ and $Y$ be topological spaces and $Z$ be a preordered set. Let $f : X \to Z$ be a function that is upper semicontinuous on a subset $T \subseteq X$. Let $z \in T$ and $c \in Z$ be such that $f(z) < c$. Suppose $\{z_s\}_{s \in S}$ is a net (or more generally, a filter $l$ is given) such that $z_s \to z$, and for all $s$, $z_s \in T$. Then, eventually along the filter $l$, it holds that $f(z_s) < c$.

Let $\alpha$ be a type with decidable equality and let $\beta$ be a conditionally complete lattice. For any non-empty finite set $t \subseteq \alpha$, any element $x \in \alpha$, and any function $f : \alpha \to \beta$, the infimum of $f$ over the set $t \cup \{x\}$ is equal to the infimum (greatest lower bound) of $f(x)$ and the infimum of $f$ over $t$. That is: $$\inf_{a \in \{x\} \cup t} f(a) = f(x) \sqcap \inf_{a \in t} f(a)$$ where $\sqcap$ denotes the meet (infimum) operator in the lattice.

Let $\alpha$ be a type with decidable equality and $\beta$ be a conditionally complete lattice. For any non-empty finite set $t \subseteq \alpha$, any element $x \in \alpha$, and any function $f: \alpha \to \beta$, the supremum of $f$ over the set $t \cup \{x\}$ is equal to the join (least upper bound) of $f(x)$ and the supremum of $f$ over $t$. That is, $$\sup_{a \in t \cup \{x\}} f(a) = f(x) \sqcup \sup_{a \in t} f(a)$$

Let $f: M \times N \to \mathbb{R}$ be a function, and let $S \subseteq M$ and $T \subseteq N$ be sets such that the image $f(S, T)$ is both bounded above and bounded below. Under the conditions of Sion's Minimax Theorem (typically that $S$ and $T$ are compact convex sets and $f$ satisfies appropriate semi-continuity and quasi-concavity/convexity conditions), the following equality holds: $$\inf_{x \in S} \sup_{y \in T} f(x, y) = \sup_{y \in T} \inf_{x \in S} f(x, y)$$ where the boundedness assumptions ensure that the conditional suprema and infima are well-defined and do not take "junk values."