Lemma 3: If is a continuous function of type , where is the space of nonempty compact subsets of the space , then given any compact set , will be compact in .
Fix some compact set , and continuous function . We will operate by taking an arbitrary open cover of and finding a finite subcover.
Let be an open cover of . The are subsets of . The topology compatible with Hausdorff distance on (space of compact subsets of ) is the Vietoris topology, where the basis opens are given by finite collections of open sets in . You take the set of all compact subsets of which are subsets of the union of your finite collection of open sets, and intersect every open set in your finite collection
Accordingly, let (the set of all finite subsets of , the index set for our open cover), and fix a collection of open sets in , . The sets are defined as:
Now, all the with are compact ( produces compact sets as output), and they are all subsets of , so is a cover of , and due to its compactness we can identify a finite subcover, and prune away every open st which doesn't intersect . is a subset of the union of those finitely many open sets, and intersects all of them, so the point lies in the open set induced by that finite cover of open sets.
This argument works for arbitrary with , so the collection is an open cover of . Also, because is continuous and is compact, is compact, so we can identify a finite subcover from .
Then, consider the collection of open sets where for some which is part of the finite cover of . This is finitely many opens, we're unioning together finitely many (finitely many selected) finite sets of open sets (each is associated with finitely many that it was built from).
Now we just have to show that this collection covers , and we'll have made our finite subcover and shown that said set is compact. Assume our finite collection of opens doesn't cover the set. Then there's some which wasn't covered completely. However, the point corresponding to in lies in some , and from its definition, the corresponding manage to cover , and we have a contradiction. We're done.
Proposition 19: is an infradistribution, and preserves all properties indicated in the diagram at the start of this section if and all the have said property.
To show this, we'll verify that it's well-defined at all, normalization, monotonicity, concavity, Lipschitzness, compact almost-support, and preservation of the properties.
Our first order of business is verifying that
is even a continuous function to be able to show that can accept it as input.
For continuity, let limit to , and we'll try to show that limits to . Let be the Lipschitz constant upper bound of .
Pick an , we'll show that there's some where
First, note that is a compact set because limits to . Thus, by the compact-shared compact almost-support condition on an infrakernel, there must be some compact set where all the agree that functions agreeing on have values only apart from each other.
Now, because f is a continuous bounded function , it's uniformly continuous when restricted to
as this is the product of two compact sets and is compact. Due to the uniform continuity of restricted to that set, there is some number where points only apart in that set have their values only differing by . Further, there is some number where, for all , .
Additionally, the maximum difference between and is .
Now that we know our number we can pick an arbitrary above it, and go:
And now, because these two functions restricted to are only apart, we can apply Lemma 2 to conclude that (since and work for all the )
This argument works for any , so we have:
Letting in particular,
And for each \eps we can construct a m_0 in this way, concluding that
Also, from our pointwise convergence condition on infradistributions,
and so, we now know that
is a continuous function . For boundedness, upper and lower bounds on are (and the negative version of it). Due to the shared Lipschitz constant on the , an upper and lower-bound on is (and the negative version.) Thus, we can safely feed said function into the infradistribution , so the semidirect product is well-defined. We must still show that it makes an infradistribution.
For monotonicity, if ,
In order, this was the definition of the semidirect product, all the being concave so splitting them up produces a lower value (and then monotonicity for ), then being concave.
This leaves Lipschitzness and CAS. For Lipschitzness, given some and , and letting be the Lipschitz constant of , we have:
Thus, that final thing shows that there's a finite Lipschitz constant for .
This leaves compact almost-support. Pick any . This induces a compact set which is an -almost-support for , and then this compact set induces a compact set which an -almost-support for all the where . Now, we can apply Lemma 2 to go:
Pretty much, that first part is the " is an -almost-support for " piece, and the second piece is the "hey, these two functions may be a bit different on said compact set, we've gotta multiply that by the Lipschitz constant" piece. So, let's work on unpacking these two distances. For the first one, we can go:
Substituting this back in produces:
Time to go after the second distance piece. We have:
And, because and agree on , we have and agreeing on , which is an -almost-support for all the where , so we have:
Substituting this back in produces:
And regrouping this and recapping means that we have:
So we have crafted a compact -support for , and we can make arbitrarily small, so the semidirect product has compact almost-support, which is the last condition we needed.
Time for property verification.
1-Lipschitz: We showed in the Lipschitz section that an upper bound on the Lipschitz constant of is the product of the Lipschitz constants of the kernel and the original infradistribution, so and 1-Lipschitzness is preserved.
Crispness: Both homogenity and C-additivity are preserved, so crispness is too.
Our task now is to show that is compact, which will take a fair amount of topology work. Our first piece that we'll need is that if limits to , then limits to in Hausdorff-distance.
To show this, we'll split it into two parts. First, we'll assume that there is an where, infinitely often, there is a point in that is away from and disprove that. Second, we'll assume there is an where, infinitely often, there is a point in that is away from , and disprove that.
For the first part, assume that there is an where, infinitely often, there is a point in that is away from . Craft the continuous function
What this does is it's 1 on the set , and 0 on anything more than away from it. One of our conditions on an infrakernel was that , so:
The latter term is 1 because is 1 over . However, because we're assuming that infinitely often, there's a point in that is away from , the sequence on the left-hand side is infinitely often 0, so it doesn't converge and we have a contradiction.
For the second part, assume there is an where, infinitely often, there is a point in that is away from . By compactness of , we can find finitely many points in it s.t. every point in is only away from one of the (cover with -size open balls centered on points in it and take a finite subcover). Now, for each of these, we can craft a function
So, this is 0 at the point , and 1 at any distance or more away from it.
One of our conditions on an infrakernel was that , and there are finitely many , so there's some time where all of them nearly converge, ie:
However, infinitely often there's a point that is away from . is away from some , so that can't be closer than to . (if it was closer, then we could pick some point in that's closer than to , and then since it's only away from , we'd have that the distance from to is below , an impossibility).
Because the distance from to any point in is above , then
This is because and attains a value of 0 according to , while stays away from and all its points must have a value of 1. This situation happens infinitely often, which leads to a contradiction with
Because infinitely often, one of these has very different values, so the sequence is 1 infinitely often and can't limit to 0.
So, we've ruled out that there is an where, infinitely often, there is a point in that is away from . And we've ruled out that there is an where, infinitely often, there is a point in that is away from . Fixing any , in the tail of the sequence, and are distance or closer in Hausdorff distance because you can't find points in either set which are far away from the other set. So, limits to in Hausdorff-distance when limits to , and we know that is a continuous function .
This lets us show that the set
is closed, because if limits to and and limits to , we have that because limits to in Hausdorff distance, so we've got closed graph.
Also, by invoking Lemma 3, we know that
Time to wrap this all up. We know that is closed in from our Hausdorff limit argument. This set is also a subset of:
Which is a product of two sets known to be compact, and is compact. It's a closed subset of a compact set, so it's compact. Therefore,
is a compact set, and from way back,
And we've shown that set is compact, so where and all the are sharp can be written as minimizing over a compact set, so is sharp. Thus, semidirect product preserves all the nice properties, and we're finally done with this proof.
Proposition 20: If all the are C-additive, then .
This is because, since doesn't depend on , it acts as a constant inside and C-additivity lets us pull it out.
Proposition 21: If are a sequence of infrakernels of type , and is an infradistribution over , then can be rewritten as where is an infrakernel of type , recursively defined as and
So, for our inductive definition,
Our task is to show that these are all infrakernels, by induction, and that for any infradistribution ,
For the base case, we observe that is an infrakernel because it equals , which is an infrakernel, and that
Time for the induction step. We'll assume that is an infrakernel, and show that is. Further, we need to show that . This will show the result.
Our first requirement is showing that for all , is an infradistribution.
By our induction assumption, is an infradistribution as is an infrakernel. Further, is an infrakernel because is and we're just restricting it to a subset of its domain, so it keeps being an infrakernel. And we know from earlier that the semidirect product of an infradistribution and an infrakernel is an infradistribution. So that's taken care of.
Now, we must show a common Lipschitz constant, pointwise function convergence, and compact-shared compact almost-support for to certify that it's an infrakernel.
Starting with common Lipschitz constant, we can just note that, in our proof of Proposition 19, we saw that the Lipschitz constant of the semidirect product was upper-bounded by the product of the Lipschitz constants of the starting infradistributions and the kernel. Assuming that is an infradistribution, we have that the Lipschitz constant of any is upper-bounded by some Lipschitz constant. Also, the Lipschitz constant of is upper-bounded by some Lipschitz constant. Thus, is an upper-bound on the Lipschitz constant of any
infradistribution, which is exactly , witnessing that has a uniform upper bound on its Lipschitz constants.
Time to move onto the second one, compact-shared compact almost-support.
For this one, we're trying to prove:
This is the sentence that says that has compact-shared compact almost-support. and have type signature .
Now, this is going to be quite complicated, so pay close attention. Fix an arbitrary compact , and an arbitrary . Let be the Lipschitz constant for the infrakernel , and be the Lipschitz constant for the infrakernel .
Due to compact-shared compact-almost-support for which exists by our induction assumption, your set induces a compact -almost-support for the family of infradistributions where . Call said almost-support .
Further, due to compact-shared compact-almost-support for , the set
induces a compact -almost-support for the family of infradistributions where
Call said almost-support
And now let your shared -almost-support for where be:
We must show that said set is indeed a shared -almost-support for where . So, let and agree on said set. Then, we have:
This is just unpacking the definition of the iterated semidirect product, no issues here. Now, we use Lemma 2 and the fact that is a -almost-support for when , to get:
Ok, this is a mess. Let's try to unpack
first. What we can do is use that, regardless of what is picked in the supremum, we have:
So this means that
is a -almost-support for . Further, because and are identical on
and was being selected from the former of those, then the functions (and the same for ) agree on