Chapter 3, Theorem 6(a) -- Q is Lipschitzian, convex and finite on K2

This declaration asserts, for every choice of natural numbers $n_1, n_2, m_1, m_2, K$ (including $0$) and every object $\mathrm{inst}$ of type $\mathrm{Instance}\; n_1\, n_2\, m_1\, m_2\, K$, the following.

Objects from the imported bundle (not unfolded here). The types $\mathrm{Instance}$, and the functions $\mathrm{QVal}$, $Q$ and $K_2$, are supplied by the imported file Definitions.Def_StochasticProg_Recourse_Instance, whose code is not part of this declaration; the read-back can only report what the statement itself forces about them. Their roles, as used in the code, are:

• $Q(\mathrm{inst}, \cdot)$ is a function on some type of points $x$ (the type is left implicit by the code and is fixed by the definition of $Q$; it is not visibly $\mathbb{R}^{n_1}$ or anything else), with values in the extended reals $\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}$.
• $\mathrm{QVal}(\mathrm{inst}, x, k)$ is a function of a point $x$ and a second argument $k$ (whose type is likewise implicit), taking values in a type that has a bottom element $\bot$; nothing in this declaration says what $\mathrm{QVal}$ computes or how it relates to $Q$.
• $K_2(\mathrm{inst})$ is a set of points $x$ of the same type as the argument of $Q$. Nothing in this declaration says that it is convex, nonempty, closed, or a polyhedron.

Hypothesis. The single hypothesis $hQ$ is: for every point $x$ of the ambient type (not merely $x \in K_2(\mathrm{inst})$) and every $k$,

If for the given instance some $x$ and $k$ make $\mathrm{QVal}$ equal to $\bot$, this hypothesis is false and the theorem holds vacuously for that instance. The hypothesis says nothing about the top element (if the value type has one).

Conclusion. Write $\tilde Q(x)$ for the real number obtained from $Q(\mathrm{inst}, x)$ by the “to-real” map, which sends a finite extended real to itself and sends both $+\infty$ and $-\infty$ to $0$. The conclusion is the conjunction of three statements:

1. Finiteness on $K_2$. For every $x \in K_2(\mathrm{inst})$ there exists a real number $r$ with

as extended reals; equivalently, $Q(\mathrm{inst}, x) \notin \{-\infty, +\infty\}$ for every $x \in K_2(\mathrm{inst})$. No claim is made about $Q$ outside $K_2(\mathrm{inst})$.

2. Convexity on $K_2$. The function $x \mapsto \tilde Q(x)$ is convex on the set $K_2(\mathrm{inst})$ over the scalar field $\mathbb{R}$. In the sense used here this means two things together: the set $K_2(\mathrm{inst})$ is itself convex (for all $x, y \in K_2(\mathrm{inst})$ and all $a, b \ge 0$ with $a + b = 1$, $a x + b y \in K_2(\mathrm{inst})$), and for all such $x, y, a, b$,

(Convexity of $K_2(\mathrm{inst})$ is therefore part of what is asserted, since it is not assumed.) The inequality is stated for the real-valued $\tilde Q$, so if $Q$ took an infinite value on $K_2$ the value $0$ would be used — although part 1 rules that out on $K_2$.

3. Lipschitz continuity on $K_2$. There exists a nonnegative real constant $L \ge 0$ such that for all $x, y \in K_2(\mathrm{inst})$,

i.e. $|\tilde Q(x) - \tilde Q(y)| \le L\, d(x,y)$, where $d(x,y)$ is the distance on the ambient type of $x$ that its (implicit) metric structure provides; which metric this is (e.g. Euclidean, sup-norm) is determined by the imported definitions, not by this declaration. The constant $L$ may be $0$, and no bound on $L$ in terms of the instance data is claimed.

Degenerate cases made explicit. If $K_2(\mathrm{inst})$ is empty, all three parts of the conclusion hold trivially (the empty set is convex and every statement quantified over its elements is vacuous). If $K_2(\mathrm{inst})$ is a single point, parts 2 and 3 hold trivially with $L = 0$. Nothing in the statement asserts that $K_2(\mathrm{inst})$ is nonempty, that the scenario set is finite, that the recourse is fixed, or that $Q$ is an expectation or a minimum of anything; all such content, if present, lives entirely inside the imported definitions of $\mathrm{Instance}$, $\mathrm{QVal}$, $Q$ and $K_2$, which this read-back cannot verify.