# 3

Theorem 1: Any sequence of infrakernels  which fulfill the niceness conditions have the infinite semidirect product  being well-defined and fulfilling the niceness conditions.

As a recap, the niceness conditions are:

1: Lower-semicontinuity for inputs: For all continuous bounded ,   is a lower-semicontinuous function.

2: 1-Lipschitzness for functions: For all  is 1-Lipschitz.

3: Compact-shared compact-almost-support: For all compact sets  and , there is a compact set  which is an -almost-support for all the  inframeasures where .

4: Constants increase: For all  and constant functions .

5: 1-normalization (only for the  type signature): For all

Now,  is defined as: Fixing an arbitrary sequence of compact sets ,

Our task is to show that  is a well-defined infrakernel which fulfills these five properties.

We will be reusing the proofs from "Less Basic Inframeasure Theory" (henceforth abbreviated as LBIT) when possible, and commenting on the differences when applicable.

The proof sketch is:

Part 1: Show that the functions you're feeding into those  infrakernels are guaranteed to be continuous.

Part 2: Show that all the  are infrakernels which fulfill the niceness conditions, via induction.

Part 3: Show that if a function only depends on the first n coordinates of the input, then the  values monotonically increase as m does.

Part 4: Give a general procedure for taking a compact subset of the space  and making a compact subset of the space  with nice properties related to compact almost-support, that preserves its nice properties when projected down to any finite stage.

Almost-Monotone Lemma: This is a sufficiently useful utility tool in other theorems to be broken out into its own result. It says you can take any  and  and compact set  and pick a sequence of compact sets  for the defining sequence of the infinite semidirect product such that the defining sequence for all the  (with ) is -almost-monotone.

Part 5: Use parts 2, 3, and 4 to show that for any two different  sequences, the defining sequences for the infinite infrakernel will limit to each each other (so if one converges, all do, if one diverges, all do, and if one wiggles around forever, all do), and then apply the Almost-Monotone Lemma to rule out the "wiggle around forever" case. Thus, the limit to define  exists, and doesn't depend on the choice of the sequence of compact sets. This solves well-definedness.

Part 6: Using parts 2 and 5, clean up the basic inframeasure conditions for  (monotonicity and concavity), and show 1-Lipschitzness, increase of constants, and 1-normalization for  while we're at it. That's 3/5 niceness conditions down, and all inframeasure conditions except for compact almost-support.

Part 7: Use our trick from Part 4 and our freedom of picking our compact set sequence from Part 5 to show the compact-shared compact-almost-support property for . This also means that individual outputs of the kernel fulfill CAS, which verifies the last condition we need to conclude that  is always an inframeasure. Only lower-semicontinuity of the kernel remains to be verified.

Part 8: We use the Almost-Monotone Lemma to wrap up the last condition, the lower-semicontinuity of the infinite infrakernel.

We often use the usual "start with thing we're trying to prove, and keep reducing it to a simpler problem" technique from the last time this proof path was used.

T1.1 Our desired result is whether the function
is continuous. This was already shown in "Less Basic Inframeasure Theory" (LBIT).

T1.2 The desired result is "if all the  have the five niceness properties, then all the  are infrakernels with the five niceness properties as well".

The proof sketch for this is that this splits into 6 properties we need to show induct up. Monotonicity (phase 1), concavity (phase 2), 1-Lipschitzness (phase 3), increasing constants (phase 4), shared compact-almost-support (phase 5), and lower-semicontinuity (phase 6), which splits into two parts, one where we show a particular function is continuous, and then show lower-semicontinuity in general. Then, we finish up by arguing that this gets everything we need.

For the base case, because  and we're assuming all the  have the niceness properties and are infrakernels,  trivially fulfills them.

Time for the induction step. Remember that

T1.2.1 Proof of monotonicity: Assume . Then

And the same goes for  so if we could prove

we'd be successful. Now, by monotonicity for  (by induction assumption), we'd have that result if

Letting  be arbitrary, by applying monotonicity for , we'd have that result if

Which is true since . And so we're done, montonicity inducts up.

T1.2.2 Proof of concavity:

and then, by concavity for all , and monotonicity for  (by induction assumption), we have

and then, by concavity for  (by induction assumption), we have

and then this packs up as

and concavity inducts on up.

T1.2.3 Proof of 1-Lipschitzness: we have

And by 1-Lipschitzness for  (by induction assumption), we have

And by 1-Lipschitzness for , we have

And 1-Lipschitzness inducts on up.

T1.2.4 Proof of increasing constants (and 1-normalization): We have

And then by increasing constants for , and monotonicity for  (induction assumption), we have

Now just apply increasing constants for  (induction assumption) to get

For 1-normalization in the  type signature, we can have , and then instead of an inequality, we have an equality, and the same proof path works, just using 1-normalization instead of increasing constants. They both induct up.

T1.2.5 Proof of the compact-shared CAS property: Our task is to take an arbitrary compact set , and find a compact set  where two functions  identical on the set only differ in expectation by  according to all  with .

Let , and define the set  as

where the first compact set is a shared -almost-support for the  where  (exists by compact-shared CAS for , an induction assumption) and the second compact set is a shared -almost-support for the  where  is in  (exists by compact-shared CAS for , an assumed niceness condition). Let  be continuous and identical on . Then, we have

Now, we apply Lemma 2 from LBIT, where we can upper-bound this quantity by "Lipschitz constant of the inframeasure times how much the functions differ on the almost-support + level of almost-support times how much the functions differ in general". We use  as our compact set for the inner function. It was defined as a -almost support for all  with , and  is 1-Lipschitz (induction assumption). So our upper bound is:

Focusing on that second chunk, we can apply 1-Lipschitzness of  to yield

For the first chunk, we can apply Lemma 2 from LBIT again, with  as our compact set, which is a -almost support for all  with , and  is 1-Lipschitz. So our upper bound is:

Now, since  and  are identical on  that first term just vanishes, yielding

We upper-bound this by

Which then clearly just reduces to

And we're done, the compact-shared CAS property inducts up.

T1.2.6.1 Proof of lower-semicontinuity: We'll start by taking an extended detour to show that the function

is lower-semicontinuous. Fix a convergent sequence of inputs,  which limit to . First up, the set

is compact in  since it converges and we have the limit point added in. By the compact-shared CAS property for , we can take any  and make a compact set  which is a shared -almost-support for all the  inframeasures. For any m, we can then apply the Lemma 2 (from LBIT) decomposition with the  -almost-support for all the  inframeasures (and 1-Lipschitzness of ) to get the inequality

That second term can be upper-bounded by , so doing that, we have

Now, the set  is a compact set, so any continuous bounded function  is uniformly continuous on it. For all , there is some  where two points only  apart within this set have  only differing by  on them. Since  limits to , for sufficiently large m, those two points will be within  of each either, so eventually

will be  or less for late enough m. So, for late enough m, we have

Since  can be arbitrary, we have that the sequences

and

limit to each other. Therefore,

And then, by lower-semicontinuity for , we have

and so, lower-semicontinuity of the function

T1.2.6.2 For lower-semicontinuity in inputs, we first unpack the semidirect product. Fix a sequence  which limits to .

Since we showed that the function

is lower-semicontinuous, we can apply the monotone convergence theorem for inframeasures and rewrite as

For any individual , call it , we have

We now run through the same proof path as earlier again. The set  is compact in  since it converges and we have the limit point added in. By the compact-shared CAS property for  (induction assumption), we can take any  and make a compact set  which is a shared -almost-support for all the  inframeasures. For any m, we can then apply the Lemma 2 (from LBIT) decomposition with the  -almost-support for all the  inframeasures (and 1-Lipschitzness of  by induction assumption) to get the inequality

That second term can be upper-bounded by , so doing that, we have

Now, the set  is a compact set, so any continuous bounded function f is uniformly continuous on it. For all , there is some  where two points only  apart within this set have  only differing by  on them. Since  limits to , for sufficiently large m, those two points will be within  of each either, so eventually

will be  or less for late enough m. So, for late enough m, we have

Since  can be arbitrary, we have that the sequences

and

limit to each other. Taking a break to recap, we had

and for any  fulfilling those bounding conditions for the sup, we have

and from our fresh new result, we then have

and, by lower-semicontinuity for  (induction assumption), we have

Since  was arbitrary below

this means that

Now, we can put our lower-semicontinuous upper bound back in to get

and we're done, induction applies for lower-semicontinuity.

All our induction steps have been shown. First, for showing that all the  are inframeasures, we have monotonicity and concavity. Lipschitzness is taken care of by our 1-Lipschitzness induction. Compact almost support is taken care of by our compact-shared CAS induction for the , because a single point is compact. And weak normalization (0 must map to 0 or more) is taken care of by our Constants Increase induction. So all the  are inframeasures.

For the 5 niceness conditions, we proved all of lower-semicontinuity, 1-Lipschitzness, compact-shared CAS, increasing constants, and 1-normalization by induction. So we can now assume that all  are nice.

T1.3 We must show that if we go far enough out in the , the value assigned to functions which only depend on finitely many inputs starts monotonically increasing. The result that we'd like to show at this point is:

Fix an arbitrary  and . Then, we can just go:

Since , that function at the end is a constant (doesn't depend on its input), so by Increasing Constants for  and Monotonicity for , we have

and we're done.

T1.4 Our desired result here is: