# 4

Formal ProofAI
Frontpage

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,

Therefore,

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 normalization,

For monotonicity, if ,

For concavity,

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.

Homogenity:

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.

Cohomogenity:

Crispness: Both homogenity and C-additivity are preserved, so crispness is too.

Sharpness:

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

is compact.

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 , the almost-support. So, the supremum is upper-bounded by

Substituting this back in, we get: