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.

Proof of C-additivity preservation:

Proof of crispness preservation: Crispness is equivalent to the conjunction of C-additivity and homogenity and both of those are preserved.

Proof of sharpness preservation: So, this will take a bit of work because we do have to get a fairly explicit form for the set you're minimizing over. Remember that when and are crisp, with associated compact sets and , then the compact minimizing set for is , from the proof of sharpness preservation for semidirect product. Another way of writing this minimizing set of the semidirect product is as the set

Now, we'll give a form for the associated compact set of . It is:

For the base case, observe that when , it's

which works out perfectly. For the induction step, because