**Lemma 7:** *For ** s.t. ** and **, and **, and ** is compact, LHC, and second-countable, then **. The same result holds for **.*

This is the only spot where we need that 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 and of a certain form, which exceed and . Then, of course, as a result. We'll then show that can be written as the supremum of finitely many functions in (or ) which all approximate , so , establishing that .

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 and . The only approximator functions you need to build any are step functions of the form with being a finite rational number, and being selected from the base of , and where is our compact hull operator. Any function of this form approximates , and taking arbitrary suprema of them, itself is produced.

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

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

and, by how our atomic step functions of the directed set associated with were built, we know that for all i, . (remember, the 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 type signature, and the type signature.

For the type signature, there's finitely many i, and everything not in the gets mapped to . Since , and is compact, is bounded below (Lemma 1), so for this finite supremum to exceed , the must cover .

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

So... Given that we have our , what does the function look like? Well, it looks like

We could do this in the case from adding in the "dummy" open sets to get the family and family to both cover .

Anyways, equals . 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 , if we can just show that all these atomic step functions are approximators for in (or ), then (supremum of finitely many approximators is an approximator), and we'd show our desired result that . So let's get started on showing that, regardless of and ,

Now, if , then this function maps everything to or 0, which trivially approximates . Otherwise, everything in gets mapped to , and everything not in it gets mapped to (or 0)

We know by our process of construction for this that and , so let's try to work with that. Well, for the case. The case is a bit more delicate since we added those two dummy functions. We have:

The first strict inequality was because of what and were. Then, just move the constants in. For the first non-strict inquality, it's because of monotonicity for our compact hull operator, , 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 , for each patch of you can find a function from your directed set that beats the value on that spot, this gets you an open cover of , 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 is approximated by the atomic step function" from Theorem 2 kicks in, to show that the atomic step function approximates . Since this works for arbitrary , and there are finitely many of these, the finite supremum approximates , and dominates , and we're done.

Now for the case. This case works perfectly fine if our pair has and being above 0. But what if our has being above 0, but our j index is picking that "dummy" approximator? Or vice-versa. Or maybe they're both the "dummy" approximator.

That last case can be disposed of, because 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 is paired with , but the other one is the "dummy" approximator. Then our goal is to show that . This can be done because, since , and , we have

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

**Lemma 8:** *If **, and **, then **, provided ** lies in the function space of interest. ** (or **), and ** 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, , as long as . Since , we can find finitely many atomic step functions which all approximate s.t. the function exceeds . In the case, since the finite supremum exceeds , which is bounded below by Lemma 1, the family covers .

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

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

And so, our result follows. It's possible that, for the case, lies in no , but then the supremum of the empty set would be 0, and since the supremum of the exceeds , as well, so the same inequality holds.

**Lemma 9:** *If ** and ** with ** with ** being compact, LHC, and second-countable, then **.*

We can invoke Theorem 2, to write any function as the supremum of atomic step functions below it, , as long as . Since , we can find finitely many atomic step functions which all approximate s.t. the function exceeds . Also, is bounded below by Lemma 1, so the finite family covers the entire space.

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

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

And so, our result follows.

**Lemma 10:** *If ** and ** with ** with ** being compact, LHC, and second-countable, then for all **, **, as long as ** is also bounded in **.*

By Theorem 2, we can always write any function as the supremum of atomic step functions below it, , where . Since , we can find finitely many atomic step functions which all approximate s.t. the function exceeds .

Now, consider the following finite finite collection of atomic step functions. , along with

If we can show that all of these approximate , and the supremum of them is larger than , then, since the supremum of finitely many approximators is an approximator, we'll have shown that , establishing approximation. So, let's show those.

For arbitrary , if , then we have

So these atomic step functions all approximate . If , then the atomic step function turns into , which also approximates .

For the one extra step function we're adding in, we have two possible cases. One is where , the other one is where . In such a case, the function turns into c_{0}, which trivially approximates . However, if , then we have

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

So, this finite collection of functions has its supremum being an approximator of . Now for showing that the supremum beats . If lies in some , then

And we've shown that this supremum of step functions beats our new function. If lies in none of the , then the original supremum of step functions must have mapped to 0, and that beats , so . 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 . The lemma then finishes up, we have that implies that for any and s.t. and and all lie in , we have

NOW we can begin proving our theorems!

**Theorem 4:** *The subset of ** (or **) consisting of inframeasures is an **-BC domain when ** 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 , or 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 -inframeasures (or -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 is infinity. Infinity plus any number in is infinity. Given two functions bounded below, then is the function which maps to , which is always continuous when are, due to being monotone, and preserving directed suprema. The distance between points in , for defining the distance between functions as 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 or with the following three properties.

should be 1-Lipschitz, it should map the constant-0 function 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 , we have that for any two functions, .

The definition of concavity is that, for all ,,

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 have a distance of infinity from each other, 1-Lipschitness is trivially fulfilled. So we can assume that have a finite distance from each other. Observe that it's impossible that (without loss of generality) is infinity, while is finite. This is because we have

So, if that first term is infinite, we can find which map arbitrarily high. And then would only be a constant away, so the values would climb arbitrarily high as well, making be infinite as well. Then we'd have

And this would also show 1-Lipschitzness. So now we arrive at our last case where 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 as an example)

So now, let's start working on the case where 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.

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 , so we can assume that this value is finite. It's also trivial if , 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 . Then, we can go:

Via Lemma 3. Now, at this point, we're going to need to invoke either Lemma 5 for the case, or Lemma 6 for the case. We'll treat the two cases identically by using the terminology . In the case, this is just , because the functions have a finite lower bound via compactness/Lemma 1, and we're in the assumed case where . In the case, it's , which is a different sort of function. Anyways, since we have , this then means that by Lemma 5 or 6 (as the type signature may be). So, swapping out the supremum over with choosing a and evaluating the , 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 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 has range in . In such a case, the latter term would turn into , so the contents as a whole of the absolute value would be . The second case is where has range in . In such a case, the latter term would be *as close or closer* to than , so we can upper-bound the contents of the absolute-value chunk by . In both cases, we have

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

Now for concavity. Concavity is trivial when or , so let's assume , 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 and and we have that by Lemma 7. Since all possible choices make an approximator for , we can go...

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 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 where , then . We'll be using that. Also we'll be using Lemma 4 that no 1-Lipschitz function mapping to 0 or higher can map a function any lower than , which is finite, by Lemma 1. So, we have

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

Now, since the space of inframeasures (concave, 1-Lipschitz, weakly-normalized) is closed under directed sup and arbitrary inf in and , 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 ** and **-inframeasures, if ** is compact, second-countable, and LHC.*

(supernormalization)

(homogenity)

(cohomogenity)

(C-additivity)

(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 type signature (where it's marginally easier), and done a second way for the case, where it's considerably more difficult to accomplish.

First, .

Second, .

Third, .

Fourth, , which is trivial from second and third.

Fifth, supernormalization.

Sixth, homogenity.

Seventh, cohomogenity.

Eighth, C-additivity.

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 case. We'll note when the same proof works for the case, and when we have to loop back later with a more sophisticated argument. Lemma 3 is used throughout.

First, preservation of under infinima. We already know that, by being preserved under arbitrary infinima it can't be *below* 0, so that leaves showing that it can't be *above* 0.

This was by monotonicity, since , and then we just apply that . This proof works for the type signature.

Second, preservation of under infinima. Since when 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 , applied concavity (value decreases), distributed the inf in (value decreases), used that always, and our assumption that (value decreases), and then we can finish up easily. Same proof works just as well for the type signature.

Third, preservation of under infinima. Since when by Lemma 2, we can go

(

Due to monotonicity. Same proof works for the type signature.

Fourth, preservation of under infinima. This is trivial since we proved preservation of and under infinima already, for both type signatures.

For 5, supernormalization is that for all numbers in or respectively. We'll show this is preserved under infinima. We have to prove both directions of this separately. In one direction, we have

Which establishes an upper bound. For a lower bound, we have, since implies by Lemma 2,

Now, for the type signature, the only fiddly bit is the lower-bound argument, because maybe . In that case, you can just apply the fact that is preserved under infinima, which we proved already.

Number 6: Homogenity, that for any , . We only need to check , because for , it's saying that