Crossposted from the AI Alignment Forum. May contain more technical jargon than usual.

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