Lemma 7:For f,f′,f′′,f′′′∈[X→(−∞,∞] s.t. f′′≪f and f′′′≪f′, and p∈(0,1), and X is compact, LHC, and second-countable, then pf′′+(1−p)f′′′≪pf+(1−p)f′. The same result holds for [X→[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, pf′′+(1−p)f′′′⊑pg+(1−p)g′ as a result. We'll then show that pg+(1−p)g′ can be written as the supremum of finitely many functions in [X→[−∞,∞]] (or [X→[0,1]]) which all approximate pf+(1−p)f′, so pf+(1−p)f′≫pg+(1−p)g′⊒pf′′+(1−p)f′′′, establishing that pf+(1−p)f′≫pf′′+(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<infx∈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)=supi(Ui↘qi)(x)=supi:x∈Uiqi

and, by how our atomic step functions of the directed set associated with f were built, we know that for all i, qi<infx∈K(Ui)f(x). (remember, the Ui are selected from the base, so we can take the compact hull of them).

There's a critical split here between the behavior of the [X→[−∞,∞]] type signature, and the [X→[0,1]] type signature.

For the [X→[−∞,∞]] type signature, there's finitely many i, and everything not in the Ui gets mapped to −∞. Since f′′∈[X→(−∞,∞]], and X is compact, f′′ is bounded below (Lemma 1), so for this finite supremum to exceed f′′, the Ui must cover X.

For the [X→[0,1]] type signature, again there's finitely many i, but we can't guarantee that the Ui cover X, because everything not in some Ui gets mapped to 0, and f′′ might not be bounded above 0. So, we'll add in a "dummy" step function (X↘0). This is just the constant-0 function, which approximates everything, so nothing changes. However, it ensures that X is indeed covered by the open sets of the finite collection of step functions.

So... Given that we have our g,g′, what does the function pg+(1−p)g′ look like? Well, it looks like

We could do this in the [0,1] case from adding in the "dummy" open sets to get the Ui family and Uj family to both cover X.

Anyways, pg+(1−p)g′ equals ⨆i,j(Ui∩Uj↘pqi+(1−p)qj). There's finitely many i's and finitely many j's by how g and g' were built, so this is a supremum of finitely many atomic step functions. Since pg+(1−p)g′⊒pf′′+(1−p)f′′′, if we can just show that all these atomic step functions are approximators for pf+(1−p)f′ in [X→[−∞,∞]] (or [X→[0,1]]), then pg+(1−p)g′≪pf+(1−p)f′ (supremum of finitely many approximators is an approximator), and we'd show our desired result that pf′′+(1−p)f′′′≪pf+(1−p)f′. So let's get started on showing that, regardless of i and j,

(Ui∩Uj↘pqi+(1−p)qj)≪pf+(1−p)f′

Now, if Ui∩Uj=∅, then this function maps everything to −∞ or 0, which trivially approximates pf+(1−p)f′. Otherwise, everything in Ui∩Uj gets mapped to pqi+(1−p)qj, and everything not in it gets mapped to −∞ (or 0)

We know by our process of construction for this that qi<infx∈K(Ui)f(x) and qj<infx∈K(Uj)f′(x), so let's try to work with that. Well, for the [X→[−∞,∞]] case. The [X→[0,1]] case is a bit more delicate since we added those two dummy functions. We have:

The first strict inequality was because of what qi and qj were. Then, just move the constants in. For the first non-strict inquality, it's because of monotonicity for our compact hull operator, Ui∩Uj⊆Ui, so it has a smaller compact hull. Then the next inequality is just grouping the two infs, and we're finished.

At this point, the usual argument of "fix a directed set of functions ascending up to pf+(1−p)f′, for each patch of K(Ui∩Uj) you can find a function from your directed set that beats the value pqi+(1−p)qj on that spot, this gets you an open cover of K(Ui∩Uj), it's compact, isolate a finite subcover ie finitely many functions, take an upper bound in your directed set, bam, it beats the step function on a compact superset of its open set so it beats the step function, and the directed set was arbitrary so pf+(1−p)f′ is approximated by the atomic step function" from Theorem 2 kicks in, to show that the atomic step function approximates pf+(1−p)f′. Since this works for arbitrary i,j, and there are finitely many of these, the finite supremum pg+(1−p)g′ approximates pf+(1−p)f′, and dominates pf′′+(1−p)f′′′, and we're done.

Now for the [X→[0,1]] case. This case works perfectly fine if our i,j pair has qi and pi being above 0. But what if our Ui has qi being above 0, but our j index is picking that (X↘0) "dummy" approximator? Or vice-versa. Or maybe they're both the "dummy" approximator.

That last case can be disposed of, because (X∩X↘p⋅0+(1−p)⋅0) is just the constant-0 function, which trivially approximates everything. That leaves the case where just one of the step functions isn't the constant-0 function. Without loss of generality, assume Ui is paired with qi>0, but the other one is the (X↘0) "dummy" approximator. Then our goal is to show that (Ui∩X↘pqi+(1−p)0)≪pf+(1−p)f′. This can be done because, since p∈(0,1), and qi<infx∈K(Ui)f(x), we have

pqi+(1−p)0<pinfx∈K(Ui)f(x)+(1−p)infx∈K(Uj)f(x)

And the rest of the argument works with no problems from there.

Lemma 8:If a∈(0,∞), and f′≪f, then af′≪af, provided af lies in the function space of interest. f,f′∈[X→(−∞,∞]] (or [X→[0,1]]), and X is compact, LHC, and second-countable.

By our constructions in Theorem 2, we can always write any function as the supremum of atomic step functions below it, (U↘q), as long as q<infx∈K(U)f(x). Since f≪f′, we can find finitely many atomic step functions (Ui↘qi) which all approximate f′ s.t. the function x↦supi:x∈Uiqi exceeds f. In the [X→(−∞,∞]] case, since the finite supremum exceeds f, which is bounded below by Lemma 1, the Ui family covers X.

Now, consider the finite collection of atomic step functions (Ui↘aqi). If we can show that all of these approximate af, and the supremum of them is larger than af′, then, since the supremum of finitely many approximators is an approximator, we'll have shown that af≫⨆i(Ui↘aqi)⊒af′, establishing approximation. So, let's show those. For arbitrary i, we have

And so, our result follows. It's possible that, for the [X→[0,1]] case, x lies in no Ui, but then the supremum of the empty set would be 0, and since the supremum of the (Ui↘qi) exceeds f′, f′(x)=0 as well, so the same inequality holds.

Lemma 9:If q∈R and f′≪f with f,f′∈[X→(−∞,∞]] with X being compact, LHC, and second-countable, then f′+cq≪f+cq.

We can invoke Theorem 2, to write any function as the supremum of atomic step functions below it, (U↘q′), as long as q′<infx∈K(U)f(x). Since f′≪f, we can find finitely many atomic step functions (Ui↘qi) which all approximate f s.t. the function x↦supi:x∈Uiqi exceeds f′. Also, f′ is bounded below by Lemma 1, so the finite family Ui covers the entire space.

Now, consider the finite collection of atomic step functions (Ui↘qi+q). If we can show that all of these approximate f+cq, and the supremum of them is larger than f′+cq, then, since the supremum of finitely many approximators is an approximator, we'll have shown that f+cq≫⨆i(Ui↘qi+q)⊒f′+cq, establishing approximation. So, let's show those. For arbitrary i, we have

qi+q<infx∈K(Ui)f(x)+q=infx∈K(Ui)(f+cq)(x)

So these atomic step functions all approximate f+cq. For exceeding f′+cq, we have, for arbitrary x,

Lemma 10:If q∈[−1,1] and f′≪f with f,f′∈[X→[0,1]] with X being compact, LHC, and second-countable, then for all ϵ, c0⊔f′+cq−ϵ≪f+cq, as long as f+cq is also bounded in [0,1].

By Theorem 2, we can always write any function as the supremum of atomic step functions below it, (U↘q′), where q′<infx∈K(O)f(x). Since f≪f′, we can find finitely many atomic step functions (Ui↘qi) which all approximate f s.t. the function x↦supi:x∈Uiqi exceeds f′.

Now, consider the following finite finite collection of atomic step functions. (Ui↘max(qi+q−ϵ,0)), along with (X↘max(q−ϵ,0))

If we can show that all of these approximate f+cq, and the supremum of them is larger than c0⊔(f′+cq−ϵ), then, since the supremum of finitely many approximators is an approximator, we'll have shown that f+cq≫(⨆i(Ui↘max(qi+q,0)))⊔(X↘max(q−ϵ,0))⊒c0⊔(f′+cq−ϵ), establishing approximation. So, let's show those.

For arbitrary i, if max(0,qi+q−ϵ)>0, then we have

qi+q−ϵ<infx∈K(Ui)f(x)+q=infx∈K(Ui)(f+cq)(x)

So these atomic step functions all approximate f+cq. If max(0,qi+q−ϵ)=0, then the atomic step function turns into c0, which also approximates f′+cq.

For the one extra step function we're adding in, we have two possible cases. One is where q−ϵ>0, the other one is where max(q−ϵ,0)=0. In such a case, the function turns into c_{0}, which trivially approximates f+cq. However, if q−ϵ>0, then we have

q−ϵ<q+infx∈Xf(x)≤(f+cq)(x′)

For any x′, so this constant strictly undershoots the minimal value of f+cq across the whole space, and thus approximates f+cq by Lemma 2.

So, this finite collection of functions has its supremum being an approximator of f+cq. Now for showing that the supremum beats c0⊔(f′+cq−ϵ). If x lies in some Ui, then

And we've shown that this supremum of step functions beats our new function. If x lies in none of the Ui, then the original supremum of step functions must have mapped x to 0, and that beats f, so f(x)=0. That's the only possible thing that could have happened. Then

So, this case is taken care of too, and our supremum of step functions beats c0⊔(f′+cq−ϵ). The lemma then finishes up, we have that f′≪f implies that for any ϵ and q s.t. f+cq and f′ and f all lie in [0,1], we have

c0⊔(f′+cq−ϵ)≪f+cq

NOW we can begin proving our theorems!

Theorem 4:The subset of [[X→(−∞,∞]]→[−∞,∞]] (or [[X→[0,1]]→[0,1]]) consisting of inframeasures is an ω-BC domain when X is compact, second-countable, and LHC.

This proof will begin by invoking either Corollary 1 or Proposition 6. Since locally hull-compact implies locally compact, we can invoke these, to get that [[X→(−∞,∞]]→[−∞,∞]], or [[X→[0,1]]→[0,1]] is an ω-BC domain with a top element.

Then, if we can just show that the set of inframeasures is closed under directed suprema and arbitrary nonempty infinima, we can invoke Theorem 3 to get that the space of R-inframeasures (or [0,1]-inframeasures) is an ω-BC domain. This is the tricky part.

For our conventions on working with infinity, we'll adopt the following. 0 times any number in (−∞,∞] is 0. Infinity times any number in (0,∞] is infinity. Infinity plus any number in (−∞,∞] is infinity. Given two functions f,f′ bounded below, then pf+(1−p)f′ is the function which maps x to pf(x)+(1−p)f′(x), which is always continuous when f,f′ are, due to being monotone, and preserving directed suprema. The distance between points in (−∞,∞], for defining the distance between functions as d(f,f′)=supxd(f(x),f′(x)) is the usual distance when both numbers are finite, 0 when both numbers are ∞ and ∞ when one point is ∞ and the other isn't.

An inframeasure is a function in [[X→(−∞,∞]]→[−∞,∞]] or [[X→[0,1]]→[0,1]] with the following three properties.

ψ should be 1-Lipschitz, it should map the constant-0 function c0 to 0 or higher, and it should be convex.

The definition of 1-Lipschitzness is that, using using our convention for the distance between points in [−∞,∞] and the distance between functions X→(−∞,∞], we have that for any two functions, d(ψ(f),ψ(f′))≤d(f,f′).

The definition of concavity is that, for all p∈[0,1],f,f′∈[X→(−∞,∞]],

pψ(f)+(1−p)ψ(f′)≤ψ(pf+(1−p)f′)

Admittedly, this might produce situations where we're adding infinity and negative infinity, which we haven't defined yet, but this case is ruled out by Lemma 3 and Lemma 1. Any function has a finite lower bound by Lemma 1, and Lemma 3 steps in to ensure that they must have a finite expectation value according to ψ. So, we'll never have to deal with cases where we're adding negative infinity to something, we're working entirely in the realm of real numbers plus infinity.

Now, let's get started on showing that the directed supremum of 1-Lipschitz, concave functions which map 0 upwards is 1-Lipschitz, concave, and maps 0 upwards.

Let's start with 1-Lipschitzness. In the case that our functions f,f′ have a distance of infinity from each other, 1-Lipschitness is trivially fulfilled. So we can assume that f,f′ have a finite distance from each other. Observe that it's impossible that (without loss of generality) (⨆↑Φ)(f) is infinity, while (⨆↑Φ)(f′) is finite. This is because we have

(⨆↑Φ)(f)=⨆↑ψ∈Φψ(f)

So, if that first term is infinite, we can find ψ∈Φ which map f arbitrarily high. And then ψ(f′) would only be a constant away, so the ψ(f′) values would climb arbitrarily high as well, making (⨆↑Φ)(f′) be infinite as well. Then we'd have

d((⨆↑Φ)(f),(⨆↑Φ)(f′))=d(∞,∞)=0≤d(f,f′)

And this would also show 1-Lipschitzness. So now we arrive at our last case where d(f,f′) is finite and the directed suprema are both finite. Then we'd have

and we're done. That was just unpacking definitions, and then the ≤ was because we can upper-bound the distance between the suprema of the two sets of numbers by the maximum distance between points paired off with each other. Then just apply 1-Lipschitzness at the end.

As for concavity, it's trivial when p=0 or 1, because then (for p=0 as an example)

p(⨆↑Φ)(f)+(1−p)(⨆↑Φ)(f′)=(⨆↑Φ)(f′)=(⨆↑Φ)(0f+1f′)

So now, let's start working on the case where p isn't 0 or 1. We have

First equality is just unpacking definitions. Second equality is because, if the directed supremum is unbounded above, multiplying by a finite constant and taking the directed supremum still gets you to infinity, and it also works for the finite constants. Then, we observe that for any ψ chosen by the first directed supremum and ψ′ chosen by the second, we can take an upper bound of the two to exceed the value. Conversely, any particular ψ can be used for both directed suprema. So we can move the directed suprema to the outside. Then we just apply concavity, and pack back up.

Finally, there's mapping 0 to above 0. This is easy.

(⨆↑Φ)(c0)=⨆↑ψ∈Φψ(c0)≥⨆↑ψ∈Φ0=0

All these proofs work equally well with both type signatures, so in both type signatures, the set of inframeausures is closed under directed suprema.

Now we'll show they're closed under unbounded infinima. This is the super-hard part. First up, 1-Lipschitzness.

1-Lipschitzness is trivial if d(f,f′)=∞, so we can assume that this value is finite. It's also trivial if (⊓Φ)(f)=∞=(⊓Φ)(f′), because then the distance is 0. So we can assume that one of these values is finite. Without loss of generality, let's say that (⊓Φ)(f)≥(⊓Φ)(f′). Then, we can go:

Via Lemma 3. Now, at this point, we're going to need to invoke either Lemma 5 for the R case, or Lemma 6 for the [0,1] case. We'll treat the two cases identically by using the terminology c⊥⊔(f′′+c−d(f,f′)). In the R case, this is just f′′+c−d(f,f′), because the functions f′′ have a finite lower bound via compactness/Lemma 1, and we're in the assumed case where d(f,f′)<∞. In the [0,1] case, it's c0⊔(f′′+c−d(f,f′)), which is a different sort of function. Anyways, since we have f′′≪f, this then means that c⊥⊔(f′′+c−d(f,f′))≪f′ by Lemma 5 or 6 (as the type signature may be). So, swapping out the supremum over f′′′≪f′ with choosing a f′′≪f and evaluating the c⊥⊔(f′′+c−d(f,f′)), makes that second directed supremum go down in value, so the value of the equation as a whole go up. So, in both cases, we have

The starting inequality was already extensively discussed. Then, the shift to the absolute value is because we know the quantity as a whole is positive. The gap between the two suprema is upper-bounded by the maximum gap between the two terms with the same f′′ chosen. Similarly, the gap between thetwo infinima is upper-bounded by the maximum gap between the two terms with the same ψ chosen. Then we just do a quick conversion to distance, and apply 1-Lipschitzness of all the ψ we're taking the infinimum of. Continuing onwards, we have

Now, we've got two possibilities. The first case is where f′′ has range in (−∞,∞]. In such a case, the latter term would turn into −d(f,f′), so the contents as a whole of the absolute value would be d(f,f′). The second case is where f′′ has range in [0,1]. In such a case, the latter term would be as close or closer to f′′(x) than f′′(x)−d(f,f′), so we can upper-bound the contents of the absolute-value chunk by d(f,f′). In both cases, we have

≤⨆f′′≪fsupx∈X|f′′(x)−(f′′(x)−d(f,f′))|=d(f,f′)

And we're done, 1-Lipschitzness is preserved under arbitrary infinima, for both type signatures.

Now for concavity. Concavity is trivial when p=0 or 1, so let's assume p∈(0,1), letting us invoke Lemma 7. Let's show concavity. We have

The first equality was just unpacking via Lemma 3. Then we can move the constant in, group into a single big directed supremum, combine the infs (making the inside bigger), then apply concavity for all our ψ∈Φ. Now it gets interesting. Since f′′≪f and f′′′≪f′ and p∈(0,1) we have that pf′′+(1−p)f′′′≪pf+(1−p)f′ by Lemma 7. Since all possible choices make an approximator for pf+(1−p)f′, we can go...

≤⨆↑f∗≪pf+(1−p)f′⊓ψ∈Φψ(f∗)=(⊓Φ)(pf+(1−p)f′)

And concavity is shown. The proof works equally well for both type signatures.

All that remains is showing that the constant-0 function maps to 0 or higher, which is thankfully, quite easy, compared to concavity and 1-Lipschitzness. This is automatic for the [0,1] case, so we'll just be dealing with the other type signature.

Remember our result back in Lemma 2 that if you have a constant function cq where q<infx∈Xf(x), then cq≪f. We'll be using that. Also we'll be using Lemma 4 that no 1-Lipschitz function mapping c0 to 0 or higher can map a function f any lower than inf(0,infx∈Xf(x)), which is finite, by Lemma 1. So, we have

(⊓Φ)(c0)=⨆↑f≪c0⊓ψ∈Φψ(f)≥⨆↑q<0⊓ψ∈Φψ(cq)≥⨆↑q<0q=0

And we're done. First equality was just the usual unpacking of infinite inf via Lemma 3, second one was because, if q<0, then cq≪c0, so the function value goes down, and the third inequality was because none of the ψ can map cq below q since q<0. That's it!

Now, since the space of inframeasures (concave, 1-Lipschitz, weakly-normalized) is closed under directed sup and arbitrary inf in [[X→(−∞,∞]]→[−∞,∞]] and [[X→[0,1]]→[0,1]], we can invoke Theorem 3 to conclude that it makes an ω-BC domain.

Theorem 5:The following properties are all preserved under arbitrary infinima and directed supremum for both R and [0,1]-inframeasures, if X is compact, second-countable, and LHC.

ψ(c0)=0

ψ(c1)≥1

ψ(c1)≤1

ψ(c1)=1

∀q∈R:ψ(cq)=q(supernormalization)

∀a∈[0,∞):ψ(af)=aψ(f) (homogenity)

∀a∈[0,∞):ψ(1−af)=1−a+aψ(f) (cohomogenity)

∀q∈R:ψ(f+cq)=ψ(f)+q (C-additivity)

∀q∈R,a∈[0,∞):ψ(af+cq)=aψ(f)+q (crispness)

So, the deal with this proof is that the directed suprema part works equally well for both cases, but the arbitrary infinima part will need to be done once for the R type signature (where it's marginally easier), and done a second way for the [0,1] case, where it's considerably more difficult to accomplish.

First, ψ(c0)=0.

(⨆↑Φ)(c0)=⨆↑ψ∈Φψ(c0)=⨆↑ψ∈Φ0=0

Second, ψ(c1)≥1.

(⨆↑Φ)(c1)=⨆↑ψ∈Φψ(c1)≥⨆↑ψ∈Φ1=1

Third, ψ(c1)≤1.

(⨆↑Φ)(c1)=⨆↑ψ∈Φψ(c1)≤⨆↑ψ∈Φ1=1

Fourth, ψ(c1)=1, which is trivial from second and third.

Ninth, crispness, which follows from six and eight since crispnes is equivalent to the conjunction of homogenity and c-additivity.

Now for arbitrary infinima in the R case. We'll note when the same proof works for the [0,1] case, and when we have to loop back later with a more sophisticated argument. Lemma 3 is used throughout.

First, preservation of ψ(c0)=0 under infinima. We already know that, by ψ(c0)≥0 being preserved under arbitrary infinima it can't be below 0, so that leaves showing that it can't be above 0.

(⊓Φ)(c0)=⨆↑f≪c0⊓ψ∈Φψ(f)≤⊓ψ∈Φψ(c0)=0

This was by monotonicity, since c0⊒f, and then we just apply that ψ(c0)=0. This proof works for the [0,1] type signature.

Second, preservation of ψ(c1)≥1 under infinima. Since cq≪c1 when q<1 via Lemma 2, we can go

And we're done. In order, that was unpacking the arbitrary inf, the inequality was because we swapped out for a more restricted class of approximators (value decreases), then we reexpressed cq, applied concavity (value decreases), distributed the inf in (value decreases), used that ψ(c0)≥0 always, and our assumption that ψ(c1)≥1 (value decreases), and then we can finish up easily. Same proof works just as well for the [0,1] type signature.

Third, preservation of ψ(c1)≤1 under infinima. Since cq≪c1 when q<1 by Lemma 2, we can go

(⊓Φ)(c1)=⨆↑f≪c1⊓ψ∈Φψ(f)≤⊓ψ∈Φψ(c1)≤1

Due to monotonicity. Same proof works for the [0,1] type signature.

Fourth, preservation of ψ(c1)=1 under infinima. This is trivial since we proved preservation of ≥ and ≤ under infinima already, for both type signatures.

For 5, supernormalization is that ψ(cq)=q for all numbers in (−∞,∞] or [0,1] respectively. We'll show this is preserved under infinima. We have to prove both directions of this separately. In one direction, we have

q=⊓ψ∈Φψ(cq)≥⨆↑f≪cq⊓ψ∈Φψ(f)=(⊓Φ)(cq)

Which establishes an upper bound. For a lower bound, we have, since p<q implies cp≪cq by Lemma 2,

(⊓Φ)(cq)=⨆↑f≪cq⊓ψ∈Φψ(f)≥⨆↑p<q⊓ψ∈Φψ(cp)=⨆↑p<qp=q

Now, for the [0,1] type signature, the only fiddly bit is the lower-bound argument, because maybe q<

Lemma 7:Forf,f′,f′′,f′′′∈[X→(−∞,∞]s.t.f′′≪fandf′′′≪f′, andp∈(0,1), andXis compact, LHC, and second-countable, thenpf′′+(1−p)f′′′≪pf+(1−p)f′. The same result holds for[X→[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, pf′′+(1−p)f′′′⊑pg+(1−p)g′ as a result. We'll then show that pg+(1−p)g′ can be written as the supremum of finitely many functions in [X→[−∞,∞]] (or [X→[0,1]]) which all approximate pf+(1−p)f′, so pf+(1−p)f′≫pg+(1−p)g′⊒pf′′+(1−p)f′′′, establishing that pf+(1−p)f′≫pf′′+(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<infx∈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)=supi(Ui↘qi)(x)=supi:x∈Uiqi

and, by how our atomic step functions of the directed set associated with f were built, we know that for all i, qi<infx∈K(Ui)f(x). (remember, the Ui are selected from the base, so we can take the compact hull of them).

There's a critical split here between the behavior of the [X→[−∞,∞]] type signature, and the [X→[0,1]] type signature.

For the [X→[−∞,∞]] type signature, there's finitely many i, and everything not in the Ui gets mapped to −∞. Since f′′∈[X→(−∞,∞]], and X is compact, f′′ is bounded below (Lemma 1), so for this finite supremum to exceed f′′, the Ui must cover X.

For the [X→[0,1]] type signature, again there's finitely many i, but we can't guarantee that the Ui cover X, because everything not in some Ui gets mapped to 0, and f′′ might not be bounded above 0. So, we'll add in a "dummy" step function (X↘0). This is just the constant-0 function, which approximates everything, so nothing changes. However, it ensures that X is indeed covered by the open sets of the finite collection of step functions.

So... Given that we have our g,g′, what does the function pg+(1−p)g′ look like? Well, it looks like

pg(x)+(1−p)g′(x)=psupi:x∈Uiqi+(1−p)supj:x∈Ujqj=supi:x∈Uipqi+supj:x∈Uj(1−p)qj

=supi,j:x∈Ui∩Uj(pqi+(1−p)qj)=supi,j(Ui∩Uj↘pqi+(1−p)qj)(x)

We could do this in the [0,1] case from adding in the "dummy" open sets to get the Ui family and Uj family to both cover X.

Anyways, pg+(1−p)g′ equals ⨆i,j(Ui∩Uj↘pqi+(1−p)qj). There's finitely many i's and finitely many j's by how g and g' were built, so this is a supremum of finitely many atomic step functions. Since pg+(1−p)g′⊒pf′′+(1−p)f′′′, if we can just show that all these atomic step functions are approximators for pf+(1−p)f′ in [X→[−∞,∞]] (or [X→[0,1]]), then pg+(1−p)g′≪pf+(1−p)f′ (supremum of finitely many approximators is an approximator), and we'd show our desired result that pf′′+(1−p)f′′′≪pf+(1−p)f′. So let's get started on showing that, regardless of i and j,

(Ui∩Uj↘pqi+(1−p)qj)≪pf+(1−p)f′

Now, if Ui∩Uj=∅, then this function maps everything to −∞ or 0, which trivially approximates pf+(1−p)f′. Otherwise, everything in Ui∩Uj gets mapped to pqi+(1−p)qj, and everything not in it gets mapped to −∞ (or 0)

We know by our process of construction for this that qi<infx∈K(Ui)f(x) and qj<infx∈K(Uj)f′(x), so let's try to work with that. Well, for the [X→[−∞,∞]] case. The [X→[0,1]] case is a bit more delicate since we added those two dummy functions. We have:

pqi+(1−p)qj<pinfx∈K(Ui)f(x)+(1−p)infx∈K(Uj)f(x)

=infx∈K(Ui)pf(x)+infx∈K(Uj)(1−p)f(x)

≤infx∈K(Ui∩Uj)pf(x)+infx∈K(Ui∩Uj)(1−p)f(x)

≤infx∈K(Ui∩Uj)(pf(x)+(1−p)f′(x))=infx∈K(Ui∩Uj)(pf+(1−p)f′)(x)

The first strict inequality was because of what qi and qj were. Then, just move the constants in. For the first non-strict inquality, it's because of monotonicity for our compact hull operator, Ui∩Uj⊆Ui, so it has a smaller compact hull. Then the next inequality is just grouping the two infs, and we're finished.

At this point, the usual argument of "fix a directed set of functions ascending up to pf+(1−p)f′, for each patch of K(Ui∩Uj) you can find a function from your directed set that beats the value pqi+(1−p)qj on that spot, this gets you an open cover of K(Ui∩Uj), it's compact, isolate a finite subcover ie finitely many functions, take an upper bound in your directed set, bam, it beats the step function on a compact superset of its open set so it beats the step function, and the directed set was arbitrary so pf+(1−p)f′ is approximated by the atomic step function" from Theorem 2 kicks in, to show that the atomic step function approximates pf+(1−p)f′. Since this works for arbitrary i,j, and there are finitely many of these, the finite supremum pg+(1−p)g′ approximates pf+(1−p)f′, and dominates pf′′+(1−p)f′′′, and we're done.

Now for the [X→[0,1]] case. This case works perfectly fine if our i,j pair has qi and pi being above 0. But what if our Ui has qi being above 0, but our j index is picking that (X↘0) "dummy" approximator? Or vice-versa. Or maybe they're both the "dummy" approximator.

That last case can be disposed of, because (X∩X↘p⋅0+(1−p)⋅0) is just the constant-0 function, which trivially approximates everything. That leaves the case where just one of the step functions isn't the constant-0 function. Without loss of generality, assume Ui is paired with qi>0, but the other one is the (X↘0) "dummy" approximator. Then our goal is to show that (Ui∩X↘pqi+(1−p)0)≪pf+(1−p)f′. This can be done because, since p∈(0,1), and qi<infx∈K(Ui)f(x), we have

pqi+(1−p)0<pinfx∈K(Ui)f(x)+(1−p)infx∈K(Uj)f(x)

And the rest of the argument works with no problems from there.

Lemma 8:Ifa∈(0,∞), andf′≪f, thenaf′≪af, providedaflies in the function space of interest.f,f′∈[X→(−∞,∞]](or[X→[0,1]]), andXis compact, LHC, and second-countable.By our constructions in Theorem 2, we can always write any function as the supremum of atomic step functions below it, (U↘q), as long as q<infx∈K(U)f(x). Since f≪f′, we can find finitely many atomic step functions (Ui↘qi) which all approximate f′ s.t. the function x↦supi:x∈Uiqi exceeds f. In the [X→(−∞,∞]] case, since the finite supremum exceeds f, which is bounded below by Lemma 1, the Ui family covers X.

Now, consider the finite collection of atomic step functions (Ui↘aqi). If we can show that all of these approximate af, and the supremum of them is larger than af′, then, since the supremum of finitely many approximators is an approximator, we'll have shown that af≫⨆i(Ui↘aqi)⊒af′, establishing approximation. So, let's show those. For arbitrary i, we have

aqi<a⋅infx∈K(Ui)f(x)=infx∈K(Ui)a⋅f(x)=infx∈K(Ui)(af)(x)

So these atomic step functions all approximate af. For exceeding af′, we have, for arbitrary x,

⊔i(Ui↘aqi)(x)=supi:x∈Ui(aqi)=asupi:x∈Uiqi≥a⋅f′(x)=(af′)(x)

And so, our result follows. It's possible that, for the [X→[0,1]] case, x lies in no Ui, but then the supremum of the empty set would be 0, and since the supremum of the (Ui↘qi) exceeds f′, f′(x)=0 as well, so the same inequality holds.

Lemma 9:Ifq∈Randf′≪fwithf,f′∈[X→(−∞,∞]]withXbeing compact, LHC, and second-countable, thenf′+cq≪f+cq.We can invoke Theorem 2, to write any function as the supremum of atomic step functions below it, (U↘q′), as long as q′<infx∈K(U)f(x). Since f′≪f, we can find finitely many atomic step functions (Ui↘qi) which all approximate f s.t. the function x↦supi:x∈Uiqi exceeds f′. Also, f′ is bounded below by Lemma 1, so the finite family Ui covers the entire space.

Now, consider the finite collection of atomic step functions (Ui↘qi+q). If we can show that all of these approximate f+cq, and the supremum of them is larger than f′+cq, then, since the supremum of finitely many approximators is an approximator, we'll have shown that f+cq≫⨆i(Ui↘qi+q)⊒f′+cq, establishing approximation. So, let's show those. For arbitrary i, we have

qi+q<infx∈K(Ui)f(x)+q=infx∈K(Ui)(f+cq)(x)

So these atomic step functions all approximate f+cq. For exceeding f′+cq, we have, for arbitrary x,

⊔i(Ui↘qi+q)(x)=supi:x∈Ui(qi+q)=supi:x∈Ui(qi)+q≥f′(x)+q=(f+cq)(x)

And so, our result follows.

Lemma 10:Ifq∈[−1,1]andf′≪fwithf,f′∈[X→[0,1]]withXbeing compact, LHC, and second-countable, then for allϵ,c0⊔f′+cq−ϵ≪f+cq, as long asf+cqis also bounded in[0,1].By Theorem 2, we can always write any function as the supremum of atomic step functions below it, (U↘q′), where q′<infx∈K(O)f(x). Since f≪f′, we can find finitely many atomic step functions (Ui↘qi) which all approximate f s.t. the function x↦supi:x∈Uiqi exceeds f′.

Now, consider the following finite finite collection of atomic step functions. (Ui↘max(qi+q−ϵ,0)), along with (X↘max(q−ϵ,0))

If we can show that all of these approximate f+cq, and the supremum of them is larger than c0⊔(f′+cq−ϵ), then, since the supremum of finitely many approximators is an approximator, we'll have shown that f+cq≫(⨆i(Ui↘max(qi+q,0)))⊔(X↘max(q−ϵ,0))⊒c0⊔(f′+cq−ϵ), establishing approximation. So, let's show those.

For arbitrary i, if max(0,qi+q−ϵ)>0, then we have

qi+q−ϵ<infx∈K(Ui)f(x)+q=infx∈K(Ui)(f+cq)(x)

So these atomic step functions all approximate f+cq. If max(0,qi+q−ϵ)=0, then the atomic step function turns into c0, which also approximates f′+cq.

For the one extra step function we're adding in, we have two possible cases. One is where q−ϵ>0, the other one is where max(q−ϵ,0)=0. In such a case, the function turns into c_{0}, which trivially approximates f+cq. However, if q−ϵ>0, then we have

q−ϵ<q+infx∈Xf(x)≤(f+cq)(x′)

For any x′, so this constant strictly undershoots the minimal value of f+cq across the whole space, and thus approximates f+cq by Lemma 2.

So, this finite collection of functions has its supremum being an approximator of f+cq. Now for showing that the supremum beats c0⊔(f′+cq−ϵ). If x lies in some Ui, then

max(supi:x∈Ui(qi+q−ϵ),q−ϵ,0)=max(supi:x∈Ui(qi+q−ϵ),0)

=max(supi:x∈Ui(qi)+q−ϵ,0)≥max(f′(x)+q−ϵ,0)=(c0⊔(f′+cq−ϵ))(x)

And we've shown that this supremum of step functions beats our new function. If x lies in none of the Ui, then the original supremum of step functions must have mapped x to 0, and that beats f, so f(x)=0. That's the only possible thing that could have happened. Then

max(supi:x∈Ui(qi+q−ϵ),q−ϵ,0)=max(0,q−ϵ)=max(0,0+q−ϵ)=(c0⊔(f′+cq−ϵ))(x)

So, this case is taken care of too, and our supremum of step functions beats c0⊔(f′+cq−ϵ). The lemma then finishes up, we have that f′≪f implies that for any ϵ and q s.t. f+cq and f′ and f all lie in [0,1], we have

c0⊔(f′+cq−ϵ)≪f+cq

NOW we can begin proving our theorems!

Theorem 4:The subset of[[X→(−∞,∞]]→[−∞,∞]](or[[X→[0,1]]→[0,1]]) consisting of inframeasures is anω-BC domain whenXis compact, second-countable, and LHC.This proof will begin by invoking either Corollary 1 or Proposition 6. Since locally hull-compact implies locally compact, we can invoke these, to get that [[X→(−∞,∞]]→[−∞,∞]], or [[X→[0,1]]→[0,1]] is an ω-BC domain with a top element.

Then, if we can just show that the set of inframeasures is closed under directed suprema and arbitrary nonempty infinima, we can invoke Theorem 3 to get that the space of R-inframeasures (or [0,1]-inframeasures) is an ω-BC domain. This is the tricky part.

For our conventions on working with infinity, we'll adopt the following. 0 times any number in (−∞,∞] is 0. Infinity times any number in (0,∞] is infinity. Infinity plus any number in (−∞,∞] is infinity. Given two functions f,f′ bounded below, then pf+(1−p)f′ is the function which maps x to pf(x)+(1−p)f′(x), which is always continuous when f,f′ are, due to being monotone, and preserving directed suprema. The distance between points in (−∞,∞], for defining the distance between functions as d(f,f′)=supxd(f(x),f′(x)) is the usual distance when both numbers are finite, 0 when both numbers are ∞ and ∞ when one point is ∞ and the other isn't.

An inframeasure is a function in [[X→(−∞,∞]]→[−∞,∞]] or [[X→[0,1]]→[0,1]] with the following three properties.

ψ should be 1-Lipschitz, it should map the constant-0 function c0 to 0 or higher, and it should be convex.

The definition of 1-Lipschitzness is that, using using our convention for the distance between points in [−∞,∞] and the distance between functions X→(−∞,∞], we have that for any two functions, d(ψ(f),ψ(f′))≤d(f,f′).

The definition of concavity is that, for all p∈[0,1],f,f′∈[X→(−∞,∞]],

pψ(f)+(1−p)ψ(f′)≤ψ(pf+(1−p)f′)

Admittedly, this might produce situations where we're adding infinity and negative infinity, which we haven't defined yet, but this case is ruled out by Lemma 3 and Lemma 1. Any function has a finite lower bound by Lemma 1, and Lemma 3 steps in to ensure that they must have a finite expectation value according to ψ. So, we'll never have to deal with cases where we're adding negative infinity to something, we're working entirely in the realm of real numbers plus infinity.

Now, let's get started on showing that the directed supremum of 1-Lipschitz, concave functions which map 0 upwards is 1-Lipschitz, concave, and maps 0 upwards.

Let's start with 1-Lipschitzness. In the case that our functions f,f′ have a distance of infinity from each other, 1-Lipschitness is trivially fulfilled. So we can assume that f,f′ have a finite distance from each other. Observe that it's impossible that (without loss of generality) (⨆↑Φ)(f) is infinity, while (⨆↑Φ)(f′) is finite. This is because we have

(⨆↑Φ)(f)=⨆↑ψ∈Φψ(f)

So, if that first term is infinite, we can find ψ∈Φ which map f arbitrarily high. And then ψ(f′) would only be a constant away, so the ψ(f′) values would climb arbitrarily high as well, making (⨆↑Φ)(f′) be infinite as well. Then we'd have

d((⨆↑Φ)(f),(⨆↑Φ)(f′))=d(∞,∞)=0≤d(f,f′)

And this would also show 1-Lipschitzness. So now we arrive at our last case where d(f,f′) is finite and the directed suprema are both finite. Then we'd have

d((⨆↑Φ)(f),(⨆↑Φ)(f′))=∣∣(⨆↑Φ)(f)−(⨆↑Φ)(f′)∣∣

=∣∣⨆↑ψ∈Φψ(f)−⨆↑ψ∈Φψ(f′)∣∣≤⨆ψ∈Φ|ψ(f)−ψ(f′)|≤d(f,f′)

and we're done. That was just unpacking definitions, and then the ≤ was because we can upper-bound the distance between the suprema of the two sets of numbers by the maximum distance between points paired off with each other. Then just apply 1-Lipschitzness at the end.

As for concavity, it's trivial when p=0 or 1, because then (for p=0 as an example)

p(⨆↑Φ)(f)+(1−p)(⨆↑Φ)(f′)=(⨆↑Φ)(f′)=(⨆↑Φ)(0f+1f′)

So now, let's start working on the case where p isn't 0 or 1. We have

p(⨆↑Φ)(f)+(1−p)(⨆↑Φ)(f′)=p⨆↑ψ∈Φψ(f)+(1−p)⨆↑ψ∈Φψ(f′)

=⨆↑ψ∈Φpψ(f)+⨆↑ψ∈Φ(1−p)ψ(f′)=⨆↑ψ∈Φ(pψ(f)+(1−p)ψ(f′))

≤⨆↑ψ∈Φψ(pf+(1−p)f′)=(⨆↑Φ)(pf+(1−p)f′)

First equality is just unpacking definitions. Second equality is because, if the directed supremum is unbounded above, multiplying by a finite constant and taking the directed supremum still gets you to infinity, and it also works for the finite constants. Then, we observe that for any ψ chosen by the first directed supremum and ψ′ chosen by the second, we can take an upper bound of the two to exceed the value. Conversely, any particular ψ can be used for both directed suprema. So we can move the directed suprema to the outside. Then we just apply concavity, and pack back up.

Finally, there's mapping 0 to above 0. This is easy.

(⨆↑Φ)(c0)=⨆↑ψ∈Φψ(c0)≥⨆↑ψ∈Φ0=0

All these proofs work equally well with both type signatures, so in both type signatures, the set of inframeausures is closed under directed suprema.

Now we'll show they're closed under unbounded infinima. This is the super-hard part. First up, 1-Lipschitzness.

1-Lipschitzness is trivial if d(f,f′)=∞, so we can assume that this value is finite. It's also trivial if (⊓Φ)(f)=∞=(⊓Φ)(f′), because then the distance is 0. So we can assume that one of these values is finite. Without loss of generality, let's say that (⊓Φ)(f)≥(⊓Φ)(f′). Then, we can go:

d((⊓Φ)(f),(⊓Φ)(f′))=(⊓Φ)(f)−(⊓Φ)(f′)=⨆↑f′′≪f⊓ψ∈Φψ(f′′)−⨆↑f′′′≪f′⊓ψ∈Φψ(f′′′)

Via Lemma 3. Now, at this point, we're going to need to invoke either Lemma 5 for the R case, or Lemma 6 for the [0,1] case. We'll treat the two cases identically by using the terminology c⊥⊔(f′′+c−d(f,f′)). In the R case, this is just f′′+c−d(f,f′), because the functions f′′ have a finite lower bound via compactness/Lemma 1, and we're in the assumed case where d(f,f′)<∞. In the [0,1] case, it's c0⊔(f′′+c−d(f,f′)), which is a different sort of function. Anyways, since we have f′′≪f, this then means that c⊥⊔(f′′+c−d(f,f′))≪f′ by Lemma 5 or 6 (as the type signature may be). So, swapping out the supremum over f′′′≪f′ with choosing a f′′≪f and evaluating the c⊥⊔(f′′+c−d(f,f′)), makes that second directed supremum go

downin value, so the value of the equation as a whole go up. So, in both cases, we have⨆↑f′′≪f⊓ψ∈Φψ(f′′)−⨆↑f′′′≪f′⊓ψ∈Φψ(f′′′)

≤⨆↑f′′≪f⊓ψ∈Φψ(f′′)−⨆↑f′′≪f⊓ψ∈Φψ(c⊥⊔(f′′+c−d(f,f′)))

=∣∣⨆↑f′′≪f⊓ψ∈Φψ(f′′)−⨆↑f′′≪f⊓ψ∈Φψ(c⊥⊔(f′′+c−d(f,f′)))∣∣

≤⨆f′′≪f|⊓ψ∈Φψ(f′′)−⊓ψ∈Φψ(c⊥⊔(f′′+c−d(f,f′)))|

≤⨆f′′≪f⨆ψ∈Φ|ψ(f′′)−ψ(c⊥⊔(f′′+c−d(f,f′)))|

=⨆f′′≪f⨆ψ∈Φd(ψ(f′′),ψ(c⊥⊔(f′′+c−d(f,f′))))

≤⨆f′′≪f⨆ψ∈Φd(f′′,c⊥⊔(f′′+c−d(f,f′)))

The starting inequality was already extensively discussed. Then, the shift to the absolute value is because we know the quantity as a whole is positive. The gap between the two suprema is upper-bounded by the maximum gap between the two terms with the same f′′ chosen. Similarly, the gap between thetwo infinima is upper-bounded by the maximum gap between the two terms with the same ψ chosen. Then we just do a quick conversion to distance, and apply 1-Lipschitzness of all the ψ we're taking the infinimum of. Continuing onwards, we have

=⨆f′′≪fd(f′′,c⊥⊔(f′′+c−d(f,f′)))=⨆f′′≪fsupx∈X|f′′(x)−sup(⊥,f′′(x)−d(f,f′))|

Now, we've got two possibilities. The first case is where f′′ has range in (−∞,∞]. In such a case, the latter term would turn into −d(f,f′), so the contents as a whole of the absolute value would be d(f,f′). The second case is where f′′ has range in [0,1]. In such a case, the latter term would be

as close or closerto f′′(x) than f′′(x)−d(f,f′), so we can upper-bound the contents of the absolute-value chunk by d(f,f′). In both cases, we have≤⨆f′′≪fsupx∈X|f′′(x)−(f′′(x)−d(f,f′))|=d(f,f′)

And we're done, 1-Lipschitzness is preserved under arbitrary infinima, for both type signatures.

Now for concavity. Concavity is trivial when p=0 or 1, so let's assume p∈(0,1), letting us invoke Lemma 7. Let's show concavity. We have

p(⊓Φ)(f)+(1−p)(⊓Φ)(f′)=p⨆↑f′′≪f⊓ψ∈Φψ(f′′)+(1−p)⨆↑f′′′≪f′⊓ψ∈Φψ(f′′′)

=⨆↑f′′≪f⊓ψ∈Φpψ(f′′)+⨆↑f′′′≪f′⊓ψ∈Φ(1−p)ψ(f′′′)

=⨆↑f′′≪f,f′′′≪f′(⊓ψ∈Φpψ(f′′)+⊓ψ∈Φ(1−p)ψ(f′′′))

≤⨆↑f′′≪f,f′′′≪f′⊓ψ∈Φ(pψ(f′′)+(1−p)ψ(f′′′))

≤⨆↑f′′≪f,f′′′≪f′⊓ψ∈Φψ(pf′′+(1−p)f′′′)

The first equality was just unpacking via Lemma 3. Then we can move the constant in, group into a single big directed supremum, combine the infs (making the inside bigger), then apply concavity for all our ψ∈Φ. Now it gets interesting. Since f′′≪f and f′′′≪f′ and p∈(0,1) we have that pf′′+(1−p)f′′′≪pf+(1−p)f′ by Lemma 7. Since all possible choices make an approximator for pf+(1−p)f′, we can go...

≤⨆↑f∗≪pf+(1−p)f′⊓ψ∈Φψ(f∗)=(⊓Φ)(pf+(1−p)f′)

And concavity is shown. The proof works equally well for both type signatures.

All that remains is showing that the constant-0 function maps to 0 or higher, which is thankfully, quite easy, compared to concavity and 1-Lipschitzness. This is automatic for the [0,1] case, so we'll just be dealing with the other type signature.

Remember our result back in Lemma 2 that if you have a constant function cq where q<infx∈Xf(x), then cq≪f. We'll be using that. Also we'll be using Lemma 4 that no 1-Lipschitz function mapping c0 to 0 or higher can map a function f any lower than inf(0,infx∈Xf(x)), which is finite, by Lemma 1. So, we have

(⊓Φ)(c0)=⨆↑f≪c0⊓ψ∈Φψ(f)≥⨆↑q<0⊓ψ∈Φψ(cq)≥⨆↑q<0q=0

And we're done. First equality was just the usual unpacking of infinite inf via Lemma 3, second one was because, if q<0, then cq≪c0, so the function value goes down, and the third inequality was because none of the ψ can map cq below q since q<0. That's it!

Now, since the space of inframeasures (concave, 1-Lipschitz, weakly-normalized) is closed under directed sup and arbitrary inf in [[X→(−∞,∞]]→[−∞,∞]] and [[X→[0,1]]→[0,1]], we can invoke Theorem 3 to conclude that it makes an ω-BC domain.

Theorem 5:The following properties are all preserved under arbitrary infinima and directed supremum for bothRand[0,1]-inframeasures, ifXis compact, second-countable, and LHC.ψ(c0)=0

ψ(c1)≥1

ψ(c1)≤1

ψ(c1)=1

∀q∈R:ψ(cq)=q(supernormalization)

∀a∈[0,∞):ψ(af)=aψ(f) (homogenity)

∀a∈[0,∞):ψ(1−af)=1−a+aψ(f) (cohomogenity)

∀q∈R:ψ(f+cq)=ψ(f)+q (C-additivity)

∀q∈R,a∈[0,∞):ψ(af+cq)=aψ(f)+q (crispness)

So, the deal with this proof is that the directed suprema part works equally well for both cases, but the arbitrary infinima part will need to be done once for the R type signature (where it's marginally easier), and done a second way for the [0,1] case, where it's considerably more difficult to accomplish.

First, ψ(c0)=0.

(⨆↑Φ)(c0)=⨆↑ψ∈Φψ(c0)=⨆↑ψ∈Φ0=0

Second, ψ(c1)≥1.

(⨆↑Φ)(c1)=⨆↑ψ∈Φψ(c1)≥⨆↑ψ∈Φ1=1

Third, ψ(c1)≤1.

(⨆↑Φ)(c1)=⨆↑ψ∈Φψ(c1)≤⨆↑ψ∈Φ1=1

Fourth, ψ(c1)=1, which is trivial from second and third.

Fifth, supernormalization.

(⨆↑Φ)(cq)=⨆↑ψ∈Φψ(cq)=⨆↑ψ∈Φq=q

Sixth, homogenity.

(⨆↑Φ)(af)=⨆↑ψ∈Φψ(af)=⨆↑ψ∈Φaψ(f)=a⨆↑ψ∈Φψ(f)=a(⨆↑Φ)(f)

Seventh, cohomogenity.

(⨆↑Φ)(c1+a(−f))=⨆↑ψ∈Φψ(c1+a(−f))=⨆↑ψ∈Φ(1−a+aψ(1+(−f)))

=1−a+a⨆↑ψ∈Φψ(1+(−f))=1−a+a(⨆↑Φ)(1+(−f))

Eighth, C-additivity.

(⨆↑Φ)(f+cq)=⨆↑ψ∈Φψ(f+cq)=⨆↑ψ∈Φ(q+ψ(f))=q+⨆↑ψ∈Φψ(f)=q+(⨆↑Φ)(f)

Ninth, crispness, which follows from six and eight since crispnes is equivalent to the conjunction of homogenity and c-additivity.

Now for arbitrary infinima in the R case. We'll note when the same proof works for the [0,1] case, and when we have to loop back later with a more sophisticated argument. Lemma 3 is used throughout.

First, preservation of ψ(c0)=0 under infinima. We already know that, by ψ(c0)≥0 being preserved under arbitrary infinima it can't be

below0, so that leaves showing that it can't beabove0.(⊓Φ)(c0)=⨆↑f≪c0⊓ψ∈Φψ(f)≤⊓ψ∈Φψ(c0)=0

This was by monotonicity, since c0⊒f, and then we just apply that ψ(c0)=0. This proof works for the [0,1] type signature.

Second, preservation of ψ(c1)≥1 under infinima. Since cq≪c1 when q<1 via Lemma 2, we can go

(⊓Φ)(c1)=⨆↑f≪c1⊓ψ∈Φψ(f)≥⨆↑q∈[0,1)⊓ψ∈Φψ(cq)=⨆↑q∈[0,1)⊓ψ∈Φψ(qc1+(1−q)c0)

≥⨆↑q∈[0,1)⊓ψ∈Φ(qψ(c1)+(1−q)ψ(c0))≥⨆↑q∈[0,1)(q⊓ψ∈Φψ(c1)+(1−q)⊓ψ∈Φψ(c0))

≥⨆↑q∈[0,1)(q⋅1+(1−q)⋅0)=⨆↑q∈[0,1)q=1

And we're done. In order, that was unpacking the arbitrary inf, the inequality was because we swapped out for a more restricted class of approximators (value decreases), then we reexpressed cq, applied concavity (value decreases), distributed the inf in (value decreases), used that ψ(c0)≥0 always, and our assumption that ψ(c1)≥1 (value decreases), and then we can finish up easily. Same proof works just as well for the [0,1] type signature.

Third, preservation of ψ(c1)≤1 under infinima. Since cq≪c1 when q<1 by Lemma 2, we can go

(⊓Φ)(c1)=⨆↑f≪c1⊓ψ∈Φψ(f)≤⊓ψ∈Φψ(c1)≤1

Due to monotonicity. Same proof works for the [0,1] type signature.

Fourth, preservation of ψ(c1)=1 under infinima. This is trivial since we proved preservation of ≥ and ≤ under infinima already, for both type signatures.

For 5, supernormalization is that ψ(cq)=q for all numbers in (−∞,∞] or [0,1] respectively. We'll show this is preserved under infinima. We have to prove both directions of this separately. In one direction, we have

q=⊓ψ∈Φψ(cq)≥⨆↑f≪cq⊓ψ∈Φψ(f)=(⊓Φ)(cq)

Which establishes an upper bound. For a lower bound, we have, since p<q implies cp≪cq by Lemma 2,

(⊓Φ)(cq)=⨆↑f≪cq⊓ψ∈Φψ(f)≥⨆↑p<q⊓ψ∈Φψ(cp)=⨆↑p<qp=q

Now, for the [0,1] type signature, the only fiddly bit is the lower-bound argument, because maybe q<