Attention conservation notice: This post has Less Basic Inframeasure Theory as a prerequisite and goes pretty heavy on the topology.
The basic results are that a whole lot of the fiddly details involved with having inframeasures over non-compact spaces automatically pop out of just trying to make everything continuous, and that some of the old results in LBIT are either wrong or about the wrong topology. Accordingly, this post completely obsoletes the section about topology of inframeasures in Less Basic Inframeasure Theory
For the rest of this post, assume is a Polish space. Basically, a Polish space is a space that has a metric, all Cauchy sequences have limiting points (like and unlike ), and there's a countable subset of it s.t. every point can be written as a limit of points from the countable subset ( is the corresponding countable subset of ).
Proofs available on request because they're 115 pages and this post was 15 pages.
Topologies and Convergence Notions
The first observation to make is that the type signature of an inframeasure over the space (or, one of the possible type signatures) is , where is the space of bounded continuous functions . You feed a function in, you get an expectation out, simple as that.
So, an extremely natural requirement to impose is that an inframeasure should be a continuous function. The topology on is obvious. The topology on , the space of continuous bounded functions , is much less obvious.
Another observation is that different notions of function convergence correspond to different topologies on function spaces.
You could say that converges to if limits to 0. This is uniform convergence, The late are close to everywhere, the rate of convergence doesn't depend on anything.
Or you could say that converges to if, for all x, limits to 0. That's pointwise convergence, for every point, the late are close to at that point. The rate of convergence depends on the point you picked.
Or you could say that converges to if, for all compact sets , we have limiting to 0. This is compact convergence. For every compact set, the late are close to on that compact set. The rate of convergence depends on the compact set you picked.
All these different notions of function convergence are linked to different topologies on . The sup-norm topology, the weak topology, and the compact-open topology, respectively, for uniform convergence, pointwise convergence, and compact convergence.
So, what notion of convergence seems to "naturally" show up in a lot of proofs? Does it seem like we're using uniform convergence, pointwise convergence, or something like that? No. The notion of convergence that has showed up basically every single time while grinding through the inframeasure theory has been the following notion of convergence.
Definition 1: Strict Convergence A sequence of bounded continuous functions strictly converges to if, for all compact sets , , and
So, basically, strict convergence is uniform convergence on compact sets, along with the entire function sequence having some uniform upper and lower bounds.
What's the motivation for this? Well, there's a few ways to do it, but here's a nice one. Let's say we want to be a sequentially continuous function. Ie, if the sequence of probability distributions converges to , and converges to , the expectation of w.r.t. should converge to the expectation of w.r.t. . This requires two questions. First, what does it mean for to converge to , and what does it mean to say that converges to ?
Well, the notion of convergence on is known, it's weak convergence, that's the sort of convergence we've been using this whole time. converges to iff, for all continuous functions , limits to .
So then the question is, "in what sense does have to converge to in order to make sequentially continuous?", and the answer is strict convergence exactly. Strict convergence means that becomes sequentially continuous, and if does not strictly converge to , then it's always possible to craft a convergent sequence of measures that makes fail.
But remember, every notion of convergence corresponds to some natural topology. So, if uniform convergence corresponds to the sup-norm topology, and pointwise convergence corresponds to the weak topology, and compact convergence corresponds to the compact-open topology, what does strict convergence correspond to?
Well, it corresponds to the strict topology on , which is a topology you've almost certainly never heard of. It's a pretty obscure choice. The maximally concise description of it is that it's the finest locally convex topology on that matches the compact-open topology on all norm-bounded subsets of .
Or, putting it a bit more intuitively, it's a nice enough topology to get basic stuff like the Hahn-Banach theorem working, and it locally looks like the compact-open topology, but if you zoom out to a global scale, it has more open sets.
Proposition 1: A sequence converges to in the strict topology iff and uniformly converges to on all compact subsets.
Good, we got the right topology.
The massive problem we have to deal with now, is that equipped with the strict topology is a pretty badly behaved space, topologically speaking. I mean, it's still Hausdorff (and more), that's a nice thing going for it. The bigger problem is that it's such a big space that it's not even first countable. Even worse than that, I don't even think it's a sequential space! Ie, "take a set, and add in all the limit points of sequences made from inside that set" might not be the same thing as topological closure. It even seems like it's possible to have functions that *look continuous, in the "if strictly converges to , then converges to " sense, but that actually aren't continuous! And I don't even know any of this for sure because it's a pretty hard sort of topology to prove things of.
However, through entirely too much scouring of obscure functional analysis papers from the 80's, I was eventually able to prove
Proposition 2: A set is sequentially compact in the strict topology iff it's compact in the strict topology.
So, we at least have "every open cover has a finite subcover" matching up with "every sequence has a convergent subsequence". It's rather surprising for this result to hold when our space isn't even first-countable, and closure and sequential closure might split apart, but it's quite handy, because it lets us speak of just "compact sets of functions" without disambiguating further.
Scott and Antiscott
Now, we'll cover something else, the Scott topology on . It's relevant because domain theory (the field of math that analyzes what sort of topological spaces Haskell types are) really really really likes the Scott topology. And there are unexpectedly many connections between inframeasures and domain theory, so it's worthwhile to have some basic familiarity with it.
Here's how the Scott-topology is defined. Given a poset , a subset is "upwards directed" if, for any two points , there's a third point s.t. and . Similarly, is downwards directed if, for any two points , there's a third point in the directed set that's below the first two points.
Definition 2: Scott-Open A set is open in the Scott topology iff
1: It's closed upwards. , and implies .
2: It's "inaccessible from below" with upwards directed sets. If there's an upwards-directed set where (the supremum of ) exists, and , then .
Closed upwards is pretty intuitive. For that second condition, it's just like the fact that, if you've got a sequence of numbers in that keep getting higher and higher, , and , then one of the in your chain must also be greater than . In fact, sets of the form are precisely the Scott-open subsets of . They're closed upwards, and any chain with a supremum that lands in that set must have an element of the chain land in the set already. Just generalize further, chains are a special case of directed sets. If the supremum lands in a Scott-open, one of the points "building up to" the supremum must land in the Scott-open too. And conversely, the supremum of a directed set of points from outside of a Scott-open also can't land in the Scott-open either.
And that's the Scott-topology! It's the topology of building stuff up from below, and has shown up... more than I expected at first.
But... the situation seems pretty symmetric with functions. Could we make a topology that "goes the other way"? Well, I don't know the official name for it, so I'll make one up. The Antiscott topology.
Definition 3: Antiscott-Open A set is open in the Antiscott topology iff
1: It's closed downwards. , and implies .
2: It's "inaccessible from above" with downward directed sets. If there's a downwards directed set where (the infinimum of ) exists, and , then .
It's basically the same thing, but with the direction flipped. Scott-opens are closed upwards, Antiscott-opens are closed downwards. Upwards-directed sets with a supremum in a Scott-open must intersect the Scott-open. Downwards-directed sets with an infinimum in an Antiscott-open must intersect the Antiscott-open.
This may seem like idle goofing around, but there's an unexpected connection to be made here.
Theorem 1: The strict topology on is the topology generated by the Scott topology and the Antiscott topology.
Ie, if you made a topology that was like "let's make a topology where all the Scott-open sets are open, and all the Antiscott-open sets are open, just close under finite intersections and arbitrary unions... Huh. That's the strict topology exactly."
The simplest way to visualize what's going on with this is that the Scott-open subsets of are the sets of the form , and the Antiscott-open subsets of are the sets of the form , and if you went "ok, let's say both of these families of sets are open", then you'd end up saying that all the open intervals are open, and bam, you'd get the usual topology on that way.
The interesting part is that it feels like this is the tip of a much more general result. It holds for function spaces, the appropriate topology on them to be using is generated by the Scott and Antiscott topologies. It holds for , the appropriate topology on it is generated by the Scott and Antiscott topologies. But this sort of pattern even shows up in weirder places. As it turns out, the canonical topology on inframeasures is, you guessed it, generated by the Scott and Antiscott topologies. And even with, like, , the space of compact subsets of , the topology on it (the Vietoris topology) is generated by an upper and lower topology that look an awful lot like Scott and Antiscott.
Part of why Theorem 1 is nifty is that, going back to our old desiderata of "inframeasures should be continuous", this result (along with some more work) means that we can split the statement " is continuous" into " is Scott-continuous" (ie, continuous when and both have the Scott topology), and " is Antiscott-continuous" (ie, continuous when and both have the Antiscott topology), and both of these fragments of continuity are saying somewhat different things!
To motivate some of why it's interesting that continuity splits up this way, let's reiterate the basic four properties of an inframeasure . These aren't all of them, just the easiest ones to check.
2: Monotonicity. implies .
And now we can get something pretty interesting. If your space is , then the function of type fulfills all four of these properties. And then you can go "ok, by LF-duality, this functional must correspond to minimizing over some set of a-measures, let's work that out, the set of a-measures is....
oh crap, something went very wrong somewhere"
As it turns out, when I proved LF-duality (the theorem about the ability to toggle back and forth between a view where an inframeasure is a concave function fulfilling certain properties, and the view where an inframeasure is a set of a-measures), I was kinda sloppy with it. I didn't realize that had to be equipped with the strict topology. At the time, I hadn't even heard of the strict topology at all. So I was using the wrong topology. And that broke the proof, the Fundamental Theorem of Inframeasures.
The key thing that went wrong is that applying the Hahn-Banach separation theorem requires that you verify that some sets are open, or closed, or compact, or whatever. But since we should be using the strict topology instead of one of the more obvious topologies, I had to be verifying open/closed/compact in the strict topology, which is... quite the ordeal.
Don't worry, it got fixed. As it turns out, the missing piece was Antiscott-continuity!!
Theorem 2, LF-duality: A concave monotone 0-increasing 1-Lipschitz functional has a representation as a set of a-measures iff it's Antiscott-continuous.
And sure enough, when we check our example that fulfills the other four conditions, it fails to be Antiscott-continuous. You can have be 0 for the numbers 0 through n, and 1 everywhere else. This is a descending chain of functions with the constant-0 function as its inf. And yet, all the are assigned a value of 1, while the constant-0 function is assigned a value of 0, breaking Antiscott-continuity.
And what about Scott-continuity? That one seems pretty important, remember that in "Inframeasures and Domain Theory", Scott-continuity was part of the definition of an inframeasure. Well... while Antiscott-continuity is intuitively saying "you can represent your functional as a set of a-measures at all", Scott-continuity is intuitively saying "the set of a-measures your function is represented as is a "small" set, in the sense of being "almost compact"".
For the next theorem, some explanation.
The -CAS property of an inframeasure is: For all , there is a compact set s.t, for any two functions with (and same for ) that agree on the set , we have . Or, as an equation, Pretty much, this is saying that "only compact sets are relevant to assessing expectations of functions", in a certain precise sense. Namely, that for any tolerance and norm bound you want, you can find a compact set where the expectation value assigned to a function fitting the norm bound is almost entirely determined by how the function behaves on the compact set. Changing the function behavior outside the compact set has little effect. CAS stands for "compact almost-support".
A strengthened version of this, which didn't have the dependence on (I didn't know I needed it at the time, it would have looked like an unmotivated hack) was one of our inframeasure conditions in Less Basic Inframeasure Theory. It seems rather complex, but it's the generalization of the analogous fact for probability distributions where there are compact sets containing arbitrarily much of the measure. Except in this case you've also gotta throw in some overall function bounds, and the analogue of "low measure outside the set" is "functions acting differently outside the set has a small effect on expectations".
Next thing of note: Sequential strict continuity of a function is "if strictly converges to , then converges to ". Strict continuity (a harder condition to fulfill) is the full "the preimage of an open set in is open in equipped with the strict topology" definition of continuity.
And one last note: For an inframeasure , is the corresponding set of a-measures, is the set of minimal points in , and "precompact" is "if you took the closure of the set, it'd be a compact set".
Oh, also, remember, by the last theorem, "representability" (ie, corresponds to minimizing over a set of a-measures) is the same thing as Antiscott-continuity.
Now we're ready.
Theorem 3: CC Theorem The following five properties are equivalent for a function which is monotone, concave, 1-Lipschitz, and 0-increasing.
1: The -CAS property.
2: Representability and Scott-continuity.
3: Strict continuity.
4: Representability and sequential strict continuity.
5: Representability and, for all , is precompact in the weak topology on measures.
CC stands for Continuity-Compactness here. The Continuity-Compactness theorem.
So, just going "the function should be continuous" ends up being equivalent to the super-complicated condition about compact sets that we made up when going to Polish spaces. And it also splits into two sorts of continuity, Antiscott and Scott, where Antiscott lets you represent the function as a set of a-measures at all, and Scott ensures that the set is "small", in the sense that if you chopped off your set of a-measures past any given value, the essential/minimal a-measures would basically be a compact set.
So, all the weird extra conditions, like Scott-continuity, and he compact-set property, and looking compact when the set of a-measures is cut off below any particular bound, are all equivalent to/flow out of mere continuity!
Quick little note. isn't the only possible type signature for inframeasures, another option is , where all the functions and expectation values are bounded in . All the other theorems still work (including the "representable iff Antiscott" one), but for the five-way equivalence, some of the equivalences end up breaking. Conditions 2 and 3 are still equivalent in the case, though.
Ok, so we got the topology on the space of continuous functions sorted out, and showed that when you do that it lets you repair the previously-broken Fundamental Theorem of Inframeasures (LF-duality), and characterized all the fiddly extra conditions you have to add when you go to non-compact spaces as just "it's continuous, lol".
And so, we can define an inframeasure on a Polish space , this obsoletes the definition from Less Basic Inframeasure Theory.
Definition 4: Inframeasure A function (or ) is an inframeasure if it fulfills
2: Monotonicity. implies .
5: Continuity when (or ) has the strict topology.
An important thing to note here is that we're adding in one extra inframeasure via these conditions. It's , the inframeasure that maps every function to . By LF-duality, it corresponds to the empty set. It actually ends up making things a bit nicer, it basically acts as a "point at infinity" and makes it so intersection of inframeasures is always defined.
What topology should the space of inframeasures have?
Well, we've got a few options.
The first option is that inframeasures have an ordering, so we could try Scott+Antiscott.
The second option is that, since the type signature is , that's a function space. Function spaces are usually equipped with the compact-open topology, so we could go with that one. The compact-open topology is the topology generated by declaring the following family of sets to all be open Where is a (strictly) compact subset of , and is an open subset of .
The third option is coming up with some sort of nice metric. Previously, in "Less Basic Inframeasure Theory", we proposed the metric Where is the Lipschitz constant of (assumed to be infinite if isn't Lipschitz), and is the norm of , ie . Basically, this metric says that two inframeasures are close if they agree pretty well on all the functions with low Lipschitz constant and low norm. This is a generalization of the KR-distance metric on probability distributions, and is equivalent to Hausdorff distance between the corresponding sets of a-measures for the two inframeasures.
As it turns out, this isn't quite the right metric. The right metric is Which we'll call the IKR metric. The "squared" isn't too important, the important part is that it be a power greater than 1. Pretty much, it's the same as our last stab at defining a metric, except it's more aggressive at discounting functions with a high norm.
This is a decent distance metric in all respects, except it doesn't deal too well with the inframeasure at infinity, .
Accordingly, the IKR-topology is defined as the topology generated by all the open balls induced by the IKR-metric, and also by the sets of the form For . These are the neighborhoods of infinity.
Proposition 3: The compact-open topology on the space of inframeasures and the IKR-topology on the space of inframeasures are identical.
Hm! That's a sign we're on the right track! It means that equipping the space of inframeasures with the obvious topology (compact-open) makes the same thing as trying to generalize the distance metric on probability distributions to the case of inframeasures (they're close if they nearly agree on low-Lipschitz-constant functions of low norm), and tweaking it a little bit.
From now on, we'll call this the I-topology. The infra-topology, the appropriate topology to equip the space of inframeasures with.
If you're wondering whatever happened to the Scott+Antiscott idea, I didn't bother proving it, but I'm >95 percent sure it's true because I worked out what the Scott topology on inframeasures looks like, and it's "half of the I-topology" in a sense that looks identical to how the Scott topology on functions looked like "half of the strict topology".
And now, we'll come to one of our major centerpiece theorems. Four very different charaterizations of when inframeasures converge.
The first possibility is that you could say that limits to iff, for all strictly convergent sequences of functions , we have . Basically, inframeasures converge however they need to to make a sequentially continuous function.
The second possibility is that you could say that limits to iff, for all compact sets of functions , uniformly limits to on . This is basically replicating our "functions must uniformly converge on compact sets" thing, but for inframeasures instead of functions.
The third possibility is that you could say that limits to iff limits to in the compact-open topology (ie, the I-topology).
And the fourth possibility is limits to iff it does so in IKR-distance.
So, there's a sequential-continuity-based way of describing convergence, a uniform-convergence-on-compact-sets way of describing convergence, a converge-in-the-obvious-topology way of describing convergence, and a metric-based way of describing convergence.
Modulo some fiddly complications with what it means to converge to , the all-infinity inframeasure, we get that they're all the same!!
Theorem 4: The Convergence Theorem The following four characterizations of inframeasure convergence are identical.
1: For all sequences that strictly limit to , limits to .
2:For all compact sets (in the strict topology on ), uniformly limits to on (if is the all-infinity function, limiting to infinity will be taken as uniform convergence to infinity)
3: limits to in the compact-open topology.
4: limits to in the IKR-metric, or and limits to .
So, all these different notions of convergence are all the same, this is pointing to us having figured out the correct thing. Oh, and this theorem works equally well in the type signature case.
A big goal is to show that if is a Polish space, then is a Polish space too. Ie, spaces of inframeasures are about as nice as the space they're defined over. And...
Theorem 5: The space of inframeasures equipped with the I-topology is a Polish space.
Stuff goes wonky with the -type-signature case, I'm not sure whether or not the space of -inframeasures is still Polish. I mean, the convergence theorem still holds, but the argument that the limit of a Cauchy sequence of inframeasures is an inframeasure relies on some arguments I can't pull off in the case.
We might ask if there's some nice properties we can impose to prove Polishness in the case, and it turns out there is! It's one of our most common "nice properties", cohomogenity.
Proposition 4: The space of cohomogenous inframeasures equipped with the I-topology is a Polish space.
But all of this is somewhat complicated, we might hope that when is compact, things get a bit nicer. And it turns out, yes, that works.
Proposition 5: If is a compact Polish space, then the space of -inframeasures and the space of -inframeasures are both compact Polish spaces.
Our next order of business is characterizing when a set of inframeasures is compact in the I-topology. One tricky part is that inframeasures can "run off to infinity", and we've got that extra point-at-infinity, to deal with. So our first order of business is reducing the question of checking compactness to a slightly easier problem.
Proposition 6: A set of inframeasures is compact in the I-topology iff, for all , is compact in the I-topology.
So now we just need to characterize compactness for bounded sets. Sadly, this proof only works for the type signature, as far as I can tell.
Theorem 6: The Infra-Prokhorov Theorem A -bounded set of inframeasures, is compact in the I-topology iff it is closed, and for all , there is a compact set , which is a -almost support for all .
The basic idea is that, if you refer back to our description of the -CAS property, it was that there were compact sets that accounted for most of what the expectation values of a function were, as long as the bounds weren't too high. In this case, compactness matches up with the property of the same compact sets working as compact-almost-supports for all the inframeasures at once. This is basically the generalization of Prokhorov's Theorem to the inframeasure case.
The "shared -CAS property" is precisely this property, of there being compact sets where all of a batch of inframeasures agree that the behavior of a function (with given bounds) on that compact set accounts for most of what the expectation value of the function is.
And a set of inframeasures will be said to be "bounded" if .
Now, referring back to Less Basic Inframeasure Theory (condition 3 of definition 13), there was a condition there about when an infrakernel is nicely-behaved. As it turns out, with our little modification, it turns out that the "nice behavior" property of an infrakernel is just equivalent to continuity!
Proposition 7: The following properties are equivalent for a function (where is the -inframeasures).
1: is continuous and bounded when is equipped with the I-topology.
2: is bounded, and for all , if limits to , then limits to . And, for all compact sets , then the family of inframeasures has the shared -CAS property.
So we've characterized the space of infradistributions pretty well. We've got two different characterizations of the topology, four different characterizations of when inframeasures converge to each other, it's a nicely behaved (ie, Polish) space, it's compact when is compact, and we know what the compact sets in it look like, and the conditions for an infrakernel to be well behaved are literally just "be bounded and continuous".
The Scott Topology (again)
So now it's time to switch gears. There's one other notable topology on the space of inframeasures, the Scott-topology. Remember, there are lots of domain-theory connections to be found, and inframeasures have an ordering, so we can define the Scott-topology in the usual way, as upwards-closed sets inaccessible from below by directed suprema.
Also note that the ordering on the Scott-topology is reversed. Big sets/low-scoring inframeasures go on the bottom, small sets/high-scoring inrameasures go on the top. Yes, that means that is the highest inframeasure under the usual Domain-theory ordering. Hopefully that isn't too much of an issue.
This is a rather abstract topology, but spurred by our result that the strict topology on functions was made by combining the Scott and Antiscott topologies on functions, we may hope that the the Scott topology on inframeasures ends up looking like "one half of the I-topology", in a certain precise sense.
And lo and behold, this is the case. Remember how the compact-open topology/I-topology on inframeasures was made by declaring the sets to be open, for compact sets of functions and open sets of numbers?
Well, what if we swapped the open sets of numbers for Scott-open sets of numbers?
Proposition 8: The Scott-topology on the space of inframeasures is the compact-open topology, but with scott-open subsets of .
Cool! The Scott-topology is like "one half of the I-topology", in the sense that we're swapping out the open sets for the compact-open base with Scott-open sets.
We may hope to go even further, to find a Scott version of the IKR-metric. This will be tricky to do, however, because the Scott topology is a T0 topology, it's not even Hausdorff. So we can't use any old metric.
We've gotta use a pseudoquasimetric. Basically, it's like a metric, but the distance between distinct points can be 0, and distance can also be asymmetric. But the triangle inequality still holds.
Proposition 9: The scott-topology has a base given by , for arbitrary choices of . is the scott pseudoquasimetric, defined by
And just like the Scott topology is one half of the I-topology, this is one half of the IKR metric. The IKR metric asked "if we scale things down by the Lipschitz and norm term in the bottom, what's the maximum difference between and ?". And this is asking "if we scale things down by the Lipschitz and norm term in the bottom, what's the maximum amount by which undershoots ?"
And there's one last little thing to clean up. We've previously used a somewhat broader definition of infrakernels where they were lower-semicontinuous. Ie, . It seemed to just show up naturally from the math, and the concept has been used a few times since them.
As it turns out, there's a lot of equivalents to this condition! Scott-continuity, lower-semicontinuity, and having closed graph all match up.
Theorem 8: The following properties are equivalent for a function (where is the -inframeasures.)
1: is continuous when is equipped with the Scott-topology.
2: If limits to , then limits to 0.
3: If limits to and limits to , then .
4: If limits to then for all , , and for all compact sets and , fulfills the shared -CAS property.
5: The shared -CAS property is fulfilled on for all compact sets and bounds , and the graph of as a function is closed.
And that's about it. The topology side of things has been conclusively sorted out.
All credit for this beautiful work goes to Alex.