Lemma 7: For $f, f^{'}, f^{''}, f^{'''} \in [X \to (- \infty, \infty]$ s.t. $f^{''} ≪ f$ and $f^{'''} ≪ f^{'}$ , and $p \in (0, 1)$ , and $X$ is compact, LHC, and second-countable, then $p f^{''} + (1 - p) f^{'''} ≪ p f + (1 - p) f^{'}$ . The same result holds for $[X \to [0, 1]]$ .

This is the only spot where we need that $X$ is LHC and not merely locally compact.

Here's how it's going to work. We're going to use the details of the proof of Theorem 2 to craft two special functions $g$ and $g^{'}$ of a certain form, which exceed $f^{''}$ and $f^{'''}$ . Then, of course, $p f^{''} + (1 - p) f^{'''} ⊑ p g + (1 - p) g^{'}$ as a result. We'll then show that $p g + (1 - p) g^{'}$ can be written as the supremum of finitely many functions in $[X \to [- \infty, \infty]]$ (or $[X \to [0, 1]]$ ) which all approximate $p f + (1 - p) f^{'}$ , so $p f + (1 - p) f^{'} ≫ p g + (1 - p) g^{'} ⊒ p f^{''} + (1 - p) f^{'''}$ , establishing that $p f + (1 - p) f^{'} ≫ p f^{''} + (1 - p) f^{'''}$ .

From our process of constructing a basis for the function space back in Theorem 2, we have a fairly explicit method of crafting a directed set of approximating functions for $f$ and $f^{'}$ . The only approximator functions you need to build any $f$ are step functions of the form $(U ↘ q)$ with $q$ being a finite rational number, and $U$ being selected from the base of $X$ , and $q < {inf}_{x \in K (U)} f (x)$ where $K$ is our compact hull operator. Any function of this form approximates $f$ , and taking arbitrary suprema of them, $f$ itself is produced.

Since functions of this form (and suprema of finite collections of them) make a directed set with a supremum of $f$ or above ( $f^{'}$ or above, respectively), we can isolate a $g$ from the directed set of basis approximators for $f$ , s.t. $g ⊒ f^{''}$ , because $f^{''} ≪ f$ . And similarly, we can isolate a $g^{'}$ which approximates $f^{'}$ s.t. $g^{'} ⊒ f^{'''}$ , because $f^{'''} ≪ f^{'}$ .

Now, it's worthwhile to look at the exact form of $g$ and $g^{'}$ . Working just with $g$ (all the same stuff works for $g^{'}$ ), it's a finite supremum of atomic step functions, so

$g (x) = {sup}_{i} (U_{i} ↘ q_{i}) (x) = {sup}_{i : x \in U_{i}} q_{i}$

and, by how our atomic step functions of the directed set associated with $f$ were built, we know that for all i, $q_{i} < {inf}_{x \in K (U_{i})} f (x)$ . (remember, the $U_{i}$ are selected from the base, so we can take the compact hull of them).

There's a critical ...

Domain Theory