# 4

Formal ProofAI
Frontpage

Part 6: Showing the basic four infradistribution properties: Normalization, monotonicity, concavity, and Lipschitzness (specifically 1-Lipschitzness). For normalization, observe that regardless of ,

The limit of the all-1 sequence is 1 and the limit of the all-0 sequence is 0, so:

For monotonicity, let  Then, regardless of ,

This is because, since , the "extend with worst-case outputs" function is bigger for  than , and then by monotonicity for , the inequality transfers to the outside.

Accordingly,

Now for concavity. For all

This was by monotonicity (minimizing over the two parts separately produces lower values, and monotonicity transfers that to the outside), and concavity respectively, because  is an infradistribution. And now:

Concavity is shown. Now for 1-Lipschitzness. Fix an arbitrary . Our proof target is:

Now, if we knew:

Then we'd be able to pair that with the 1-Lipschitzness of  to get our desired result. So let this be our new proof target. Reexpressing it a bit, it's:

Now, if two functions are only  apart, then their minimal values over a compact set can only be  apart at most. Let your compact set be  to see the result. Thus, we have proved our proof target and we have the result that, for all

Since they're always only  apart, the same property transfers to the limit, so we get:

And so,  is 1-Lipschitz for all . This takes care of the Lipschitzness condition on infradistributions and the uniform Lipschitz bound condition on infrakernels. All that's left is the compact almost-support condition on infradistributions and the compact-shared compact almost-support condition on infrakernels, and the pointwise convergence condition on infrakernels.

Part 7: This will use our result from Part 4 about making a suitable compact set. Our desired thing we want to prove is that

Because this property is exactly the compact-shared compact-almost-support property for .

So, here's our plan of attack. Fix our  and , so our target is

Let our  be , as defined from Part 4, and let  be arbitrary in  and  be arbitrary and agree with each other on . Then our goal becomes

Now, letting our chosen defining sequence be , our goal is to show

If we could do this, all the approximating points being only  away from each other shows that the same property transfers to the limit and we get our result. Accordingly, let  be arbitrary, and our proof goal is now:

Hypothetically, if we were able to show:

Then we could conclude the two functions were equal on the set , which, from Part 4, is an -almost support for all the  where , and it would yield our result. So our proof target is now

Accordingly, let  be arbitrary within said set, turning our proof target into:

However,  and  are equal on the set , which breaks down as . And we know that , and since the second part is being selected from , the two values are equal, and we've proved our proof target. Thus, we have compactly-shared  compact almost-support, and that's the second condition for  to be an infrakernel, as well as the last condition needed for all the  to be infradistributions. Just pointwise convergence left!

Part 8: Alright, for showing pointwise convergence, we'll need a lemma. We need to show:

This is roughly saying that the rate of convergence of  to  is uniform over compact sets. Let's begin. Let  be arbitrary, so our proof target is now:

Here's what we'll do. Because we have a  and , we can craft our sequence  of compact -supports. Now, on the set:

which is compact, we know that  is uniformly continuous, so there's some  you need to go to to ensure that function values are only  away from each other, which translates into an  via . Any two inputs which only differ beyond that point will be only  apart and can only get an -difference in values from . Now that that's defined, let  and  be arbitrary. Our proof target is now to show:

We know from Part 3 that

So let's make that substitution, turning our proof target into

Assuming hypothetically we were able to show that:

Then, because  is an -almost-support for  as long as  (which we know to be the case), we could apply Lemma 2 to get our desired proof target.

The "Lipschitz constant times deviation over compact set" part would make one , and the "degree of almost-support times difference in the two functions" part would make  in the worst-case due to being an -almost-support and the worst possible case where the two functions differ by  somewhere.

So now our proof target is:

Thus, let  be arbitrary within the appropriate set, so our proof target is now:

Because we're minimizing over a compact set in both instances, we can consider the infs to be attained by a  and a , so our proof target is now

Now, because , and , we have:

And also, because , and ,

So, both inputs lie in the relevant compact set, and they agree on , so the inputs are only  apart, so they only have value differing by , and we're done, our desired result of

goes through.

Part 9: Now, for showing our pointwise continuity property, fix a sequence  which limits to , and an arbitrary . Our task is now to show that:

Fixing some arbitrary  sequence, we could do this if we could show that

Now, because

we can rewrite our desired proof target as:

Huh, we just need to swap our limits! And the Moore-Osgood theorem says you can swap limits while preserving equality if, for fixed ,

and (this part is harder)

limits to

uniformly in . However, back in Part 8 we established uniform convergence on any compact set. And  is a compact set! So we have uniform convergence and can invoke Moore-Osgood to swap the limits and get our proof target, showing our result, that

So,  fulfills pointwise convergence and we've verified all properties needed to show it's an infrakernel.

Part 10: Showing that if all the  have some nice property, then  inherits it too. Homogenity, Cohomogenity, C-additivity, crispness, and sharpness.

Proof of homogenity preservation:

Proof of cohomogenity preservation: Let your  be a mere sequence of points , that's compact.