Proofs Theorem 1

Theorem 1: Any sequence of infrakernels $K_{n} : \prod_{i = 0}^{i = n} X_{i} i k \to X_{n + 1}$ which fulfill the niceness conditions have the infinite semidirect product $K_{: \infty}$ being well-defined and fulfilling the niceness conditions.

As a recap, the niceness conditions are:

1: Lower-semicontinuity for inputs: For all continuous bounded $f$ , $x_{0 : n} \mapsto K_{n} (x_{0 : n}) (f)$ is a lower-semicontinuous function.

2: 1-Lipschitzness for functions: For all $x_{0 : n}$ , $f \mapsto K_{n} (x_{0 : n}) (f)$ is 1-Lipschitz.

3: Compact-shared compact-almost-support: For all compact sets $C \subseteq \prod_{i = 0}^{i = n} X_{i}$ and $ϵ$ , there is a compact set $C_{n + 1} \subseteq X_{n + 1}$ which is an $ϵ$ -almost-support for all the $K_{n} (x_{0 : n})$ inframeasures where $x_{0 : n} \in C$ .

4: Constants increase: For all $x_{0 : n}$ and constant functions $c$ , $K_{n} (x_{0 : n}) (c) \geq c$ .

5: 1-normalization (only for the $[0, 1]$ type signature): For all $x_{0 : n}$ , $K_{n} (x_{0 : n}) (1) = 1$

Now, $K_{: \infty} : X_{0} i k \to \prod_{i = 1}^{\infty} X_{i}$ is defined as: Fixing an arbitrary sequence of compact sets $C_{i} \subseteq X_{i}$ ,

$K_{: \infty} (x_{0}) (f) := {lim}_{n \to \infty} K_{: n} (x_{0}) (λ x_{1 : n + 1} {inf}_{x_{n + 2 : \infty} \in \prod_{i = n + 2}^{\infty} C_{i}} f (x_{1 : n + 1}, x_{n + 2 : \infty}))$

Our task is to show that $K_{: \infty}$ 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 $K_{: n}$ infrakernels are guaranteed to be continuous.

Part 2: Show that all the $K_{: n}$ 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 $K_{: n + m} (x_{0}) (f)$ values monotonically increase as m does.

Part 4: Give a general procedure for taking a compact subset of the space $X_{0}$ and making a compact subset of the space $\prod_{i = 1}^{\infty} X_{i}$ 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 $f$ and $ϵ$ and compact set $C_{0} \subseteq X_{0}$ and pick a sequence of compact sets $C_{i}$ for the defining sequence of the infinite semidirect product such that the defining sequence for all the $K_{: \infty} (x_{0}) (f)$ (with $x_{0} \in C_{0}$ ) is $4 ϵ | | f | |$ -almost-monotone.

Part 5: Use parts 2, 3, and 4 to show that for any two different $C_{i}$ 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 $K_{: \infty} (x_{0}) (f)$ 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 $K_{: \infty} (x_{0})$ (monotonicity and concavity), and show 1-Lipschitzness, increase of constants, and 1-normalization for $K_{: \infty}$ 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 $K_{: \infty}$ . This also means that individual outputs of the kernel fulfill CAS, which verifies the last condition we need to conclude that $K_{: \infty} (x_{0})$ 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 $λ x_{1 : n + 1} . {inf}_{x_{n + 2 : \infty} \in \prod_{i = n + 2}^{\infty} C_{i}} f (x_{1 : n + 1}, x_{n + 2 : \infty})$
is continuous. This was already shown in "Less Basic Inframeasure Theory" (LBIT).

T1.2 The desired result is "if all the $K_{n}$ have the five niceness properties, then all the $K_{: n}$ 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 $K_{: 0} := K_{0}$ and we're assuming all the $K_{n}$ have the niceness properties and are infrakernels, $K_{: 0}$ trivially fulfills them.

Time for the induction step. Remember that $K_{: n + 1} (x_{0}) := K_{: n} (x_{0}) ⋉ (λ x_{1 : n + 1} . K_{n + 1} (x_{0}, x_{1 : n + 1}))$

T1.2.1 Proof of monotonicity: Assume $f^{'} \geq f$ . Then

$K_{: n + 1} (x_{0}) (f^{'}) = K_{: n} (x_{0}) (λ x_{1 : n + 1} . K_{n + 1} (x_{0}, x_{1 : n + 1}) (λ x_{n + 2} . f^{'} (x_{1 : n + 1}, x_{n + 2})))$

And the same goes for $f$ so if we could prove

$K_{: n} (x_{0}) (λ x_{1 : n + 1} . K_{n + 1} (x_{0}, x_{1 : n + 1}) (λ x_{n + 2} . f^{'} (x_{1 : n + 1}, x_{n + 2})))$
$\geq K_{: n} (x_{0}) (λ x_{1 : n + 1} . K_{n + 1} (x_{0}, x_{1 : n + 1}) (λ x_{n + 2} . f (x_{1 : n + 1}, x_{n + 2})))$

we'd be successful. Now, by monotonicity for $K_{: n}$ (by induction assumption), we'd have that result if

$\forall x_{1 : n + 1} : K_{n + 1} (x_{0}, x_{1 : n + 1}) (λ x_{n + 2} . f^{'} (x_{1 : n + 1}, x_{n + 2}))$
$\geq K_{n + 1} (x_{0}, x_{1 : n + 1}) (λ x_{n + 2} . f (x_{1 : n + 1}, x_{n + 2}))$

Letting $x_{1 : n + 1}$ be arbitrary, by applying monotonicity for $K_{n + 1}$ , we'd have that result if

$\forall x_{n + 2} : f^{'} (x_{1 : n + 1}, x_{n + 2}) \geq f (x_{1 : n + 1}, x_{n + 2})$

Which is true since $f^{'} \geq f$ . And so we're done, montonicity inducts up.

T1.2.2 Proof of concavity:

$K_{: n + 1} (x_{0}) (p f + (1 - p) f^{'})$

$= K_{: n} (x_{0}) (λ x_{1 : n + 1} . K_{n + 1} (x_{0}, x_{1 : n + 1}) (λ x_{n + 2} . p f (x_{1 : n + 1}, x_{n + 2}) + (1 - p) f^{'} (x_{1 : n + 1}, x_{n + 2})))$

and then, by concavity for all $K_{n + 1}$ , and monotonicity for $K_{: n}$ (by induction assumption), we have

$\geq K_{: n} (x_{0}) (λ x_{1 : n + 1} . p K_{n + 1} (x_{0}, x_{1 : n + 1}) (λ x_{n + 2} . f (x_{1 : n + 1}, x_{n + 2}))$
$+ (1 - p) K_{n + 1} (x_{0}, x_{1 : n + 1}) (λ x_{n + 2} . f^{'} (x_{1 : n + 1}, x_{n + 2})))$

and then, by concavity for $K_{: n}$ (by induction assumption), we have

$\geq p K_{: n} (x_{0}) (λ x_{1 : n + 1} . K_{n + 1} (x_{0}, x_{1 : n + 1}) (λ x_{n + 2} . f (x_{1 : n + 1}, x_{n + 2})))$
$+ (1 - p) K_{: n} (x_{0}) (λ x_{1 : n + 1} . K_{n + 1} (x_{0}, x_{1 : n + 1}) (λ x_{n + 2} . f^{'} (x_{1 : n + 1}, x_{n + 2})))$

and then this packs up as

$= p K_{: n + 1} (x_{0}) (f) + (1 - p) K_{: n + 1} (f^{'})$

and concavity inducts on up.

T1.2.3 Proof of 1-Lipschitzness: we have

$| K_{: n + 1} (x_{0}) (f) - K_{: n + 1} (x_{0}) (f^{'}) |$

$= | K_{: n} (x_{0}) (λ x_{1 : n + 1} . K_{n + 1} (x_{0}, x_{1 : n + 1}) (λ x_{n + 2} . f (x_{1 : n + 1}, x_{n + 2})))$
$- K_{: n} (x_{0}) (λ x_{1 : n + 1} . K_{n + 1} (x_{0}, x_{1 : n + 1}) (λ x_{n + 2} . f^{'} (x_{1 : n + 1}, x_{n + 2}))) |$

And by 1-Lipschitzness for $K_{: n}$ (by induction assumption), we have

$\leq {sup}_{x_{1 : n + 1}} | K_{n + 1} (x_{0}, x_{1 : n + 1}) (λ x_{n + 2} . f (x_{1 : n + 1}, x_{n + 2}))$
$- K_{n + 1} (x_{0}, x_{1 : n + 1}) (λ x_{n + 2} . f^{'} (x_{1 : n + 1}, x_{n + 2})) |$

And by 1-Lipschitzness for $K_{n + 1}$ , we have

$\leq {sup}_{x_{1 : n + 1}, x_{n + 2}} | f (x_{1 : n + 1}, x_{n + 2}) - f^{'} (x_{1 : n + 1}, x_{n + 2}) | = d (f, f^{'})$

And 1-Lipschitzness inducts on up.

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

$K_{: n + 1} (x_{0}) (c) = K_{: n} (x_{0}) (λ x_{1 : n + 1} . K_{n + 1} (x_{0}, x_{1 : n + 1}) (c))$

And then by increasing constants for $K_{n + 1}$ , and monotonicity for $K_{: n}$ (induction assumption), we have

$\geq K_{: n} (x_{0}) (λ x_{1 : n + 1} . c)$

Now just apply increasing constants for $K_{: n}$ (induction assumption) to get $\geq c$

For 1-normalization in the $[0, 1]$ type signature, we can have $c = 1$ , 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 $C^{X_{0}} \subseteq X_{0}$ , and find a compact set $C_{ϵ}^{\prod_{i = 1}^{i = n + 2} X_{i}} \subseteq \prod_{i = 1}^{i = n + 2} X_{i}$ where two functions $f, f^{'}$ identical on the set only differ in expectation by $ϵ d (f, f^{'})$ according to all $K_{: n + 1} (x_{0})$ with $x_{0} \in C^{X_{0}}$ .

Let $x_{0} \in C^{X_{0}}$ , and define the set $C_{ϵ}^{\prod_{i = 1}^{i = n + 2} X_{i}}$ as $C_{\frac{ϵ}{2}}^{\prod_{i = 1}^{i = n + 1} X_{i}} \times C_{\frac{ϵ}{2}}^{X_{n + 2}}$

where the first compact set is a shared $\frac{ϵ}{2}$ -almost-support for the $K_{: n} (x_{0})$ where $x_{0} \in C^{X_{0}}$ (exists by compact-shared CAS for $K_{: n}$ , an induction assumption) and the second compact set is a shared $\frac{ϵ}{2}$ -almost-support for the $K_{n + 1} (x_{0}, x_{1 : n + 1})$ where $x_{0}, x_{1 : n + 1}$ is in $C^{X_{0}} \times C_{\frac{ϵ}{2}}^{\prod_{i = 1}^{i = n + 1} X_{i}}$ (exists by compact-shared CAS for $K_{n + 1}$ , an assumed niceness condition). Let $f, f^{'}$ be continuous and identical on $C_{ϵ}^{\prod_{i = 1}^{i = n + 2} X_{i}}$ . Then, we have

$| K_{: n + 1} (x_{0}) (f) - K_{: n + 1} (x_{0}) (f^{'}) |$

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 $C_{\frac{ϵ}{2}}^{\prod_{i = 1}^{i = n + 1} X_{i}}$ as our compact set for the inner function. It was defined as a $\frac{ϵ}{2}$ -almost support for all $K_{: n} (x_{0})$ with $x_{0} \in C^{X_{0}}$ , and $K_{: n}$ is 1-Lipschitz (induction assumption). So our upper bound is:

$\leq {sup}_{x_{1 : n + 1} \in C_{\frac{ϵ}{2}}^{\prod_{i = 1}^{i = n + 1} X_{i}}} | K_{n + 1} (x_{0}, x_{1 : n + 1}) (λ x_{n + 2} . f (x_{1 : n + 1}, x_{n + 2}))$
$- K_{n + 1} (x_{0}, x_{1 : n + 1}) (λ x_{n + 2} . f^{'} (x_{1 : n + 1}, x_{n + 2})) |$
$+ \frac{ϵ}{2} \cdot {sup}_{x_{1 : n + 1}} | K_{n + 1} (x_{0}, x_{1 : n + 1}) (λ x_{n + 2} . f (x_{1 : n + 1}, x_{n + 2}))$
$- K_{n + 1} (x_{0}, x_{1 : n + 1}) (λ x_{n + 2} . f^{'} (x_{1 : n + 1}, x_{n + 2})) |$

Focusing on that second chunk, we can apply 1-Lipschitzness of $K_{n + 1}$ to yield

$\leq {sup}_{x_{1 : n + 1} \in C_{\frac{ϵ}{2}}^{\prod_{i = 1}^{i = n + 1} X_{i}}} | K_{n + 1} (x_{0}, x_{1 : n + 1}) (λ x_{n + 2} . f (x_{1 : n + 1}, x_{n + 2}))$
$- K_{n + 1} (x_{0}, x_{1 : n + 1}) (λ x_{n + 2} . f^{'} (x_{1 : n + 1}, x_{n + 2})) |$
$+ \frac{ϵ}{2} \cdot {sup}_{x_{1 : n + 1}, x_{n + 2}} | f (x_{1 : n + 1}, x_{n + 2}) - f^{'} (x_{1 : n + 1}, x_{n + 2}) |$

For the first chunk, we can apply Lemma 2 from LBIT again, with $C_{\frac{ϵ}{2}}^{X_{n + 2}}$ as our compact set, which is a $\frac{ϵ}{2}$ -almost support for all $K_{n + 1} (x_{0}, x_{1 : n + 1})$ with $x_{0}, x_{1 : n + 1} \in C^{X_{0}} \times C_{\frac{ϵ}{2}}^{\prod_{i = 1}^{i = n + 1} X_{i}}$ , and $K_{n + 1}$ is 1-Lipschitz. So our upper bound is:

$\leq {sup}_{x_{1 : n + 1} \in C_{\frac{ϵ}{2}}^{\prod_{i = 1}^{i = n + 1} X_{i}}} ({sup}_{x_{n + 2} \in C_{\frac{ϵ}{2}}^{X_{n + 2}}} | f (x_{1 : n + 1}, x_{n + 2}) - f^{'} (x_{1 : n + 1}, x_{n + 2}) |$
$+ \frac{ϵ}{2} \cdot {sup}_{x_{n + 2}} | f (x_{1 : n + 1}, x_{n + 2}) - f^{'} (x_{1 : n + 1}, x_{n + 2}) |)$
$+ \frac{ϵ}{2} \cdot {sup}_{x_{1 : n + 1}, x_{n + 2}} | f (x_{1 : n + 1}, x_{n + 2}) - f^{'} (x_{1 : n + 1}, x_{n + 2}) |$

Now, since $f$ and $f^{'}$ are identical on $C_{\frac{ϵ}{2}}^{\prod_{i = 1}^{i = n + 1} X_{i}} \times C_{\frac{ϵ}{2}}^{X_{n + 2}}$ that first term just vanishes, yielding

$= {sup}_{x_{1 : n + 1} \in C_{\frac{ϵ}{2}}^{\prod_{i = 1}^{i = n + 1} X_{i}}} (\frac{ϵ}{2} \cdot {sup}_{x_{n + 2}} | f (x_{1 : n + 1}, x_{n + 2}) - f^{'} (x_{1 : n + 1}, x_{n + 2}) |)$
$+ \frac{ϵ}{2} \cdot {sup}_{x_{1 : n + 1}, x_{n + 2}} | f (x_{1 : n + 1}, x_{n + 2}) - f^{'} (x_{1 : n + 1}, x_{n + 2}) |$

We upper-bound this by

$\leq \frac{ϵ}{2} {sup}_{x_{1 : n + 1}, x_{n + 2}} | f (x_{1 : n + 1}, x_{n + 2}) - f^{'} (x_{1 : n + 1}, x_{n + 2}) |$
$+ \frac{ϵ}{2} \cdot {sup}_{x_{1 : n + 1}, x_{n + 2}} | f (x_{1 : n + 1}, x_{n + 2}) - f^{'} (x_{1 : n + 1}, x_{n + 2}) |$

Which then clearly just reduces to

$= ϵ d (f, f^{'})$

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

$λ x_{0}, x_{1 : n + 1} . K_{n + 1} (x_{0}, x_{1 : n + 1}) (λ x_{n + 2} . f (x_{1 : n + 1}, x_{n + 2}))$

is lower-semicontinuous. Fix a convergent sequence of inputs, $x_{0}^{m}, x_{1 : n + 1}^{m}$ which limit to $x_{0}^{\infty}, x_{1 : n + 1}^{\infty}$ . First up, the set

${x_{0}^{m}, x_{1 : n + 1}^{m}}_{m \in N ⊔ {\infty}}$

is compact in $\prod_{i = 0}^{i = n + 1} X_{i}$ since it converges and we have the limit point added in. By the compact-shared CAS property for $K_{n + 1}$ , we can take any $ϵ$ and make a compact set $C_{ϵ}^{X_{n + 2}} \subseteq X_{n + 2}$ which is a shared $ϵ$ -almost-support for all the $K_{n + 1} (x_{0}^{m}, x_{1 : n + 1}^{m})$ inframeasures. For any m, we can then apply the Lemma 2 (from LBIT) decomposition with the $C_{ϵ}^{X_{n + 2}}$ $ϵ$ -almost-support for all the $K_{n + 1} (x_{0}^{m}, x_{1 : n + 1}^{m})$ inframeasures (and 1-Lipschitzness of $K_{n + 1}$ ) to get the inequality

$| K_{n + 1} (x_{0}^{m}, x_{1 : n + 1}^{m}) (λ x_{n + 2} . f (x_{1 : n + 1}^{m}, x_{n + 2})) - K_{n + 1} (x_{0}^{m}, x_{1 : n + 1}^{m}) (λ x_{n + 2} . f (x_{1 : n + 1}^{\infty}, x_{n + 2})) |$

$\leq {sup}_{x_{n + 2} \in C_{ϵ}^{X_{n + 2}}} | f (x_{1 : n + 1}^{m}, x_{n + 2}) - f (x_{1 : n + 1}^{\infty}, x_{n + 2}) |$
$+ ϵ {sup}_{x_{n + 2}} | f (x_{1 : n + 1}^{m}, x_{n + 2}) - f (x_{1 : n + 1}^{\infty}, x_{n + 2}) |$

That second term can be upper-bounded by $2 | | f | |$ , so doing that, we have

$\leq {sup}_{x_{n + 2} \in C_{ϵ}^{X_{n + 2}}} | f (x_{1 : n + 1}^{m}, x_{n + 2}) - f (x_{1 : n + 1}^{\infty}, x_{n + 2}) | + 2 ϵ | | f | |$

Now, the set ${x_{0}^{m}, x_{1 : n + 1}^{m}}_{m \in N ⊔ {\infty}} \times C_{ϵ}^{X_{n + 2}}$ 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 $f$ only differing by $ϵ$ on them. Since $x_{1 : n + 1}^{m}$ limits to $x_{1 : n + 1}^{\infty}$ , for sufficiently large m, those two points will be within $δ$ of each either, so eventually

${sup}_{x_{n + 2} \in C_{ϵ}^{X_{n + 2}}} | f (x_{1 : n + 1}^{m}, x_{n + 2}) - f (x_{1 : n + 1}^{\infty}, x_{n + 2}) |$

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

$| K_{n + 1} (x_{0}^{m}, x_{1 : n + 1}^{m}) (λ x_{n + 2} . f (x_{1 : n + 1}^{m}, x_{n + 2})) - K_{n + 1} (x_{0}^{m}, x_{1 : n + 1}^{m}) (λ x_{n + 2} . f (x_{1 : n + 1}^{\infty}, x_{n + 2})) |$

$\leq ϵ + 2 ϵ | | f | |$

Since $ϵ$ can be arbitrary, we have that the sequences

$K_{n + 1} (x_{0}^{m}, x_{1 : n + 1}^{m}) (λ x_{n + 2} . f (x_{1 : n + 1}^{m}, x_{n + 2}))$

and

$K_{n + 1} (x_{0}^{m}, x_{1 : n + 1}^{m}) (λ x_{n + 2} . f (x_{1 : n + 1}^{\infty}, x_{n + 2}))$

limit to each other. Therefore,

${liminf}_{m \to \infty} K_{n + 1} (x_{0}^{m}, x_{1 : n + 1}^{m}) (λ x_{n + 2} . f (x_{1 : n + 1}^{m}, x_{n + 2}))$

$= {liminf}_{m \to \infty} K_{n + 1} (x_{0}^{m}, x_{: n + 1}^{m}) (λ x_{n + 2} . f (x_{1 : n + 1}^{\infty}, x_{n + 2}))$

And then, by lower-semicontinuity for $K_{n + 1}$ , we have

$\geq K_{n + 1} (x_{0}^{\infty}, x_{1 : n + 1}^{\infty}) (λ x_{n + 2} . f (x_{1 : n + 1}^{\infty}, x_{n + 2}))$

and so, lower-semicontinuity of the function

$λ x_{0}, x_{1 : n + 1} . K_{n + 1} (x_{0}, x_{1 : n + 1}) (λ x_{n + 2} . f (x_{1 : n + 1}, x_{n + 2}))$

is shown. Time to return to the usual induction proof.

T1.2.6.2 For lower-semicontinuity in inputs, we first unpack the semidirect product. Fix a sequence $x_{0}^{m}$ which limits to $x_{0}^{\infty}$ .

${liminf}_{m \to \infty} K_{: n + 1} (x_{0}^{m}) (f)$

$= {liminf}_{m \to \infty} K_{: n} (x_{0}^{m}) (λ x_{1 : n + 1} . K_{n + 1} (x_{0}^{m}, x_{1 : n + 1}) (λ x_{n + 2} . f (x_{1 : n + 1}, x_{n + 2})))$

Since we showed that the function

$λ x_{0}, x_{1 : n + 1} . K_{n + 1} (x_{0}, x_{1 : n + 1}) (λ x_{n + 2} . f (x_{1 : n + 1}, x_{n + 2}))$

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

$= {liminf}_{m \to \infty} {sup}_{f^{'} \leq λ x_{0}, x_{1 : n + 1} . K_{n + 1} (x_{0}, x_{1 : n + 1}) (λ x_{n + 2} . f (x_{1 : n + 1}, x_{n + 2}))} K_{: n} (x_{0}^{m}) (λ x_{1 : n + 1} . f^{'} (x_{0}^{m}, x_{1 : n + 1}))$

For any individual $f^{'}$ , call it $f^{*}$ , we have

$\geq {liminf}_{m \to \infty} K_{: n} (x_{0}^{m}) (λ x_{1 : n + 1} . f^{*} (x_{0}^{m}, x_{1 : n + 1}))$

We now run through the same proof path as earlier again. The set ${x_{0}^{m}}_{m \in N ⊔ {\infty}}$ is compact in $X_{0}$ since it converges and we have the limit point added in. By the compact-shared CAS property for $K_{: n}$ (induction assumption), we can take any $ϵ$ and make a compact set $C_{ϵ}^{\prod_{i = 1}^{i = n + 1} X_{i}}$ which is a shared $ϵ$ -almost-support for all the $K_{: n} (x_{0}^{m})$ inframeasures. For any m, we can then apply the Lemma 2 (from LBIT) decomposition with the $C_{ϵ}^{\prod_{i = 1}^{i = n + 1} X_{i}}$ $ϵ$ -almost-support for all the $K_{: n} (x_{0}^{m})$ inframeasures (and 1-Lipschitzness of $K_{: n}$ by induction assumption) to get the inequality

$| K_{: n} (x_{0}^{m}) (λ x_{1 : n + 2} . f^{*} (x_{0}^{m}, x_{1 : n + 1})) - K_{: n} (x_{0}^{m}) (λ x_{1 : n + 2} . f^{*} (x_{0}^{\infty}, x_{1 : n + 1})) |$

$\leq {sup}_{x_{1 : n + 1} \in C_{ϵ}^{\prod_{i = 1}^{i = n + 1} X_{i}}} | f^{*} (x_{0}^{m}, x_{1 : n + 1}) - f (x_{0}^{\infty}, x_{1 : n + 1}) |$
$+ ϵ {sup}_{x_{1 : n + 1}} | f^{*} (x_{0}^{m}, x_{1 : n + 1}) - f^{*} (x_{0}^{\infty}, x_{1 : n + 1}) |$

That second term can be upper-bounded by $2 | | f | |$ , so doing that, we have

$\leq {sup}_{x_{1 : n + 1} \in C_{ϵ}^{\prod_{i = 1}^{i = n + 1} X_{i}}} | f^{*} (x_{0}^{m}, x_{1 : n + 1}) - f^{*} (x_{0}^{\infty}, x_{1 : n + 1}) | + 2 ϵ | | f | |$

Now, the set ${x_{0}^{m}}_{m \in N ⊔ {\infty}} \times C_{ϵ}^{\prod_{i = 1}^{i = n + 1} X_{i}}$ 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 $f$ only differing by $ϵ$ on them. Since $x_{0}^{m}$ limits to $x_{0}^{\infty}$ , for sufficiently large m, those two points will be within $δ$ of each either, so eventually

${sup}_{x_{1 : n + 1} \in C_{ϵ}^{\prod_{i = 1}^{i = n + 1} X_{i}}} | f^{*} (x_{0}^{m}, x_{1 : n + 1}) - f^{*} (x_{0}^{\infty}, x_{1 : n + 1}) |$

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

$| K_{: n} (x_{0}^{m}) (λ x_{1 : n + 2} . f^{*} (x_{0}^{m}, x_{1 : n + 1})) - K_{: n} (x_{0}^{m}) (λ x_{1 : n + 2} . f^{*} (x_{0}^{\infty}, x_{1 : n + 1})) | \leq ϵ + 2 ϵ | | f | |$

Since $ϵ$ can be arbitrary, we have that the sequences

$K_{: n} (x_{0}^{m}) (λ x_{1 : n + 2} . f^{*} (x_{0}^{m}, x_{1 : n + 1}))$

and

$K_{: n} (x_{0}^{m}) (λ x_{1 : n + 2} . f^{*} (x_{0}^{\infty}, x_{1 : n + 1}))$

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

${liminf}_{m \to \infty} K_{: n + 1} (x_{0}^{m}) (f)$

and for any $f^{*}$ fulfilling those bounding conditions for the sup, we have

$\geq {liminf}_{m \to \infty} K_{: n} (x_{0}^{m}) (λ x_{1 : n + 1} . f^{*} (x_{0}^{m}, x_{1 : n + 1}))$

and from our fresh new result, we then have

$= {liminf}_{m \to \infty} K_{: n} (x_{0}^{m}) (λ x_{1 : n + 1} . f^{*} (x_{0}^{\infty}, x_{1 : n + 1}))$

and, by lower-semicontinuity for $K_{: n}$ (induction assumption), we have

$\geq K_{: n} (x_{0}^{\infty}) (λ x_{1 : n + 1} . f^{*} (x_{0}^{\infty}, x_{1 : n + 1}))$

Since $f^{*}$ was arbitrary below

$λ x_{0}, x_{1 : n + 1} . K_{n + 1} (x_{0}, x_{1 : n + 1}) (λ x_{n + 2} . f (x_{1 : n + 1}, x_{n + 2}))$

this means that

${liminf}_{m \to \infty} K_{: n + 1} (x_{0}^{m}) (f)$

$\geq {sup}_{f^{'} \leq λ x_{0}, x_{1 : n + 1} . K_{n + 1} (x_{0}, x_{1 : n + 1}) (λ x_{n + 2} . f (x_{1 : n + 1}, x_{n + 2}))} K_{: n} (x_{0}^{\infty}) (λ x_{1 : n + 1} . f^{'} (x_{0}^{\infty}, x_{1 : n + 1}))$

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

$= K_{: n} (x_{0}^{\infty}) (λ x_{1 : n + 1} . K_{n + 1} (x_{0}^{\infty}, x_{1 : n + 1}) (λ x_{n + 2} . f (x_{1 : n + 1}, x_{n + 2})))$

$= K_{: n + 1} (x_{0}^{\infty}) (f)$

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

All our induction steps have been shown. First, for showing that all the $K_{: n} (x_{0})$ 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 $K_{: n}$ , 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 $K_{: n} (x_{0})$ 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 $K_{: n}$ are nice.

T1.3 We must show that if we go far enough out in the $K_{: n}$ , 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:

$\forall x_{0} \in X_{0}, n, m \in N, f \in C_{B} (\prod_{i = 1}^{i = n + 1} X_{i}) : K_{: n + m + 1} (x_{0}) (f) \geq K_{: n + m} (x_{0}) (f)$

Fix an arbitrary $x_{0}, n, m,$ and $f$ . Then, we can just go:

$K_{: n + m + 1} (x_{0}) (f)$

$= K_{: n + m} (x_{0}) (λ x_{1 : n + m + 1} . K_{n + m + 1} (x_{0}, x_{1 : n + m + 1}) (λ x_{n + m + 2} . f (x_{1 : n + 1})))$

Since $m \geq 0$ , that function at the end is a constant (doesn't depend on its input), so by Increasing Constants for $K_{n + m + 1}$ and Monotonicity for $K_{: n + m}$ , we have

$\geq K_{: n + m} (x_{0}) (λ x_{1 : n + m + 1} . f (x_{1 : n + 1})) = K_{: n + m} (x_{0}) (f)$

and we're done.

T1.4 Our desired result here is:

$\forall C^{X_{0}} \in K (X_{0}), ϵ > 0 : \exists C_{1 : \infty} [C^{X_{0}}, ϵ] \in K (\prod_{i = 1}^{\infty} X_{i}) : \forall n \in N, x_{0} \in C^{X_{0}}, f, f^{'} \in C_{B} (\prod_{i = 1}^{n + 1} X_{i}) :$
$f_{↓ p r_{1 : n + 1} (C_{1 : \infty} [C^{X_{0}}, ϵ])} = f_{↓ p r_{1 : n + 1} (C_{1 : \infty} [C^{X_{0}}, ϵ])}^{'}$
$\to | K_{: n} (x_{0}) (f) - K_{: n} (x_{0}) (f^{'}) | \leq ϵ (1 - \frac{1}{2^{n + 1}}) d (f, f^{'})$

This says that if you pick any compact subset of $X_{0}$ , you can make a compact subset of $\prod_{i = 1}^{\infty} X_{i}$ where the projection of it to coordinates 1 through $n + 1$ acts as a compact $ϵ (1 - \frac{1}{2^{n + 1}})$ -almost-support for all the $K_{: n} (x_{0})$ infradistributions when $x_{0}$ lies in your compact set $C^{X_{0}}$ .

The proof of this is word-for-word identical to the proof of this from LBIT, nothing changes. To recap the construction, fix some $C^{X_{0}}$ and $ϵ$ . Now, we recursively build up compact subsets of all the $X_{n}$ via the following inductive process.

$C_{i + 1} [C^{X_{0}}, ϵ] \subseteq X_{i + 1}$ is an arbitrary compact shared $\frac{ϵ}{2^{i + 1}}$ -almost-support for $K_{i} (x_{0 : i})$ where $x_{0 : i}$ is in $C^{X_{0}} \times \prod_{j = 1}^{j = i} C_{j} [C^{X_{0}}, ϵ]$ , these sets exist by compact-shared CAS for all the $K_{i}$ .

We define the abbreviations

$C_{1 : n} [C^{X_{0}}, ϵ] := \prod_{i = 1}^{i = n} C_{i} [C^{X_{0}}, ϵ]$

and

$C_{1 : \infty} [C^{X_{0}}, ϵ] := \prod_{i = 1}^{\infty} C_{i} [C^{X_{0}}, ϵ]$

This is the product of all the compact sets, and is compact. Notice the dependence of these on the starting compact set and $ϵ$ . Notice that the projection of $C_{1 : \infty} [C^{X_{0}}, ϵ]$ to coordinates 1 through n is exactly $C_{1 : n} [C^{X_{0}}, ϵ]$ .

Almost-Monotone Lemma: If ${K_{n}}_{n \in N}$ is a sequence of infrakernels fulfilling the niceness conditions, then

$\forall C^{X_{0}} \in K (X_{0}), ϵ > 0 : \exists ¯ ¯¯ ¯ C \in \prod_{i = 1}^{\infty} K (X_{i}) : \forall n, m \in N, x_{0} \in C^{X_{0}}, f \in C_{B} (\prod_{i = 1}^{\infty} X_{i}) :$
$K_{: n + m} (x_{0}) (λ x_{1 : n + m + 1} . {inf}_{x_{n + m + 2 : \infty} \in \prod_{i = n + m + 2}^{\infty} C_{i}} f (x_{1 : n + m + 1}, x_{n + m + 2 : \infty}))$
$\geq K_{: n} (x_{0}) (λ x_{1 : n + 1} . {inf}_{x_{n + 2 : \infty} \in \prod_{i = n + 2}^{\infty} C_{i}} f (x_{1 : n + 1}, x_{n + 2 : \infty})) - 4 ϵ | | f | |$

This says that for any compact subset of $X_{0}$ and $ϵ$ you name, I can find a "good" sequence of compact sets where the defining sequence for all the $K_{: \infty} (x_{0}) (f)$ quantities is "almost monotone". Every time the sequence hits a certain value (at time n), it will never again be able to dip below $4 ϵ | | f | |$ of that value as the sequence progresses. This proof progresses in 5 phases. The first phase is just doing some rewrites of our proof goal, the second, third, and fourth are showing setup results on functions undershooting other functions, and certain pairs of quantities being similar. The last phase is wrapping up the actual result.

L1.1 So, for the rewrites, let $C^{X_{0}}$ be an arbitrary compact subset of $X_{0}$ , and $ϵ$ be arbitrary. Our proof goal is now

$\exists ¯ ¯¯ ¯ C \in \prod_{i = 1}^{\infty} K (X_{i}) : \forall n, m \in N, x_{0} \in C^{X_{0}}, f \in C_{B} (\prod_{i = 1}^{\infty} X_{i}) :$
$K_{: n + m} (x_{0}) (λ x_{1 : n + m + 1} . {inf}_{x_{n + m + 2 : \infty} \in \prod_{i = n + m + 2}^{\infty} C_{i}} f (x_{1 : n + m + 1}, x_{n + m + 2 : \infty}))$
$\geq K_{: n} (x_{0}) (λ x_{1 : n + 1} . {inf}_{x_{n + 2 : \infty} \in \prod_{i = n + 2}^{\infty} C_{i}} f (x_{1 : n + 1}, x_{n + 2 : \infty})) - 4 ϵ | | f | |$

Let your sequence of compact sets be the $C_{i} [C^{X_{0}}, ϵ]$ sequence recursively defined from $C^{X_{0}}$ and $ϵ$ . Then our proof goal becomes

$\forall n, m \in N, x_{0} \in C^{X_{0}}, f \in C_{B} (\prod_{i = 1}^{\infty} X_{i}) :$
$K_{: n + m} (x_{0}) (λ x_{1 : n + m + 1} . {inf}_{x_{n + m + 2 : \infty} \in C_{n + m + 2 : \infty} [C^{X_{0}}, ϵ]} f (x_{1 : n + m + 1}, x_{n + m + 2 : \infty}))$
$\geq K_{: n} (x_{0}) (λ x_{1 : n + 1} . {inf}_{x_{n + 2 : \infty} \in C_{n + 2 : \infty} [C^{X_{0}}, ϵ]} f (x_{1 : n + 1}, x_{n + 2 : \infty})) - 4 ϵ | | f | |$

Let $n, m, x_{0}$ , and $f$ be arbitrary. Remember $x_{0}$ is in $C^{X_{0}}$ . Then our proof goal becomes

$K_{: n + m} (x_{0}) (λ x_{1 : n + m + 1} . {inf}_{x_{n + m + 2 : \infty} \in C_{n + m + 2 : \infty} [C^{X_{0}}, ϵ]} f (x_{1 : n + m + 1}, x_{n + m + 2 : \infty}))$
$\geq K_{: n} (x_{0}) (λ x_{1 : n + 1} . {inf}_{x_{n + 2 : \infty} \in C_{n + 2 : \infty} [C^{X_{0}}, ϵ]} f (x_{1 : n + 1}, x_{n + 2 : \infty})) - 4 ϵ | | f | |$

First, let's define some abbreviations for later. The function

$λ x_{1 : n + m + 1} . {inf}_{x_{n + m + 2 : \infty} \in C_{n + m + 2 : \infty} [C^{X_{0}}, ϵ]} f (x_{1 : n + m + 1}, x_{n + m + 2 : \infty})$

will be abbreviated as $f_{n + m + 1}^{♢}$ , and the function

$λ x_{1 : n + m + 1} . {inf}_{x_{n + 2 : \infty} \in C_{n + 2 : \infty} [C^{X_{0}}, ϵ]} f (x_{1 : n + 1}, x_{n + 2 : \infty})$

will be abbreviated as $f_{n + 1}^{♢}$ . Both of these functions are continuous, by section 1. We'll need three key results before beginning.

L1.2 Our first desired result is:

$\forall x_{1 : n + m + 1} \in C_{1 : n + m + 1} [C^{X_{0}}, ϵ] : f_{n + m + 1}^{♢} (x_{1 : n + m + 1}) \geq f_{n + 1}^{♢} (x_{1 : n + m + 1})$

Unpacking this proof target, it is

$\forall x_{1 : n + m + 1} \in C_{1 : n + m + 1} [C^{X_{0}}, ϵ] :$
${inf}_{x_{n + m + 2 : \infty} \in C_{n + m + 2 : \infty} [C^{X_{0}}, ϵ]} f (x_{1 : n + m + 1}, x_{n + m + 2 : \infty}) \geq {inf}_{x_{n + 2 : \infty} \in C_{n + 2 : \infty} [C^{X_{0}}, ϵ]} f (x_{1 : n + 1}, x_{n + 2 : \infty})$

If $m = 0$ , this result is trivial, we have equality. So now we'll assume $m > 0$ . Observe that it is now possible to factorize $C_{n + 2 : \infty} [C^{X_{0}}, ϵ]$ as $C_{n + 2 : n + m + 1} [C^{X_{0}}, ϵ] \times C_{n + m + 2 : \infty} [C^{X_{0}}, ϵ]$ , therefore,

${inf}_{x_{n + 2 : \infty} \in C_{n + 2 : \infty} [C^{X_{0}}, ϵ]} f (x_{1 : n + 1}, x_{n + 2 : \infty})$

turns into

${inf}_{x_{n + 2 : n + m + 1} \in C_{n + 2 : n + m + 1} [C^{X_{0}}, ϵ]} {inf}_{x_{n + m + 2 : \infty} \in C_{n + m + 2 : \infty} [C^{X_{0}}, ϵ]} f (x_{1 : n + 1}, x_{n + 2 : n + m + 1}, x_{n + m + 2 : \infty})$

which is just

${inf}_{x_{n + 2 : n + m + 1} \in C_{n + 2 : n + m + 1} [C^{X_{0}}, ϵ]} f_{n + m + 1}^{♢} (x_{n + 1}, x_{n + 2 : n + m + 1})$

Packing up $f_{n + m + 1}^{♢}$ on the left side of our proof target, our proof target is now

$\forall x_{1 : n + m + 1} \in C_{1 : n + m + 1} [C^{X_{0}}, ϵ] :$
$f_{n + m + 1}^{♢} (x_{1 : n + m + 1}) \geq {inf}_{x_{n + 2 : n + m + 1} \in C_{n + 2 : n + m + 1} [C^{X_{0}}, ϵ]} f_{n + m + 1}^{♢} (x_{n + 1}, x_{n + 2 : n + m + 1})$

And then, since we can factorize $C_{1 : n + m + 1} [C^{X_{0}}, ϵ]$ as $C_{1 : n + 1} [C^{X_{0}}, ϵ] \times C_{n + 2 : n + m + 1} [C^{X_{0}}, ϵ]$ , our proof target is now

$\forall x_{1 : n + 1}, x_{n + 2 : n + m + 1} \in C_{1 : n + 1} [C^{X_{0}}, ϵ] \times C_{n + 2 : n + m + 1} [C^{X_{0}}, ϵ] :$
$f_{n + m + 1}^{♢} (x_{1 : n + 1}, x_{n + 2 : n + m + 1}) \geq {inf}_{x_{n + 2 : n + m + 1}^{'} \in C_{n + 2 : n + m + 1} [C^{X_{0}}, ϵ]} f_{n + m + 1}^{♢} (x_{n + 1}, x_{n + 2 : n + m + 1}^{'})$

Which is obviously true. So, we have our first result of

$\forall x_{1 : n + m + 1} \in C_{1 : n + m + 1} [C^{X_{0}}, ϵ] : f_{n + m + 1}^{♢} (x_{1 : n + m + 1}) \geq f_{n + 1}^{♢} (x_{1 : n + m + 1})$

L1.3 Time for our second desired result. Our second desired result is that

$| K_{: n + m} (x_{0}) (sup (f_{n + m + 1}^{♢}, f_{n + 1}^{♢})) - K_{: n + m} (x_{0}) (f_{n + m + 1}^{♢}) | \leq 2 ϵ | | f | |$

For this, since $f_{n + m + 1}^{♢} \geq f_{n + 1}^{♢}$ on the set $C_{1 : n + m + 1} [C^{X_{0}}, ϵ]$ , as we showed in our first desired result, $sup (f_{n + m + 1}^{♢}, f_{n + 1}^{♢})$ equals $f_{n + m + 1}^{♢}$ on the set $C_{1 : n + m + 1} [C^{X_{0}}, ϵ]$ .

Further, $C_{1 : n + m + 1} [C^{X_{0}}, ϵ]$ is an $ϵ (1 - \frac{1}{2^{n + m + 1}})$ -almost-support for all the $K_{: n + m} (x_{0})$ with $x_{0} \in C^{X_{0}}$ , as our $x_{0}$ is. So, in particular, it's an $ϵ$ -almost-support. Accordingly, we have

$| K_{: n + m} (x_{0}) (sup (f_{n + m + 1}^{♢}, f_{n + 1}^{♢})) - K_{: n + m} (x_{0}) (f_{n + m + 1}^{♢}) |$

$\leq ϵ d (sup (f_{n + m + 1}^{♢}, f_{n + 1}^{♢}), f_{n + m + 1}^{♢})$

Now, for any input, either $f_{n + m + 1}^{♢}$ is higher (and so the distance between the functions at that point is 0), or $f_{n + 1}^{♢}$ is higher, and so the distance between the functions at that point is upper-bounded by $d (f_{n + m + 1}^{♢}, f_{n + 1}^{♢})$ . So, we have

$\leq ϵ d (f_{n + 1}^{♢}, f_{n + m + 1}^{♢})$

At this point, we recall that both $f_{n + m + 1}^{♢}$ and $f_{n + 1}^{♢}$ were just $f$ , but taking worst-case inputs past a certain point, so a trivial bound on this quantity is $2 | | f | |$ . So, our net result is

$| K_{: n + m} (x_{0}) (sup (f_{n + m + 1}^{♢}, f_{n + 1}^{♢})) - K_{: n + m} (x_{0}) (f_{n + m + 1}^{♢}) | \leq 2 ϵ | | f | |$

L1.4 And it's time to move onto our third setup result. Our desired third setup result is that

$| K_{: n + m} (x_{0}) (f_{n + 1}^{♢}) - K_{: n + m} (x_{0}) (inf (f_{n + m + 1}^{♢}, f_{n + 1}^{♢})) | \leq 2 ϵ | | f | |$

For this, since $f_{n + m + 1}^{♢} \geq f_{n + 1}^{♢}$ on the set $C_{1 : n + m + 1} [C^{X_{0}}, ϵ]$ , as we showed in our first desired result, $inf (f_{n + m + 1}^{♢}, f_{n + 1}^{♢})$ equals $f_{n + 1}^{♢}$ on the set $C_{1 : n + m + 1} [C^{X_{0}}, ϵ]$ .

$| K_{: n + m} (x_{0}) (f_{n + 1}^{♢}) - K_{: n + m} (x_{0}) (inf (f_{n + m + 1}^{♢}, f_{n + 1}^{♢})) |$

$\leq ϵ d (inf (f_{n + m + 1}^{♢}, f_{n + 1}^{♢}), f_{n + 1}^{♢})$

Now, for any input, either $f_{n + 1}^{♢}$ is lower (and so the distance between the functions at that point is 0), or $f_{n + m + 1}^{♢}$ is lower, and so the distance between the functions at that point is upper-bounded by $d (f_{n + m + 1}^{♢}, f_{n + 1}^{♢})$ . So, we have

$\leq ϵ d (f_{n + 1}^{♢}, f_{n + m + 1}^{♢})$

$| K_{: n + m} (x_{0}) (f_{n + 1}^{♢}) - K_{: n + m} (x_{0}) (inf (f_{n + m + 1}^{♢}, f_{n + 1}^{♢})) | \leq 2 ϵ | | f | |$

Now that everything's in place, we can start working on our actual result.

L1.5 Remember, our overall proof target at this stage is

We can reshuffle this proof target a little to get the equivalent statement

$K_{: n + m} (x_{0}) (λ x_{1 : n + m + 1} . {inf}_{x_{n + m + 2 : \infty} \in C_{n + m + 2 : \infty} [C^{X_{0}}, ϵ]} f (x_{1 : n + m + 1}, x_{n + m + 2 : \infty})) + 4 ϵ | | f | |$
$\geq K_{: n} (x_{0}) (λ x_{1 : n + 1} . {inf}_{x_{n + 2 : \infty} \in C_{n + 2 : \infty} [C^{X_{0}}, ϵ]} f (x_{1 : n + 1}, x_{n + 2 : \infty}))$

So let's get cracking on that inequality.

$K_{: n + m} (x_{0}) (λ x_{1 : n + m + 1} . {inf}_{x_{n + m + 2 : \infty} \in C_{n + m + 2 : \infty} [C^{X_{0}}, ϵ]} f (x_{1 : n + m + 1}, x_{n + m + 2 : \infty})) + 4 ϵ | | f | |$

First, we abbreviate it as

$= K_{: n + m} (x_{0}) (f_{n + m + 1}^{♢}) + 4 ϵ | | f | |$

Then, we apply our second sublemma we proved to get

$\geq K_{: n + m} (x_{0}) (f_{n + m + 1}^{♢}) + | K_{: n + m} (x_{0}) (sup (f_{n + m + 1}^{♢}, f_{n + 1}^{♢})) - K_{: n + m} (x_{0}) (f_{n + m + 1}^{♢}) | + 2 ϵ | | f | |$

And undo the absolute value to get

$\geq K_{: n + m} (x_{0}) (f_{n + m + 1}^{♢}) + K_{: n + m} (x_{0}) (sup (f_{n + m + 1}^{♢}, f_{n + 1}^{♢})) - K_{: n + m} (x_{0}) (f_{n + m + 1}^{♢}) + 2 ϵ | | f | |$

and cancel out to get

$= K_{: n + m} (x_{0}) (sup (f_{n + m + 1}^{♢}, f_{n + 1}^{♢})) + 2 ϵ | | f | |$

and then, by monotonicity we have

$\geq K_{: n + m} (x_{0}) (inf (f_{n + m + 1}^{♢}, f_{n + 1}^{♢})) + 2 ϵ | | f | |$

and apply our third sublemma we proved to get

$\geq K_{: n + m} (x_{0}) (inf (f_{n + m + 1}^{♢}, f_{n + 1}^{♢})) + | K_{: n + m} (x_{0}) (f_{n + 1}^{♢}) - K_{: n + m} (x_{0}) (inf (f_{n + m + 1}^{♢}, f_{n + 1}^{♢})) |$

And undo the absolute value

$\geq K_{: n + m} (x_{0}) (inf (f_{n + m + 1}^{♢}, f_{n + 1}^{♢})) + K_{: n + m} (x_{0}) (f_{n + 1}^{♢}) - K_{: n + m} (x_{0}) (inf (f_{n + m + 1}^{♢}, f_{n + 1}^{♢}))$

And cancel

$= K_{: n + m} (x_{0}) (f_{n + 1}^{♢})$

and at this point, we can unpack the inner function to get

$= K_{: n + m} (x_{0}) (λ x_{1 : n + m + 1} . {inf}_{x_{n + 2 : \infty} \in C_{n + 2 : \infty} [C^{X_{0}}, ϵ]} f (x_{1 : n + 1}, x_{n + 2 : \infty}))$

And then, we apply our Part 3 result that for functions which only depend on finitely many inputs, $K_{: n + m} (x_{0}) (f)$ is monotonically increasing, to get

$\geq K_{: n} (x_{0}) (λ x_{1 : n + 1} . {inf}_{x_{n + 2 : \infty} \in C_{n + 2 : \infty} [C^{X_{0}}, ϵ]} f (x_{1 : n + 1}, x_{n + 2 : \infty}))$

and we're done with the Almost-Monotone Lemma!

T1.5 Our aim here is to show that no matter what sequence of compact sets you have, they all limit to the same result. In order to do this, we'll have to show the result (letting $C_{i, 1}$ being your first sequence of nonempty compact sets to attempt to define the limit and $C_{i, 2}$ being your second sequence of nonempty compact sets, and abbreviating $C_{n + m + 2 : \infty, 1}$ as the product of the $C_{i, 1}$ from $n + m + 2$ to $\infty$ ) that,

$\forall x_{0} \in X_{0}_{1},_{2} \in \prod_{i = 1}^{\infty} K (X_{i}), f \in C_{B} (\prod_{i = 1}^{\infty} X_{i}), ϵ > 0 \exists n \in N \forall m \in N :$
$| K_{: n + m} (x_{0}) (λ x_{1 : n + m + 1} . {inf}_{x_{n + m + 2 : \infty} \in C_{n + m + 2 : \infty, 1}} f (x_{1 : n + m + 1}, x_{n + m + 2 : \infty}))$
$- K_{: n + m} (x_{0}) (λ x_{1 : n + m + 1} . {inf}_{x_{n + m + 2 : \infty} \in C_{n + m + 2 : \infty, 2}} f (x_{1 : n + m + 1}, x_{n + m + 2 : \infty})) | \leq ϵ (2 | | f | | + 1)$

In words, this is saying that for any two sequences of compact sets, there exists some threshold where if you pick any value of the defining sequence for $K_{: \infty} (x_{0}) (f)$ associated with using $C_{i, 1}$ as your compact sets, and the sequence associated with using $C_{i, 2}$ as your compact sets (as long as they're both past some shared threshold), they'll be close. So all choices of compact set must limit to each other, because $ϵ$ can be arbitrary.

Fix our $x_{0}, ϵ,_{1},_{2}, f$ (input value, closeness parameter, two sequences of compact sets, function), and now we'll find our n to make

$\forall m \in N : | K_{: n + m} (x_{0}) (λ x_{1 : n + m + 1} . {inf}_{x_{n + m + 2 : \infty} \in C_{n + m + 2 : \infty, 1}} f (x_{1 : n + m + 1}, x_{n + m + 2 : \infty}))$
$- K_{: n + m} (x_{0}) (λ x_{1 : n + m + 1} . {inf}_{x_{n + m + 2 : \infty} \in C_{n + m + 2 : \infty, 2}} f (x_{1 : n + m + 1}, x_{n + m + 2 : \infty})) | \leq ϵ (2 | | f | | + 1)$

true. Do it in the following way. Use ${x_{0}}$ as your compact seed set to invoke the technique in part 4 to construct your sequence $C_{i} [x_{0}, ϵ]$ , and then consider the set:

$\prod_{i = 1}^{\infty} (C_{i, 1} \cup C_{i, 2} \cup C_{i} [x_{0}, ϵ])$

A finite union of compact sets is compact, and the product of compact sets is compact. If we restrict $f$ to this set, it's uniformly continuous. In particular, using the standard product metric (which metrizes the product topology), defined as:

$d (x_{1 : \infty}, x_{1 : \infty}^{'}) = \sum_{i = 1}^{\infty} 2^{- i} inf (1, d_{X_{i}} (x_{i}, x_{i}^{'}))$

We can conclude that two sequences which agree up till time n must be, at most, distance $2^{- n}$ apart. Since $f$ restricted to our compact set of interest is uniformly continuous, there is some $δ$ difference in inputs that only leads to an $ϵ$ difference in values. Now we can define our n as ${log}_{2} (δ)$ .

Now that we've picked our n, let m be arbitrary. Our goal is to now prove:

$| K_{: n + m} (x_{0}) (λ x_{1 : n + m + 1} . {inf}_{x_{n + m + 2 : \infty} \in C_{n + m + 2 : \infty, 1}} f (x_{1 : n + m + 1}, x_{n + m + 2 : \infty}))$
$- K_{: n + m} (x_{0}) (λ x_{1 : n + m + 1} . {inf}_{x_{n + m + 2 : \infty} \in C_{n + m + 2 : \infty, 2}} f (x_{1 : n + m + 1}, x_{n + m + 2 : \infty})) | \leq ϵ (2 | | f | | + 1)$

First-up, we use that $C_{1 : n + m + 1} [x_{0}, ϵ]$ is an $ϵ$ -almost support for $K_{: n + m} (x_{0})$ , and 1-Lipschitzness, to apply Lemma 2 from LBIT to break up

$\leq {sup}_{x_{1 : n + m + 1} \in C_{1 : n + m + 1} [x_{0}, ϵ]} | {inf}_{x_{n + m + 2 : \infty} \in C_{n + m + 2 : \infty, 1}} f (x_{1 : n + m + 1}, x_{n + m + 2 : \infty})$
$- {inf}_{x_{n + m + 2 : \infty} \in C_{n + m + 2 : \infty, 2}} f (x_{1 : n + m + 1}, x_{n + m + 2 : \infty}) |$
$+ ϵ \cdot {sup}_{x_{1 : n + m + 1}} | {inf}_{x_{n + m + 2 : \infty} \in C_{n + m + 2 : \infty, 1}} f (x_{1 : n + m + 1}, x_{n + m + 2 : \infty})$
$- {inf}_{x_{n + m + 2 : \infty} \in C_{n + m + 2 : \infty, 2}} f (x_{1 : n + m + 1}, x_{n + m + 2 : \infty}) |$

We can upper-bound the second term with just $2 | | f | |$ , as the difference in values can't be any higher than the gap between the maximum value of $f$ and the minimum value of $f$ . As for the first term, note that if $x_{1 : n + m + 1} \in C_{1 : n + m + 1} [x_{0}, ϵ]$ and $x_{n + m + 2 : \infty} \in \prod_{i = n + m + 2}^{\infty} C_{i, 1}$ and $x_{n + m + 2 : \infty}^{'} \in \prod_{i = n + m + 2}^{\infty} C_{i, 2}$ (the latter two are the inf terms for a particular $x_{1 : n + m + 1}$ ) then we have

$x_{1 : n + m + 1}, x_{n + m + 2 : \infty} \in \prod_{i = 1}^{\infty} (C_{i, 1} \cup C_{i, 2} \cup C_{i} [x_{0}, ϵ])$

And same for $x_{1 : n + m + 1}, x_{n + m + 2 : \infty}^{'}$ . And these two points agree on $x_{1 : n + m + 1}$ , and n is large enough that the function itself varies by only $ϵ$ for any two points in that set which share the same prefix up to length n (and $x_{1 : n + m + 1}$ fulfills that) So, we can break down the upper bound as

$\leq ϵ + ϵ \cdot 2 | | f | | = ϵ (2 | | f | | + 1)$

And so we're done here and have our result.

Moving on, the statement

is the same as

$\forall x_{0} \in X_{0}_{1},_{2} \in \prod_{i = 1}^{\infty} K (X_{i}), f \in C_{B} (\prod_{i = 1}^{\infty} X_{i}) :$
${lim}_{n \to \infty} | K_{: n} (x_{0}) (λ x_{1 : n + 1} . {inf}_{x_{n + 2 : \infty} \in C_{n + 2 : \infty, 1}} f (x_{1 : n + 1}, x_{n + 2 : \infty}))$
$- K_{: n} (x_{0}) (λ x_{1 : n + 1} . {inf}_{x_{n + 2 : \infty} \in C_{n + 2 : \infty, 2}} f (x_{1 : n + 1}, x_{n + 2 : \infty})) | = 0$

So all the defining sequences for $K_{: \infty} (x_{0}) (f)$ limit to each other. We've got three possible cases. One is divergence, that liminf of the defining sequences goes to infinity. This is fine, the limit exists. One is convergence, that liminf and limsup are finite and equal, ie, the limit exists. This is fine. And the third case, that liminf and limsup aren't equal, must be ruled out. We'll invoke the Almost-Monotone Lemma, that

Specializing to the compact set consisting of a single arbitrary point $x_{0}$ , and recalling that the defining sequence for that was the $C_{i} [x_{0}, ϵ]$ sequence of almost-supports, and an arbitrary function $f$ , the lemma turns into

$\forall ϵ > 0, n, m \in N :$
$K_{: n + m} (x_{0}) (λ x_{1 : n + m + 1} . {inf}_{x_{n + m + 2 : \infty} \in C_{n + m + 2 : \infty} [x_{0}, ϵ]} f (x_{1 : n + m + 1}, x_{n + m + 2 : \infty}))$
$\geq K_{: n} (x_{0}) (λ x_{1 : n + 1} . {inf}_{x_{n + 2 : \infty} \in C_{n + 2 : \infty} [x_{0}, ϵ]} f (x_{1 : n + 1}, x_{n + 2 : \infty})) - 4 ϵ | | f | |$

Fix an arbitrary $ϵ$ and $n^{*}$ now. Just by definitions, we have

${liminf}_{n \to \infty} K_{: n} (x_{0}) (λ x_{1 : n + 1} . {inf}_{x_{n + 2 : \infty} \in C_{n + 2 : \infty} [x_{0}, ϵ]} f (x_{1 : n + 1}, x_{n + 2 : \infty}))$

$= {lim}_{n \to \infty} {inf}_{m} K_{: n + m} (x_{0}) (λ x_{1 : n + m + 1} . {inf}_{x_{n + m + 2 : \infty} \in C_{n + m + 2 : \infty} [x_{0}, ϵ]} f (x_{1 : n + m + 1}, x_{n + m + 2 : \infty}))$

This sequence is monotonically increasing, so a lower bound on this is

$\geq {inf}_{m} K_{: n^{*} + m} (x_{0}) (λ x_{1 : n^{*} + m + 1} . {inf}_{x_{n^{*} + m + 2 : \infty} \in C_{n^{*} + m + 2 : \infty} [x_{0}, ϵ]} f (x_{1 : n^{*} + m + 1}, x_{n^{*} + m + 2 : \infty}))$

and then, using $ϵ$ and $n^{*}$ in the Almost-Monotone Lemma, we have

$\geq K_{: n^{*}} (x_{0}) (λ x_{1 : n^{*} + 1} . {inf}_{x_{n^{*} + 2 : \infty} \in C_{n^{*} + 2 : \infty} [x_{0}, ϵ]} f (x_{1 : n^{*} + 1}, x_{n^{*} + 2 : \infty})) - 4 ϵ | | f | |$

Since $n^{*}$ was an arbitrary number, we have

${liminf}_{n \to \infty} K_{: n} (x_{0}) (λ x_{1 : n + 1} . {inf}_{x_{n + 2 : \infty} \in C_{n + 2 : \infty} [x_{0}, ϵ]} f (x_{1 : n + 1}, x_{n + 2 : \infty}))$

$\geq {sup}_{n^{*} \in N} K_{: n^{*}} (x_{0}) (λ x_{1 : n^{*} + 1} . {inf}_{x_{n^{*} + 2 : \infty} \in C_{n^{*} + 2 : \infty} [x_{0}, ϵ]} f (x_{1 : n^{*} + 1}, x_{n^{*} + 2 : \infty})) - 4 ϵ | | f | |$

and then we can lower-bound this by the limsup, yielding

$\geq {limsup}_{n \to \infty} K_{: n} (x_{0}) (λ x_{1 : n + 1} . {inf}_{x_{n + 2 : \infty} \in C_{n + 2 : \infty} [x_{0}, ϵ]} f (x_{1 : n + 1}, x_{n + 2 : \infty})) - 4 ϵ | | f | |$

Since the limsup is always equal or greater than the liminf, this implies that the limsup and liminf can be at most $4 ϵ | | f | |$ apart for this sequence. And since all the defining sequences limit to each other, they all have the same limsup and liminf. Since $ϵ$ was arbitrary, we get that all the defining sequences limit to each other, and either converge to a fixed number, or diverge to infinity. The infinite semidirect product is now well-defined, and we can use whichever sequence of compact sets is the most convenient.

T1.6 Showing the following infradistribution properties for the infinite semidirect product: monotonicity and concavity. Also, the 1-Lipschitz property and 1-normalization property and Constants Increase property, for 4/5 inframeasure properties, and 3/5 niceness properties.

For monotonicity, concavity, and 1-Lipschitzness, the exact proof from LBIT works.

For constants increasing, observe that regardless of n,

$K_{: n} (x_{0}) (λ x_{1 : n + 1} . {inf}_{x_{n + 2 : \infty} \in \prod_{i = n + 2}^{\infty} C_{i}} c) = K_{: n} (x_{0}) (c) \geq c$

Then, this bound transfers to the limit, so

$K_{: \infty} (x_{0}) (c) \geq c$

The same proof applies to 1-normalization, but with equality signs, if we plug in 1, and the limit of the all-1 sequence is always 1.

T1.7 Showing compact-shared compact-almost-support for $K_{: \infty}$ . Again, the exact proof from LBIT works here. We're up to 5/5 inframeasure properties, and 4/5 niceness properties for the infinite semidirect product.

T1.8 Our task is to show lower-semicontinuity for $K_{: \infty}$ . This will take some cunning. At the start, fix an $ϵ$ , we'll see why later. Our task is to show that

${liminf}_{m \to \infty} K_{: \infty} (x_{0}^{m}) (f) \geq K_{: \infty} (x_{0}^{\infty}) (f)$

For some arbitrary sequence of $x_{0}^{m}$ which limits to $x_{0}^{\infty}$ . What we can do is first unpack.

${liminf}_{m \to \infty} K_{: \infty} (x_{0}^{m}) (f)$

$= {liminf}_{m \to \infty} {lim}_{n \to \infty} K_{: n} (x_{0}^{m}) (λ x_{1 : n + 1} . {inf}_{x_{n + 2 : \infty} \in C_{n + 2 : \infty} [{x_{0}^{m}}_{m \in N ⊔ {\infty}}, ϵ]} f (x_{1 : n + 1}, x_{n + 2 : \infty}))$

Now, the sequence of sets we picked was important. It means we can now apply the Almost-Monotone Lemma. Regardless of m, the defining sequence for $K_{: \infty} (x_{0}^{m}) (f)$ is almost monotone now. We can fix a particular $n^{*}$ (arbitrary) to get a lower bound of

$\geq {liminf}_{m \to \infty} K_{: n^{*}} (x_{0}^{m}) (λ x_{1 : n^{*} + 1} . {inf}_{x_{n^{*} + 2 : \infty} \in C_{n^{*} + 2 : \infty} [{x_{0}^{m}}_{m \in N ⊔ {\infty}}, ϵ]} f (x_{1 : n^{*} + 1}, x_{n^{*} + 2 : \infty})) - 4 ϵ | | f | |$

And then, by lower-semicontinuity for $K_{: n^{*}}$ , which was already established by induction, we get

$\geq K_{: n^{*}} (x_{0}^{\infty}) (λ x_{1 : n^{*} + 1} . {inf}_{x_{n^{*} + 2 : \infty} \in C_{n^{*} + 2 : \infty} [{x_{0}^{m}}_{m \in N ⊔ {\infty}}, ϵ]} f (x_{1 : n^{*} + 1}, x_{n^{*} + 2 : \infty})) - 4 ϵ | | f | |$

But, since this holds for all $n^{*}$ , we can take a limit and get

${liminf}_{m \to \infty} K_{: \infty} (x_{0}^{m}) (f)$

$\geq {lim}_{n \to \infty} K_{: n} (x_{0}^{\infty}) (λ x_{1 : n + 1} . {inf}_{x_{n + 2 : \infty} \in C_{n + 2 : \infty} [{x_{0}^{m}}_{m \in N ⊔ {\infty}}, ϵ]} f (x_{1 : n + 1}, x_{n + 2 : \infty})) - 4 ϵ | | f | |$

$= K_{: \infty} (x_{0}^{\infty}) (f) - 4 ϵ | | f | |$

But since $ϵ$ can be arbitrarily small, we have

${liminf}_{m \to \infty} K_{: \infty} (x_{0}^{m}) (f) \geq K_{: \infty} (x_{0}^{\infty}) (f)$

and thus, lower-semicontinuity. And we're finally done!!

LESSWRONG
LW

LESSWRONG
LW

5

5

Ω 3

5

Ω 3