Infra-Domain proofs 1

by Diffractor23 min read28th Mar 2021No comments


Domain TheoryWorld ModelingAI


A quick note here is that whenever a proposition or theorem or something is cited with a complicated-looking number, like, not Proposition 3, but "Proposition", it's being cited from this book.

Proposition 2: If X is a metrizable space, then the pointwise limit of a sequence of lower-bounded lower-semicontinuous functions  with  is lower-bounded and lower-semicontinuous.

Proof: Lower-boundedness of (the pointwise limit of the ) is trivial because , and  is lower-bounded. For lower-semicontinuity, let  limit to , and  be some arbitrary natural number. We have

Because  and  is lower-semicontinuous. And, since this works regardless of , we have

Since  is the pointwise limit of the , showing that  is lower-semicontinuous.


Proposition 3: If  is a metrizable space, then given any lower-bounded lower-semicontinuous function , there exists a sequence of bounded continuous functions  s.t.  and the  limit pointwise to .

First, fix  with an arbitrary metric, and stipulate that  is lower-bounded and lower-semicontinuous. We'll be defining some helper functions for this proof. Our first one is the  family, defined as follows for :

Ie, we take a point, and map it to the worst-case value according to  produced in an open ball of size  around said point. Obviously, regardless of .

Now we must show that , regardless of , is upper-semicontinuous, for later use. Let  be arbitrary, and  be some arbitrary point in , and  be some sequence limiting to . Our task is to show , that's upper-semicontinuity.

First, we observe that there must exist an  s.t. , and . Why? Well,  is "what's the worst-case value of  in the -sized open ball", and said worst-case value may not be exactly attained, but we should be able to find points in said open ball which get arbitrarily close to the infinimum or attain it.

Now, since  converges to , there must be some  where, forever afterward,  (the latter term is always nonzero from how we selected ). For any  in that tail, we can rearrange this and get that , so by the triangle inequality, we have that . Ie,  is in the open ball around  for the tail of the convergent sequence.

Now, since  is in all those open balls, the definition of  means that for our tail of sufficiently late , and we already know that . Putting these together, for all sufficiently late  was arbitrary, so we have

(the limit might not exist, but limsup always does). And now we know that our  auxiliary functions are upper-semicontinuous.

Next up: We must show that, if  is some continuous function,  is upper-semicontinuous. For this, we do:

For this, we distributed the limsup inside the sup, used that  is continuous, and then used that  is upper-semicontinuous for the inequality.

Now, here's what we're going to do. We're going to inductively define the continuous  as follows. Abbreviate  (which is finite) as , and then consider the set-valued functions, for  inductively defined as follows:

where  is a continuous selection from .

The big unknown is whether we can even find a continuous selection from all these set-valued functions to have the induction work. However, assuming that part works out, we can easily clean up the rest of the proof. So let's begin.

We'll be applying the Michael Selection Theorem.  is a Banach space, and  being metrizable implies that  is paracompact, so those conditions are taken care of. We need to show that, for all  and  is nonempty, closed, and convex, and  is lower-hemicontinuous. This will be done by induction, we'll show it for , establish some inequalities, and use induction to keep going.

For , remember, 

This is obviously nonempty, closed, and convex for all . That just leaves establishing lower-hemicontinuity. Lower-hemicontinuity is, if , and there's a sequence  limiting to , there's a (sub)sequence  that limits to . We can let our . Since , so 

So it's an appropriate sequence to pick. Now, we can go:


The first equality was distributing the liminf in and neglecting it for constants, the second is because  because , and the inequality is from lower-semicontinuity of , and the equality is because  so .

Since the limsup of this sequence is below  and the liminf is above , we have:

And bam, lower-hemicontinuity is proved for the base case, we can get off the ground with the Michael selection theorem picking our .

Now for the induction step. The stuff we'll be assuming for our induction step is that  (we have this from the base case), and that  is continuous (we have this from the base case). Now,

Because  by induction assumption, and , because the definition of  was

we have nonemptiness, and closure and convexity are obvious, so we just need to verify lower-hemicontinuity. Lower-hemicontinuity is, if , and there's a sequence  limiting to , there's a (sub)sequence  that limits to . We can define


And also,

because  and , by our induction assumption and definition of  respectively. Then, we can observe that because

we have

and also we have

so we have

Putting all this together, our net result is that

Combining this with previous results (because the later term is an upper-bound to our  when unpacked), we have:

putting the upper and lower bounds together, we have:

So it's an appropriate sequence of  to pick. I will reiterate that, since  is continuous (induction assumption) and we already established that all the  are upper-semicontinuous, and the sup of a continuous function and upper-semicontinuous function is upper-semicontinuous as I've shown, we have upper-semicontinuity for . Remember that. Now, we can go:

Up to this point, what we did is move the limsup into the max for the equality, and then swapped our min of three components for one of the components (the ), producing a higher value.

Now, we can split into two exhaustive cases. Our first possible case is one where . In such a case, we can go:

This occurred because we swapped out our min of two components for one of the components, the constant lower bound, producing a higher value. Then, the equality was because, by assumption,  so we can alter the second term. Then, we finally observe that because , and  is the lower-bound on said set,  is the larger of the two.

Our second possible case is one where . In such a case, we can go:

The first inequality was we swapped out our min of two components for one of the components, producing a higher value regardless of the . The second inequality was because  is upper-semicontinuous, as established before. The equality then is just because we're in the case where . Finally, we just observe that the latter term is the lower-bound for , which is the set that  lies in, so  is greater. These cases were exhaustive, so we have a net result that

Now for the other direction.

The first inequality was swapping out the max for just one of the components, as that reduces the value of your liminf. Then, for the equality, we just distribute the liminf in, and neglect it on the constants. The next inequality after that is lower-semicontinuity of , then we just regroup the mins in a different way. Finally, we observe that  is the upper-bound on , which  lies in, so  is lower and takes over the min.

Since the limsup of this sequence is below  and the liminf is above , we have:

And we've shown lower-hemicontinuity, and the Michael selection theorem takes over from there, yielding a continuous . Now, let's verify the following facts in order to show A: that the induction proceeds all the way up, and B: that the induction produces a sequence of functions  fulfilling the following properties.

First: . This is doable by , from our  upper bound. It holds for our base case as well, since the upper bound there was .

Second: , which is doable by the exact same sort of argument as our first property.

Third: . This is doable by

Where the inequality uses that  is a selection of , and the lower bound on . Then we just swap out some contents for lower contents, and use our second fact which inducts up the tower to establish that  is an upper bound on the function . This is our one missing piece to show that our induction proceeds through all the .

Fourth: . Same argument as before, except we swap  out for  instead.

At this point, we've built a sequence of continuous functions  where you always have , and  and , regardless of .

Our last step is to show that  limits to  pointwise, ie, regardless of .

We recall that the definition of  was 

Obviously, as  goes up,  goes up, it's monotonically increasing, since we're minimizing over fewer and fewer points each time, the open ball is shrinking. So the limit exists. And we also know that all the  lie below . So, to show that  limits to  pointwise, we just have to rule out the case where .

Assume this was the case. Then, for each  we can pick a point  only  distance away from  that comes extremely close to attaining the infinimum value. These  get closer and closer to , they limit to it. So, we'd have:

But the definition of lower-semicontinuity is that

So we have a contradiction, and this can't be the case. Thus, the  limit to  pointwise.

Now, we will attempt to show that the  limit to  pointwise. Let  be arbitrary, and we have

The first inequality was  for all , the equality was just a reindexing, and the second inequality was  (from our induction). Now, we can split into two cases. In case 1,  diverges to . Since  diverges as well, we have

In case 2,  doesn't diverge, but since  does, we have

So, in either case, we can continue by

Because the  limit to  pointwise. Wait, we just showed  no matter what. So all the inequalities must be equalities, and we have

And now we have our result, that any lower-bounded lower-semicontinuous function  can be written as the pointwise limit of an increasing sequence of bounded continuous functions (since all the  were bounded above by some constant and bounded below by .)


Theorem 1/Monotone Convergence Theorem For Inframeasures: Given  a Polish space,  an inframeasure set over  a lower-bounded lower-semicontinuous function , and  an ascending sequence of lower-bounded lower-semicontinuous functions  which limit pointwise to , then 

We'll need to do a bit of lemma setup first. Said intermediate result is that, if some  is lower-semicontinuous and lower-bounded, then the function from a-measures to  given by  is lower-semicontinuous.

By Proposition 3, we can craft an ascending sequence  of bounded continuous functions which limit pointwise to .

Now to establish lower-semicontinuity of . Let  limit to . Let  be arbitrary. Then

The first inequality is because  is above the  sequence that limit to it. We then use limits because the sequence converges now. Since  is continuous and bounded, and  converges to , then  must converge to .

Anyways, now that we know that for arbitrary 

We can get the inequality that

Where the equality comes from Beppo Levi's monotone convergence theorem, since the  sequence is an ascending sequence of lower-bounded functions. Accordingly, we now know that if  is lower-bounded and lower-semicontinuous, then  is a lower-semicontinuous function. Let's proceed.

Remember, the thing we're trying to show is that

Where all the  are lower-semicontinuous and lower-bounded, and limit to  pointwise. One direction of this is pretty easy to show.

The first equality is just unpacking what expectation means, then we use that  regardless of  to show that all the points in  are like "yup, the value increased" to get the inequality. Then we just observe that it doesn't depend on n anymore and pack up the expectation, yielding

So, that's pretty easy to show. The reverse direction, that 

is much trickier to show.

We'll start with splitting into cases. The first case is that  is the empty set, in which case, everything is infinity, and the reverse inequality holds and we're done. 

The second case is that  isn't empty. In such a case, for each , we can pick  a-measures from the minimal points of  s.t.

coming as close to minimizing said functions within  as we like!

Now, we can again split into two cases from here. In our first case, the  sequence from the  sequence diverges. Then, in such a case, we have

Why does this work? Well, the  approximately minimize the expectation value of . Then, the worst-case value of  is either 0, or the amount of measure in  times the lowest value of . Since it's an ascending sequence of functions, we can lower-bound this by (amount of measure in ) times (worst-case value of ). And, since we're picking minimal points, and there's an upper bound on the amount of measure present in minimal points of an inframeausure set from the Lipschitz criterion (our finite  value), the worst-case value we could possibly get for  is either 0 or the maximum amount of measure possible times a lower bound on . Both of these quantities are finite, so we get a finite negative number. But the  are assumed to diverge, so the expectation values head off to infinity.

Ok then, we're on to our last case. What if  isn't empty, and our sequence  of a-measures has a subsequence where the  doesn't diverge? Well, the only possible way a sequence of a-measures in a nonempty inframeasure set can fail to have a convergent subsequence is for the b values to diverge, from the compact-projection property for an inframeasure set.

So, in our last case, we can isolate a convergent subsequence of our  sequence of a-measures, which converges to the a-measure . Let's use the index  to denote this subsequence. At this point, the argument proceeds as follows. Let  be an arbitrary natural number.

In order, this is just "we went to a subsequence of an ascending sequence, so it's got the same limit", then swapping out the worst-case value for the actual minimizing point. Then we just use that since the sequence of functions is ascending, eventually  will blow past  (at timestep ) because  is a fixed constant. Then we just apply that  is lower-bounded and lower-semicontinuous, so the function  is lower-semicontinuous, getting our inequality we pass to .

Since this holds for arbitrary j, this then means we have

And then we can go

And we have the inequality going the other way, proving our result! This last stretch was done via Beppo Levi's Monotone Convergence Theorem for the equality, then the inequality is because nonempty inframeasure sets  are closed, so the limit point  also lies in , and then packing up definitions.

Since we've proven both directions of the inequality, we have

and we're done!


Proposition 4: All compact Polish spaces are compact second-countable LHC spaces.

Proof: Compactness is obvious. All Polish spaces are second-countable. So that just leaves the LHC property. Our compact hull operator  will be taken to just be the closure of the set. Since the space  is compact, all closed subsets of it are compact as well. The two properties

Are trivially fulfilled when  is interpreted as set closure.

That leaves the LHC property. Since all Polish spaces are Hausdorff, the various definitions of local compactness coincide, and the space is compact, so all definitions of local compactness hold. So, given some  and , by local compactness for the space , we can find a compact set  and open set  s.t. . Since  is open, it can be written as a union of sets from the topology base. Now, pick a set from the base that makes  and contains , call it . We have . In Hausdorff spaces, all compact sets are closed, so  is a closed superset of , and so  (the closure of ) is a subset of . Since , and  (since  is just closure), we have , as desired. This works for any  and , so the space fulfills the LHC property.


Proposition 5: All open subsets of -BC domains are second-countable LHC spaces.

Given , an -BC domain, it has a countable basis. You can close the countable basis under finite suprema (when they exist), and the set will stay countable and stay a basis, but now it's closed under finite suprema. Do that, to get a countable basis  which is closed under finite suprema.

Our attempted base for the open subset  will be those of the form  for , ie, the set of all the points  where , and  is in the countable basis for the domain and also in . Also the empty set. This is clearly countable, because  is.

To show it's a topology base, we need to check closure under finite intersection, check that all these are open, and check that every open set in  can be made by unioning these things together.

First, closure under finite intersection. In order to do this, we'll need to show a lemma that if  for finitely many , then . This occurs because, given any directed set with a supremum of  or higher, since , you can find a  in the directed set which is above , and then take an upper bound for the finitely many  which exists within your directed set, and it'll exceed . So, every directed set with a supremum of  or higher has an element which matches or exceeds the supremum of the , so the supremum of the  approximates .

Now that we have this result, we'll show that 

In the two directions, anything which is approximated by  is also approximated by anything below it, ie, all the , so we have 

And, for the reverse direction, we've already established that anything which all the  approximate will also have the supremum of the  approximate it. Since our countable basis  was made to be closed under finite suprema, the open set associated with the supremum of the  is also in our basis, so our base is closed under finite intersection.

Second, checking that they're open. Sets of the form  are always open in the Scott-topology, and every Scott-open set is closed upwards, so all the sets in this base are open in the original domain , and so remain open when we restrict to the open subset of  and equip it with the subspace topology.

All that remain to show that this is a base is that it can make any Scott-open subset of  by union. By Proposition, a set  is open in the Scott-topology on  iff .

Since all of our open subsets of  are open in , they can be written as a union of sets from our countable collection by this result.

We have crafted a countable base for our open subset of an -BC domain , so it's indeed second-countable.

Now for the LHC property. The compact hull operator  maps the set  to . This is compact because all Scott-opens are closed upwards, so an open cover of  must have an open which includes  itself, and this single open covers the entire set. This set is a subset of  because everything that  approximates lies above , so  is a lower bound, and thus must equal or lie below . Since  is in our open subset , the same must also apply to this lower bound, because Scott-open sets are closed up.

For our first property of a compact hull operator, we need to show that . This is easy, anything which lies in  must lie above the infinimum of that set.

For our second property of a compact hull operator, we need to show that  implies . For this, assuming the starting assumption, by basic properties of inf, we have , so then anything above that first point must also be above the second point, so we have our result.

Now, we just need to check the LHC property. Let  be an open subset of , and let . We can consider the directed set of approximants to  from the basis of our domain , called . Scott-opens have the feature that for any directed set with a supremum in the open set (and  is directed and has a supremum of , which lies in ), there's an element in the directed set which also lies in the open set. So, we can find a  which lies in the basis, and , and . Then just let your open set from the base be . This is an open from the base. It contains . And, , because  and Scott-opens are closed upwards.

And thus, our result is shown.


Corollary 1: All -BC domains are compact second-countable LHC spaces.

Just use Proposition 5 when your open set is all of your domain to get second-countability and LHC-ness. For compactness, any open cover of the domain  must have an open set which includes the bottom point , and Scott-opens are closed upwards, so we can isolate a particular open set which covers the entire domain.


Theorem 2: If  is second-countable and locally compact, then  is an -BC domain, as is .

To begin,  is topologically identical to , so we can just prove it for the  case to get both results.

As a recap, the Scott-topology on  is the topology with the open sets being ,, and all sets of the form  for 

The space  is the space of all continuous functions , where  is equipped with the Scott-topology, which has been equipped with a partial order via 

We will actually show a stronger result, that this space is a continuous complete lattice with a countable basis, as this implies that the set is an -BC domain.

To show this, we'll need to show that the space is closed under arbitrary suprema. This is sufficient to show that the space is a complete lattice because, to get the infinimum of the empty set, we can get a top element by taking the supremum of everything, and to get the infinimum of any nonempty set of elements, we can take the set of lower bounds (which is nonempty because a bottom element exists, the supremum of the empty set), and take supremum of that. Then we just need to find a countable basis, and we'll be done. Most of the difficulty is in finding the countable basis for the function space.

Showing there's a bottom element (sup of the empty set) is easy, just consider the function which maps everything in  to 0.

Now, we'll show that suprema exist for all nonempty sets of functions. Let  be our nonempty set of functions.

The natural candidate for the supremum of functions is is , call this function . It's a least upper bound of all the functions , the only fiddly part we need to show is that this function is a continuous function , in order for it to appear in the space .

Fix an arbitrary open set in , we'll show that the preimage is open in . If the set is the empty set or  itself, then the preimage will be the empty set or all of , so those two cases are taken care of. Otherwise, the open set is of the form  for . Now, we have

And now we see that this preimage can be written as a union of preimages of open sets, which are open since all the  are continuous, so the set  is open. Since  was arbitrary in , we have that the preimage of all open sets in the unit interval is open in , so  is indeed continuous and exists in , to serve as the least upper bound there.

All that remains is coming up with a countable basis for , which is the hard part. Let  be a countable base of  (this can be done since  is second-countable). Given an open set  and rational number , we define the atomic step function  as:

First things first is showing these are continuous. Clearly, any preimage will either be the empty set, all of , or the open set  (because there's no open set in  with the Scott-topology that contains 0 without containing ), so they're indeed continuous.

Our attempted countable basis  will be all of these atomic step functions, and all finite suprema of such. Suprema of arbitrary sets of functions always exist as we've shown, so this is well-defined. It's countable because there's countably many choices of open set, countably many choices of rational number, and we're considering only the finite subsets of this countable set.

The hard part is showing that for any , it can be built as the supremum of stuff from this basis which approximates . First up, as a preliminary, is showing that  is a directed set for some arbitrary function  is the set of all elements of the basis which approximate . What we can do is pick two arbitrary functions from the basis,  and  s.t.  and . From back in Proposition 5, we know that . Since our basis is closed under finite suprema, we now know that the intersection of the basis and the approximants to  is closed under finite suprema, so it's directed.

So, now that we know that  is a directed set for arbitrary , we must ask, does ? For one direction, we have that every function in  approximates , so it must be less than  itself, so we have  trivially. So let's get the other direction going, by showing 

First, let's solve the case where . We'd have 

Now we can assume that . We now have

The inequality is because now we're restricting to the atomic step functions instead of all the suprema of such. And then we have

Why is this? Well,  is 0 if , and  if . So, if, for a rational number , we can find an open set  s.t. , and , then the supremum of atomic step functions must map  to  or higher. And if there's an atomic step function which approximates  and maps  to some , we can read out the open set from it to certify that  lies in the latter set of rational numbers we're taking the supremum over.

Our proof target will be to show that