Hyperplane separation of a concave functional and a point, in domain theory

Question

Problem:

Let $D$ be an $\omega$-BC domain, and $[D\to[0,\infty]]$ be the space of Scott-continuous nonnegative functions on $D$, equipped with the obvious ordering and the Scott-topology.

EDIT: I don't think the specific properties of $D$ are needed, I think the important part is just that the function space is a continuous complete second-countable lattice, and you can add points in it (adding functions) and multiply points in it by nonnegative scalars (scaling functions), so it makes a cone. Hopefully this should make the problem a bit more approachable to those without much domain-theory knowledge.

Let $\psi$ be of type $[D\to[0,\infty]]\to[0,\infty]$, fulfilling the following four properties.

1: Scott-continuous. Ie, $\psi$ is monotone and preserves suprema of directed sets.

2: Concave. $\psi(pf+(1-p)g)\ge p\psi(f)+(1-p)\psi(g)$ for $p\in[0,1]$

3: Lipschitz. $\frac{|\psi(f)-\psi(g)|}{d_{sup}(f,g)}\le c$ for some fixed constant $c<\infty$. $d_{sup}(f,g)$ is the sup-norm distance, ie, $\sup_{d\in D}|f(d)-g(d)|$.

4: Homogenous. $\psi(\lambda f)=\lambda\psi(f)$ for all finite $\lambda\ge 0$. In particular, note that the constant-0 function maps to 0.

The task is as follows: Given some $\psi$ fulfilling those four properties, some function $f:[D\to[0,\infty]]$, and some number $x$ where $x>\psi(f)$, find a lipschitz, scott-continuous, linear functional $\mu:[D\to[0,\infty]]\to[0,\infty]$ s.t. $\mu\ge\psi$, and $x\ge\mu(f)$.

Motivation:

In simpler cases, this would be an easy application of the Hahn-Banach theorem, which lets you cook up a linear functional to separate the region on and below the graph of your concave function $\psi$, from the point $(\psi,x)$ that lies above the graph. This is inspired by the classical result about how a concave function can be characterized via its tangent hyperplanes, but I'm trying to generalize it to domain theory and valuations.

The most applicable-looking result I've found is Hahn-Banach Type Theorems for Locally Convex Cones. Theorem 3.1 looks very much like what I need. The problem I was running into is that I don't actually know whether or not $[D\to[0,\infty]]$ equipped with the Scott-topology is a locally convex cone, which neighborhood $v$ to use, which quasiuniformity $\mathcal{V}$ would work, or how to go from their particular definition of uniform continuity on a neighborhood to showing Scott-continuity of $\mu$. But something like that feels like the right way to go, it's the only sufficiently generalized separation theorem I've seen.

Answer 1

Welp, I proved it.

PROOF SKETCH

So, here's the rough idea of the proof path. Given the linked paper "Hahn-Banach Type Theorems for Locally Convex Cones", what we use is not Theorem 3.1, but the very first theorem. Theorem 2.1, the first sandwich theorem.

The reason I was pessimistic about taking this approach is that, when you invoke 2.1, it just gives you a separating linear functional. With some work you can adapt the proof to make said functional Lipschitz-continuous, but the proof says nothing at all about Scott-continuity, which is the one missing piece. There are intuitions that a general linear function would be quite badly-behaved, so it seems hopeless to fix this issue.

But, as we'll see, it's possible in this setting to take a separating linear functional and "continu-ify" it, turning it continuous. There's an extensive amount of domain theory work that goes into showing that, yes, the separating functional stays linear when you continu-ify, which is the main hard part, besides realizing that continu-ification might actually be doable in the first place.

Once that's out of the way, showing that the linear functional remains separating when you continu-ify it isn't particularly difficult.

It feels like there's a considerable generalization of this theorem left to find, but it suffices for my purposes.

BEGIN PROOF

For notation, $\psi$ will be our concave functional of interest, $f^*$ will be our function of interest, and $x$ will be our number of interest, specified at the start. $f,g$ are used to notate generic functions of type $[D\to[0,\infty]]$, and $c$ is used to denote constants or constant functions (we're abusing some notation here). $d$ is used for elements of the domain $D$.

So, $\psi, f^*, x$ are specified at the start, having the indicated properties. Let $L$ denote the (finite) Lipschitz constant of $\psi$.

DEFINING $\phi$

We'll cook up a special sublinear functional $\phi$ to start invoking the Hahn-Banach variant in the paper. It takes some fanciness to establish this, because we'll be adapting the proof to make the separating functional Lipschitz.

We can split into several possible cases. The one thing all the cases have in common is that, unless otherwise defined, $\phi(f):=\infty$, so we'll just define these functionals where they're being interesting (ie, not infinity). $c$ is an arbitrary nonnegative constant/constant function that isn't infinity, though it can be zero. The conventions for multiplying a function by zero is that any function times zero is the constant-zero function.

Case 1: $x=\infty$ or $f^*$ is the constant-0 function. In such a case, $\phi(c):=c\cdot L$

Case 2: $x\neq\infty$, and $f^*$ is the constant-infinity function. $\phi(f):=0$ for all $f$.

Case 3: $x\neq\infty$, and $f^*$ is 0 on some nonempty subset of $D$ (call it $A$), and $\infty$ otherwise (no other behaviors). Then, $\phi(c):=c\cdot L$ and $\phi(\infty, c\text{ otherwise}):=c\cdot L$

Case 4: $x\neq\infty$, and $f^*$ is some nonzero constant $c^*$ on some nonempty subset of $D$ (call it $A$), and $\infty$ otherwise (no other behaviors). Then, $\phi(c):=c\cdot L$ and $\phi(\infty,c\cdot c^*\text{ otherwise}):=c\cdot \min(x,c^*\cdot L)$

Case 5: $x\neq\infty$, and $f^*$ is not a constant on the subset of $D$ where it doesn't equal $\infty$. In such a case, it's possible to take any function that's a linear mix of $f^*$ and the constant-1 function, and uniquely figure out the coefficients used to mix the two functions together, so we have $\phi(af^*+c):=a\cdot x + c\cdot L$

Case 6: $x\neq\infty$, and $f^*$ is some nonzero constant function $c^*$.Then, $\phi(c\cdot c^*):=c\cdot\min(x,c^*\cdot L)$

SEPARATION THEOREM SETUP:

To start invoking the theorem from the listed paper, we need to verify that $\psi$ is superadditive and homogenous, and that $\phi$ is subadditive and homogenous, and that $f\ge g\to\phi(f)\ge\psi(g)$. Let's clean up $\psi$ first. Homogenity was assumed at the start for $\psi$, so that leaves superadditivity.

Proof: $$\psi(f+g)=\psi(0.5\cdot 2f+0.5\cdot 2g)\ge 0.5\cdot\psi(2f)+0.5\cdot\psi(2g)=\psi(f)+\psi(g)$$ The first inequality was concavity, the second equality was homogenity.

Establishing homogenity for our $\phi$ abomination is pretty easy, just play around with it a bit. Basically, all cases assign the constant-0 function has 0 value, the specified functions (closed under nonzero scalar multiplication) to values that vary linearly as you do scalar multiplication, and the-nonspecified functions (closed under nonzero scalar multiplication) to infinity, and nonzero number times infinity is infinity.

Next up, we need to establish that $\phi$ is subadditive, that $\phi(f+g)\le\phi(f)+\phi(g)$. This is a routine but hideously long and boring proof by cases that will be skipped.

PROVING $\phi\ge\psi$

Also, there's establishing that when $f\ge g$, $\phi(f)\ge\psi(g)$. We can reduce this to just establishing that $\phi\ge\psi$, because by monotonicity of $\psi$ we can go $\phi(f)\ge\psi(f)\ge\psi(g)$. Also, we only need to check the functions that $\phi$ had to especially pinpoint the value of, because all other values are infinity which trivially wins. Time to go through the cases.

In case 1, we have $\phi(c)=c\cdot L\ge\psi(c)-\psi(0)=\psi(c)$, by L being the Lipschitz constant of $\psi$, and the constant-c function and constant-0 function only being $c$ apart from each other.

In case 2, we'll show that $\psi(\infty)=0$, which then, by monotonicity, extends to show $\psi(f)=0=\phi(f)$ for all $f$. Here's why this must occur. By scott-continuity and homogenity, $\psi(\infty)=\psi(\bigsqcup^{\uparrow}_{n:\mathbb{N}}c_n)=\bigsqcup^{\uparrow}_{n:\mathbb{N}}\psi(c_n)=\bigsqcup^{\uparrow}_{n:\mathbb{N}}(n\cdot\psi(1))$ Now, by this point, either $\psi(1)$ is zero or nonzero. If it's finite, then that means that $\psi(\infty)=\infty$, but we assumed that $x>\psi(f^*)$ in this case. Since our function is constant-infinity, we get a contradiction. So, $\psi(1)=0$, and we get $\bigsqcup^{\uparrow}_{n:\mathbb{N}}(n\cdot\psi(1))=\bigsqcup^{\uparrow}_{n:\mathbb{N}}0=0$. Done.

For case 3, we've got $\phi(\infty, c \text{ otherwise})=c\cdot L\ge\psi(\infty,c \text{ otherwise})-\psi(\infty, 0\text{ otherwise})=\psi(\infty, c\text{ otherwise})$ by Lipschitzness of $\psi$ for the inequality. That last inequality is because $\psi(\infty, 0\text{ otherwise})$ must be 0 by the same sort of argument as the second case.

For case 4, we have $\phi(\infty, c\cdot c^*\text{ otherwise})=c\cdot\min(x,c^*\cdot L)$. Both of these possible values will be shown to beat $\psi$. $c\cdot x > c\cdot\psi(\infty, c^*\text{ otherwise})=\psi(\infty,c\cdot c^*\text{ otherwise})$ because we assumed at the start that $x>\psi(f^*)$ and in this case $f^*$ is infinity on some set and $c^*$ on another set. For the other possible value, we have $c\cdot c^*\cdot L\ge\psi(\infty, c\cdot c^*\text{ otherwise})-\psi(\infty, 0\text{ otherwise})=\psi(\infty, c\cdot c^*\text{ otherwise})$ by Lipschitz-continuity of $\psi$, and the case 2 argument that $\psi(\infty, 0\text{ otherwise})=0$.

For case 5, we have $\phi(a f^*+c)=a\cdot x+c\cdot L\ge a\cdot\psi(f^*)+c\cdot L=\psi(af^*)+c\cdot L\ge\psi(af^*+c)$ via $x>\psi(f^*)$ assumed at the start, and homogenity of $\psi$ and Lipschitzness of $\psi$.

For case 6, we have $\phi(c\cdot c^*)=c\cdot\min(x,c^*\cdot L)$ Time to prove both of these beat $\psi(c\cdot c^*)$. For one, we have $c\cdot x>c\cdot\psi(c^*)=\psi(c\cdot c^*)$ via $x>\psi(f^*)$ at the start and homogenity, and for the other, we have $c\cdot c^*\cdot L\ge\psi(c\cdot c^*)$ by Lipschitzness.

And bam, we're done.

Oh wait, one more thing we need, arguing that $\phi(f^*)\le x$. This is pretty easy to do, just look at the definitions of $\phi$, I won't cover it here.

INVOCATION OF PROOF:

Alright, NOW we can finally work on this dang thing. We know that $\phi$ is homogenous and subadditive, and that $\psi$ is homogenous and superadditive, and that $\phi\ge\psi$, and so applying the very first theorem from the linked paper, we get a monotone linear functional $\mu$ s.t. $\psi\le\mu\le\phi$.

We also know that $\mu(f^*)\le\phi(f^*)\le x$ because $\mu\le\phi$ and we checked that $\phi(f^*)\le x$.

Even further, we know that $\mu$ is Lipschitz. Why? Well, $\phi(1)$, in all cases, is either 0, $L$ (finite), or $\frac{x}{c^*}$ for non-infinite $x$ and nonzero $c^*$ (see case 6), and thus finite. So, by linearity of $\mu$, we can pick some functions $f$ and $g$ that are only $\epsilon$ apart, and go $\mu(g)\le\mu(f+\epsilon)=\mu(f)+\mu(\epsilon)=\mu(f)+\epsilon\mu(1)$ And symmetrically, we can get the above line but with $g$ and $f$ interchanged, and so we get $|\mu(f)-\mu(g)|\le\epsilon\mu(1)$. $\epsilon$ could be anything, so we've got a Lipschitz constant of $\mu(1)$, which we know is finite.

Ok, so that gets us Lipschitzness, linearity, and monotonicity and looking like a good separating functional, but what about Scott-continuity? Well, to do that, we'll need to continu-ize $\mu$ as follows.

$\mu'(f):=\bigsqcup^{\uparrow}_{f'\ll f}\mu(f')$

So, basically, there can't be rips or tears in $\mu'$. If $\mu$ says that $f$ suddenly jumps up in value relative to what you'd expect by looking at approximants, it's brought down to the supremum of the values of its approximants. We have that $\mu'\le\mu$.

SHOWING THAT $\mu'$ WORKS OK

Our to-do list now is:

1: Show that $\psi\le\mu'$ still holds. Ie, it's still a separating functional since we have $\psi\le\mu'$, and $\mu'(f^*)\le\mu(f^*)\le\phi(f^*)\le x$.

2: Show that Lipschitznes applies to $\mu'$

3: Show that Scott-continuity applies to $\mu'$.

4: Show that linearity applies to $\mu'$

And bam, we will have made a Scott-continuous linear Lipschitz separating functional that overshoots $\psi$ and undershoots $x$ at $f^*$.

Part 1, dominating $\psi$. $$\mu'(f)=\bigsqcup^{\uparrow}_{f'\ll f}\mu(f')\ge\bigsqcup^{\uparrow}_{f'\ll f}\psi(f')=\psi(f)$$ The first equality was by definition, second was $\mu\ge\psi$, third was Scott-continuity of $\psi$.

Part 2, Lipschitzness. Our proof of it for $\mu$ only relied on linearity and $\mu(1)$ being finite. We have $\mu'\le\mu$, so this will follow automatically once we manage to prove the last part about linearity.

Part 3, Scott-continuity. We have $$\mu'(f)=\bigsqcup^{\uparrow}_{f'\ll f}\mu(f')=\bigsqcup^{\uparrow}_{f'\ll f}\bigsqcup^{\uparrow}_{f''\ll f'}\mu(f'')=\bigsqcup^{\uparrow}_{f'\ll f}\mu'(f')$$ First equality was unpacking definitions, the second equality was nontrivial, the trick with that is the interpolation property of approximation in Scott-domains (which $[D\to[0,\infty]]$ certainly is, it's an L-domain, actually), which basically says that if $f''\ll f$, then you can find some $f'$ s.t. $f''\ll f'\ll f$. Combined with monotonicity of $\mu$, of course. Then, just pack up definitions.

From here we can show Scott-continuity by letting $A$ be an arbitrary directed subset of the function space, and go $$\mu'(\bigsqcup^{\uparrow}A)=\bigsqcup^{\uparrow}_{f'\ll \bigsqcup^{\uparrow}A}\mu'(f')=\bigsqcup^{\uparrow}_{f\in A}\bigsqcup^{\uparrow}_{f'\ll f}\mu'(f')=\bigsqcup^{\uparrow}_{f\in A}\mu'(f)$$ First equality is from what we showed just before this. The second equality is because every approximant of a directed supremum is also an approximant for some point in the directed set, so any particularly good choice of $f'$ has a $f$ that lets you pick that $f'$. And, vice-versa, every approximant of an element of a directed set is an approximant of the directed supremum. Then just pack up what we showed about how $\mu'$ worked. Bam, Scott-continuity, established.

LINEARITY PROOF:

Part 3, Linearity. Here's how this goes. $\mu'(af+bg)=\bigsqcup^{\uparrow}_{h\ll af+bg}\mu(h)=\bigsqcup^{\uparrow}_{f'\ll f,g'\ll g}\mu(af'+bg')=\bigsqcup^{\uparrow}_{f'\ll f,g'\ll g}(a\mu(f')+b\mu(g'))=\bigsqcup^{\uparrow}_{f'\ll f}a\mu(f')+\bigsqcup^{\uparrow}_{g'\ll g}b\mu(g')=a\bigsqcup^{\uparrow}_{f'\ll f}\mu(f')+b\bigsqcup^{\uparrow}_{g'\ll g}\mu(g')=a\mu'(f)+b\mu'(g)$

First equality is just unpacking definitions, the second equality is... we'll address that later, third is just linearity of $\mu$, fourth is just breaking up the directed supremum a bit, and the rest is just shuffling constants a bit and packing up definitions.

So, linearity hinges on this one equation

$\bigsqcup^{\uparrow}_{h\ll af+bg}\mu(h)=\bigsqcup^{\uparrow}_{f'\ll f,g'\ll g}\mu(af'+bg')$

which is... not obvious at all. Not one bit. One direction of this, that

$\bigsqcup^{\uparrow}_{f'\ll f,g'\ll g}\mu(af'+bg')\ge\bigsqcup^{\uparrow}_{h\ll af+bg}\mu(h)$

can be derived as follows: Roughly, given any $h\ll af+bg$, we need to find some $f',g'$ where $af'+bg'\ge h$, because $\mu$ is monotone. Since we can beat the value of all $h$ in the right-hand-side set, the supremum of the left hand side beats the supremum of the right hand side.

Here's how it's done. The function $\lambda f,g.af+bg$ of type $[D\to[0,\infty]]^{2}\to[D\to[0,\infty]]$ is indeed Scott-continuous, it preserves directed suprema of sets of functions. The set $\{<f',g'>|f'\ll f,g'\ll g\}$ is directed with a suprema of $<f,g>$, so shoving it through our scott-continuous function, you get the directed set $\{af'+bg'|f'\ll f,g'\ll g\}$ with a supremum of $af+bg$. Since $h\ll af+bg$, there is some element of this directed set with a supremum of $af+bg$ which surpasses $h$, some $f',g'$ pair where $af'+bg'\ge h$. Now just apply monotonicity.

The reverse direction is a rather nasty piece of work. I've already proved it in a different context, but it's a fairly long proof, that I won't be reproducing here. It's pretty easy to show that $f'\ll f\to af'\ll af$, but showing the result that $f'\ll f\wedge g'\ll g\to f'+g'\ll f+g$... takes some thought.

Proof sketch time! If anyone wants to attempt it on their own, the basic idea is to use that $D$ is an $\omega$-BC domain, and how the order of approximation works in function spaces, to swap out $f'$ and $g'$ with higher $f''$ and $g''$ (that still approximate $f$ and $g$) which are finite suprema of atomic step functions (functions which map a base open set of the form $d^{\upuparrows}$ to a particular finite value and all else to 0). Then, adding together the two finite suprema of atomic step functions turns out to be a finite suprema of atomic step functions. Then you just need to show that $f+g$ is approximated by each component atomic step function (this is trickier than other steps), to show that it's approximated by your finite suprema of atomic step functions (since order of approximation is preserved under suprema), and your finite suprema beats $f'+g'$, and bam, you've shown that function addition preserves the order of approximation.

And we're done! We made a suitable $\mu'$ that has all the nice properties we want!