Theorem 1:Any sequence of infrakernels Kn:∏i=ni=0Xiik→Xn+1 which fulfill the niceness conditions have the infinite semidirect product K:∞ 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, x0:n↦Kn(x0:n)(f) is a lower-semicontinuous function.

2: 1-Lipschitzness for functions: For all x0:n, f↦Kn(x0:n)(f) is 1-Lipschitz.

3: Compact-shared compact-almost-support: For all compact sets C⊆∏i=ni=0Xi and ϵ, there is a compact set Cn+1⊆Xn+1 which is an ϵ-almost-support for all the Kn(x0:n) inframeasures where x0:n∈C.

4: Constants increase: For all x0:n and constant functions c, Kn(x0:n)(c)≥c.

5: 1-normalization (only for the [0,1] type signature): For all x0:n, Kn(x0:n)(1)=1

Now, K:∞:X0ik→∏∞i=1Xi is defined as: Fixing an arbitrary sequence of compact sets Ci⊆Xi,

Our task is to show that K:∞ 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(x0)(f) values monotonically increase as m does.

Part 4: Give a general procedure for taking a compact subset of the space X0 and making a compact subset of the space ∏∞i=1Xi 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 C0⊆X0 and pick a sequence of compact sets Ci for the defining sequence of the infinite semidirect product such that the defining sequence for all the K:∞(x0)(f) (with x0∈C0) is 4ϵ||f||-almost-monotone.

Part 5: Use parts 2, 3, and 4 to show that for any two different Ci 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:∞(x0)(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:∞(x0) (monotonicity and concavity), and show 1-Lipschitzness, increase of constants, and 1-normalization for K:∞ 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:∞. This also means that individual outputs of the kernel fulfill CAS, which verifies the last condition we need to conclude that K:∞(x0) 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 λx1:n+1.infxn+2:∞∈∏∞i=n+2Cif(x1:n+1,xn+2:∞) is continuous. This was already shown in "Less Basic Inframeasure Theory" (LBIT).

T1.2 The desired result is "if all the Kn 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:=K0 and we're assuming all the Kn have the niceness properties and are infrakernels, K:0 trivially fulfills them.

Time for the induction step. Remember that K:n+1(x0):=K:n(x0)⋉(λx1:n+1.Kn+1(x0,x1:n+1))

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

K:n+1(x0)(c)=K:n(x0)(λx1:n+1.Kn+1(x0,x1:n+1)(c))

And then by increasing constants for Kn+1, and monotonicity for K:n (induction assumption), we have

≥K:n(x0)(λx1:n+1.c)

Now just apply increasing constants for K:n (induction assumption) to get ≥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 CX0⊆X0, and find a compact set C∏i=n+2i=1Xiϵ⊆∏i=n+2i=1Xi where two functions f,f′ identical on the set only differ in expectation by ϵd(f,f′) according to all K:n+1(x0) with x0∈CX0.

Let x0∈CX0, and define the set C∏i=n+2i=1Xiϵ as C∏i=n+1i=1Xiϵ2×CXn+2ϵ2

where the first compact set is a shared ϵ2-almost-support for the K:n(x0) where x0∈CX0 (exists by compact-shared CAS for K:n, an induction assumption) and the second compact set is a shared ϵ2-almost-support for the Kn+1(x0,x1:n+1) where x0,x1:n+1 is in CX0×C∏i=n+1i=1Xiϵ2 (exists by compact-shared CAS for Kn+1, an assumed niceness condition). Let f,f′ be continuous and identical on C∏i=n+2i=1Xiϵ. 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 C∏i=n+1i=1Xiϵ2 as our compact set for the inner function. It was defined as a ϵ2-almost support for all K:n(x0) with x0∈CX0, and K:n is 1-Lipschitz (induction assumption). So our upper bound is:

For the first chunk, we can apply Lemma 2 from LBIT again, with CXn+2ϵ2 as our compact set, which is a ϵ2-almost support for all Kn+1(x0,x1:n+1) with x0,x1:n+1∈CX0×C∏i=n+1i=1Xiϵ2, and Kn+1 is 1-Lipschitz. So our upper bound is:

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

λx0,x1:n+1.Kn+1(x0,x1:n+1)(λxn+2.f(x1:n+1,xn+2))

is lower-semicontinuous. Fix a convergent sequence of inputs, xm0,xm1:n+1 which limit to x∞0,x∞1:n+1. First up, the set

{xm0,xm1:n+1}m∈N⊔{∞}

is compact in ∏i=n+1i=0Xi since it converges and we have the limit point added in. By the compact-shared CAS property for Kn+1, we can take any ϵ and make a compact set CXn+2ϵ⊆Xn+2 which is a shared ϵ-almost-support for all the Kn+1(xm0,xm1:n+1) inframeasures. For any m, we can then apply the Lemma 2 (from LBIT) decomposition with the CXn+2ϵϵ-almost-support for all the Kn+1(xm0,xm1:n+1) inframeasures (and 1-Lipschitzness of Kn+1) to get the inequality

Now, the set {xm0,xm1:n+1}m∈N⊔{∞}×CXn+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 xm1:n+1 limits to x∞1:n+1, for sufficiently large m, those two points will be within δ of each either, so eventually

supxn+2∈CXn+2ϵ|f(xm1:n+1,xn+2)−f(x∞1:n+1,xn+2)|

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

We now run through the same proof path as earlier again. The set {xm0}m∈N⊔{∞} is compact in X0 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∏i=n+1i=1Xiϵ which is a shared ϵ-almost-support for all the K:n(xm0) inframeasures. For any m, we can then apply the Lemma 2 (from LBIT) decomposition with the C∏i=n+1i=1Xiϵϵ-almost-support for all the K:n(xm0) inframeasures (and 1-Lipschitzness of K:n by induction assumption) to get the inequality

Now, the set {xm0}m∈N⊔{∞}×C∏i=n+1i=1Xiϵ 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 xm0 limits to x∞0, for sufficiently large m, those two points will be within δ of each either, so eventually

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

All our induction steps have been shown. First, for showing that all the K:n(x0) 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(x0) 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:

Since m≥0, that function at the end is a constant (doesn't depend on its input), so by Increasing Constants for Kn+m+1 and Monotonicity for K:n+m, we have

Theorem 1:Any sequence of infrakernelsKn:∏i=ni=0Xiik→Xn+1which fulfill the niceness conditions have the infinite semidirect productK:∞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, x0:n↦Kn(x0:n)(f) is a lower-semicontinuous function.2: 1-Lipschitzness for functions:For all x0:n, f↦Kn(x0:n)(f) is 1-Lipschitz.3: Compact-shared compact-almost-support:For all compact sets C⊆∏i=ni=0Xi and ϵ, there is a compact set Cn+1⊆Xn+1 which is an ϵ-almost-support for all the Kn(x0:n) inframeasures where x0:n∈C.4: Constants increase:For all x0:n and constant functions c, Kn(x0:n)(c)≥c.5: 1-normalization (only for the[0,1]type signature):For all x0:n, Kn(x0:n)(1)=1Now, K:∞:X0ik→∏∞i=1Xi is defined as: Fixing an arbitrary sequence of compact sets Ci⊆Xi,

K:∞(x0)(f):=limn→∞K:n(x0)(λx1:n+1infxn+2:∞∈∏∞i=n+2Cif(x1:n+1,xn+2:∞))

Our task is to show that K:∞ 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(x0)(f) values monotonically increase as m does.

Part 4: Give a general procedure for taking a compact subset of the space X0 and making a compact subset of the space ∏∞i=1Xi 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 C0⊆X0 and pick a sequence of compact sets Ci for the defining sequence of the infinite semidirect product such that the defining sequence for all the K:∞(x0)(f) (with x0∈C0) is 4ϵ||f||-almost-monotone.

Part 5: Use parts 2, 3, and 4 to show that for any two different Ci 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:∞(x0)(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:∞(x0) (monotonicity and concavity), and show 1-Lipschitzness, increase of constants, and 1-normalization for K:∞ 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:∞. This also means that individual outputs of the kernel fulfill CAS, which verifies the last condition we need to conclude that K:∞(x0) 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.1Our desired result is whether the function λx1:n+1.infxn+2:∞∈∏∞i=n+2Cif(x1:n+1,xn+2:∞)is continuous. This was already shown in "Less Basic Inframeasure Theory" (LBIT).

T1.2The desired result is "if all the Kn 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:=K0 and we're assuming all the Kn have the niceness properties and are infrakernels, K:0 trivially fulfills them.

Time for the induction step. Remember that K:n+1(x0):=K:n(x0)⋉(λx1:n+1.Kn+1(x0,x1:n+1))

T1.2.1Proof of monotonicity: Assume f′≥f. ThenK:n+1(x0)(f′)=K:n(x0)(λx1:n+1.Kn+1(x0,x1:n+1)(λxn+2.f′(x1:n+1,xn+2)))

And the same goes for f so if we could prove

K:n(x0)(λx1:n+1.Kn+1(x0,x1:n+1)(λxn+2.f′(x1:n+1,xn+2)))

≥K:n(x0)(λx1:n+1.Kn+1(x0,x1:n+1)(λxn+2.f(x1:n+1,xn+2)))

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

∀x1:n+1:Kn+1(x0,x1:n+1)(λxn+2.f′(x1:n+1,xn+2))

≥Kn+1(x0,x1:n+1)(λxn+2.f(x1:n+1,xn+2))

Letting x1:n+1 be arbitrary, by applying monotonicity for Kn+1, we'd have that result if

∀xn+2:f′(x1:n+1,xn+2)≥f(x1:n+1,xn+2)

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

T1.2.2Proof of concavity:K:n+1(x0)(pf+(1−p)f′)

=K:n(x0)(λx1:n+1.Kn+1(x0,x1:n+1)(λxn+2.pf(x1:n+1,xn+2)+(1−p)f′(x1:n+1,xn+2)))

and then, by concavity for all Kn+1, and monotonicity for K:n (by induction assumption), we have

≥K:n(x0)(λx1:n+1.pKn+1(x0,x1:n+1)(λxn+2.f(x1:n+1,xn+2))

+(1−p)Kn+1(x0,x1:n+1)(λxn+2.f′(x1:n+1,xn+2)))

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

≥pK:n(x0)(λx1:n+1.Kn+1(x0,x1:n+1)(λxn+2.f(x1:n+1,xn+2)))

+(1−p)K:n(x0)(λx1:n+1.Kn+1(x0,x1:n+1)(λxn+2.f′(x1:n+1,xn+2)))

and then this packs up as

=pK:n+1(x0)(f)+(1−p)K:n+1(f′)

and concavity inducts on up.

T1.2.3Proof of 1-Lipschitzness: we have|K:n+1(x0)(f)−K:n+1(x0)(f′)|

=|K:n(x0)(λx1:n+1.Kn+1(x0,x1:n+1)(λxn+2.f(x1:n+1,xn+2)))

−K:n(x0)(λx1:n+1.Kn+1(x0,x1:n+1)(λxn+2.f′(x1:n+1,xn+2)))|

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

≤supx1:n+1|Kn+1(x0,x1:n+1)(λxn+2.f(x1:n+1,xn+2))

−Kn+1(x0,x1:n+1)(λxn+2.f′(x1:n+1,xn+2))|

And by 1-Lipschitzness for Kn+1, we have

≤supx1:n+1,xn+2|f(x1:n+1,xn+2)−f′(x1:n+1,xn+2)|=d(f,f′)

And 1-Lipschitzness inducts on up.

T1.2.4Proof of increasing constants (and 1-normalization): We haveK:n+1(x0)(c)=K:n(x0)(λx1:n+1.Kn+1(x0,x1:n+1)(c))

And then by increasing constants for Kn+1, and monotonicity for K:n (induction assumption), we have

≥K:n(x0)(λx1:n+1.c)

Now just apply increasing constants for K:n (induction assumption) to get ≥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.5Proof of the compact-shared CAS property: Our task is to take an arbitrary compact set CX0⊆X0, and find a compact set C∏i=n+2i=1Xiϵ⊆∏i=n+2i=1Xi where two functions f,f′ identical on the set only differ in expectation by ϵd(f,f′) according to all K:n+1(x0) with x0∈CX0.Let x0∈CX0, and define the set C∏i=n+2i=1Xiϵ as C∏i=n+1i=1Xiϵ2×CXn+2ϵ2

where the first compact set is a shared ϵ2-almost-support for the K:n(x0) where x0∈CX0 (exists by compact-shared CAS for K:n, an induction assumption) and the second compact set is a shared ϵ2-almost-support for the Kn+1(x0,x1:n+1) where x0,x1:n+1 is in CX0×C∏i=n+1i=1Xiϵ2 (exists by compact-shared CAS for Kn+1, an assumed niceness condition). Let f,f′ be continuous and identical on C∏i=n+2i=1Xiϵ. Then, we have

|K:n+1(x0)(f)−K:n+1(x0)(f′)|

=|K:n(x0)(λx1:n+1.Kn+1(x0,x1:n+1)(λxn+2.f(x1:n+1,xn+2)))

−K:n(x0)(λx1:n+1.Kn+1(x0,x1:n+1)(λxn+2.f′(x1:n+1,xn+2)))|

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∏i=n+1i=1Xiϵ2 as our compact set for the inner function. It was defined as a ϵ2-almost support for all K:n(x0) with x0∈CX0, and K:n is 1-Lipschitz (induction assumption). So our upper bound is:

≤supx1:n+1∈C∏i=n+1i=1Xiϵ2|Kn+1(x0,x1:n+1)(λxn+2.f(x1:n+1,xn+2))

−Kn+1(x0,x1:n+1)(λxn+2.f′(x1:n+1,xn+2))|

+ϵ2⋅supx1:n+1|Kn+1(x0,x1:n+1)(λxn+2.f(x1:n+1,xn+2))

−Kn+1(x0,x1:n+1)(λxn+2.f′(x1:n+1,xn+2))|

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

≤supx1:n+1∈C∏i=n+1i=1Xiϵ2|Kn+1(x0,x1:n+1)(λxn+2.f(x1:n+1,xn+2))

−Kn+1(x0,x1:n+1)(λxn+2.f′(x1:n+1,xn+2))|

+ϵ2⋅supx1:n+1,xn+2|f(x1:n+1,xn+2)−f′(x1:n+1,xn+2)|

For the first chunk, we can apply Lemma 2 from LBIT again, with CXn+2ϵ2 as our compact set, which is a ϵ2-almost support for all Kn+1(x0,x1:n+1) with x0,x1:n+1∈CX0×C∏i=n+1i=1Xiϵ2, and Kn+1 is 1-Lipschitz. So our upper bound is:

≤supx1:n+1∈C∏i=n+1i=1Xiϵ2(supxn+2∈CXn+2ϵ2|f(x1:n+1,xn+2)−f′(x1:n+1,xn+2)|

+ϵ2⋅supxn+2|f(x1:n+1,xn+2)−f′(x1:n+1,xn+2)|)

+ϵ2⋅supx1:n+1,xn+2|f(x1:n+1,xn+2)−f′(x1:n+1,xn+2)|

Now, since f and f′ are identical on C∏i=n+1i=1Xiϵ2×CXn+2ϵ2 that first term just vanishes, yielding

=supx1:n+1∈C∏i=n+1i=1Xiϵ2(ϵ2⋅supxn+2|f(x1:n+1,xn+2)−f′(x1:n+1,xn+2)|)

+ϵ2⋅supx1:n+1,xn+2|f(x1:n+1,xn+2)−f′(x1:n+1,xn+2)|

We upper-bound this by

≤ϵ2supx1:n+1,xn+2|f(x1:n+1,xn+2)−f′(x1:n+1,xn+2)|

+ϵ2⋅supx1:n+1,xn+2|f(x1:n+1,xn+2)−f′(x1:n+1,xn+2)|

Which then clearly just reduces to

=ϵd(f,f′)

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

T1.2.6.1Proof of lower-semicontinuity: We'll start by taking an extended detour to show that the functionλx0,x1:n+1.Kn+1(x0,x1:n+1)(λxn+2.f(x1:n+1,xn+2))

is lower-semicontinuous. Fix a convergent sequence of inputs, xm0,xm1:n+1 which limit to x∞0,x∞1:n+1. First up, the set

{xm0,xm1:n+1}m∈N⊔{∞}

is compact in ∏i=n+1i=0Xi since it converges and we have the limit point added in. By the compact-shared CAS property for Kn+1, we can take any ϵ and make a compact set CXn+2ϵ⊆Xn+2 which is a shared ϵ-almost-support for all the Kn+1(xm0,xm1:n+1) inframeasures. For any m, we can then apply the Lemma 2 (from LBIT) decomposition with the CXn+2ϵ ϵ-almost-support for all the Kn+1(xm0,xm1:n+1) inframeasures (and 1-Lipschitzness of Kn+1) to get the inequality

|Kn+1(xm0,xm1:n+1)(λxn+2.f(xm1:n+1,xn+2))−Kn+1(xm0,xm1:n+1)(λxn+2.f(x∞1:n+1,xn+2))|

≤supxn+2∈CXn+2ϵ|f(xm1:n+1,xn+2)−f(x∞1:n+1,xn+2)|

+ϵsupxn+2|f(xm1:n+1,xn+2)−f(x∞1:n+1,xn+2)|

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

≤supxn+2∈CXn+2ϵ|f(xm1:n+1,xn+2)−f(x∞1:n+1,xn+2)|+2ϵ||f||

Now, the set {xm0,xm1:n+1}m∈N⊔{∞}×CXn+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 xm1:n+1 limits to x∞1:n+1, for sufficiently large m, those two points will be within δ of each either, so eventually

supxn+2∈CXn+2ϵ|f(xm1:n+1,xn+2)−f(x∞1:n+1,xn+2)|

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

|Kn+1(xm0,xm1:n+1)(λxn+2.f(xm1:n+1,xn+2))−Kn+1(xm0,xm1:n+1)(λxn+2.f(x∞1:n+1,xn+2))|

≤ϵ+2ϵ||f||

Since ϵ can be arbitrary, we have that the sequences

Kn+1(xm0,xm1:n+1)(λxn+2.f(xm1:n+1,xn+2))

and

Kn+1(xm0,xm1:n+1)(λxn+2.f(x∞1:n+1,xn+2))

limit to each other. Therefore,

liminfm→∞Kn+1(xm0,xm1:n+1)(λxn+2.f(xm1:n+1,xn+2))

=liminfm→∞Kn+1(xm0,xm:n+1)(λxn+2.f(x∞1:n+1,xn+2))

And then, by lower-semicontinuity for Kn+1, we have

≥Kn+1(x∞0,x∞1:n+1)(λxn+2.f(x∞1:n+1,xn+2))

and so, lower-semicontinuity of the function

λx0,x1:n+1.Kn+1(x0,x1:n+1)(λxn+2.f(x1:n+1,xn+2))

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

T1.2.6.2For lower-semicontinuity in inputs, we first unpack the semidirect product. Fix a sequence xm0 which limits to x∞0.liminfm→∞K:n+1(xm0)(f)

=liminfm→∞K:n(xm0)(λx1:n+1.Kn+1(xm0,x1:n+1)(λxn+2.f(x1:n+1,xn+2)))

Since we showed that the function

λx0,x1:n+1.Kn+1(x0,x1:n+1)(λxn+2.f(x1:n+1,xn+2))

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

=liminfm→∞supf′≤λx0,x1:n+1.Kn+1(x0,x1:n+1)(λxn+2.f(x1:n+1,xn+2))K:n(xm0)(λx1:n+1.f′(xm0,x1:n+1))

For any individual f′, call it f∗, we have

≥liminfm→∞K:n(xm0)(λx1:n+1.f∗(xm0,x1:n+1))

We now run through the same proof path as earlier again. The set {xm0}m∈N⊔{∞} is compact in X0 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∏i=n+1i=1Xiϵ which is a shared ϵ-almost-support for all the K:n(xm0) inframeasures. For any m, we can then apply the Lemma 2 (from LBIT) decomposition with the C∏i=n+1i=1Xiϵ ϵ-almost-support for all the K:n(xm0) inframeasures (and 1-Lipschitzness of K:n by induction assumption) to get the inequality

|K:n(xm0)(λx1:n+2.f∗(xm0,x1:n+1))−K:n(xm0)(λx1:n+2.f∗(x∞0,x1:n+1))|

≤supx1:n+1∈C∏i=n+1i=1Xiϵ|f∗(xm0,x1:n+1)−f(x∞0,x1:n+1)|

+ϵsupx1:n+1|f∗(xm0,x1:n+1)−f∗(x∞0,x1:n+1)|

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

≤supx1:n+1∈C∏i=n+1i=1Xiϵ|f∗(xm0,x1:n+1)−f∗(x∞0,x1:n+1)|+2ϵ||f||

Now, the set {xm0}m∈N⊔{∞}×C∏i=n+1i=1Xiϵ 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 xm0 limits to x∞0, for sufficiently large m, those two points will be within δ of each either, so eventually

supx1:n+1∈C∏i=n+1i=1Xiϵ|f∗(xm0,x1:n+1)−f∗(x∞0,x1:n+1)|

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

|K:n(xm0)(λx1:n+2.f∗(xm0,x1:n+1))−K:n(xm0)(λx1:n+2.f∗(x∞0,x1:n+1))|≤ϵ+2ϵ||f||

Since ϵ can be arbitrary, we have that the sequences

K:n(xm0)(λx1:n+2.f∗(xm0,x1:n+1))

and

K:n(xm0)(λx1:n+2.f∗(x∞0,x1:n+1))

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

liminfm→∞K:n+1(xm0)(f)

=liminfm→∞supf′≤λx0,x1:n+1.Kn+1(x0,x1:n+1)(λxn+2.f(x1:n+1,xn+2))K:n(xm0)(λx1:n+1.f′(xm0,x1:n+1))

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

≥liminfm→∞K:n(xm0)(λx1:n+1.f∗(xm0,x1:n+1))

and from our fresh new result, we then have

=liminfm→∞K:n(xm0)(λx1:n+1.f∗(x∞0,x1:n+1))

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

≥K:n(x∞0)(λx1:n+1.f∗(x∞0,x1:n+1))

Since f∗ was arbitrary below

λx0,x1:n+1.Kn+1(x0,x1:n+1)(λxn+2.f(x1:n+1,xn+2))

this means that

liminfm→∞K:n+1(xm0)(f)

≥supf′≤λx0,x1:n+1.Kn+1(x0,x1:n+1)(λxn+2.f(x1:n+1,xn+2))K:n(x∞0)(λx1:n+1.f′(x∞0,x1:n+1))

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

=K:n(x∞0)(λx1:n+1.Kn+1(x∞0,x1:n+1)(λxn+2.f(x1:n+1,xn+2)))

=K:n+1(x∞0)(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(x0) 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(x0) 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.3We 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:∀x0∈X0,n,m∈N,f∈CB(∏i=n+1i=1Xi):K:n+m+1(x0)(f)≥K:n+m(x0)(f)

Fix an arbitrary x0,n,m, and f. Then, we can just go:

K:n+m+1(x0)(f)

=K:n+m(x0)(λx1:n+m+1.Kn+m+1(x0,x1:n+m+1)(λxn+m+2.f(x1:n+1)))

Since m≥0, that function at the end is a constant (doesn't depend on its input), so by Increasing Constants for Kn+m+1 and Monotonicity for K:n+m, we have

≥K:n+m(x0)(λx1:n+m+1.f(x1:n+1))=K:n+m(x0)(f)

and we're done.

T1.4Our desired result here is:∀CX0∈K(X0),ϵ>0:∃C1:∞[CX0,ϵ]∈K(∏∞i=1Xi):∀n∈N,x0∈CX0,f,f′∈CB(∏n+1i=1Xi):

f↓pr1:n+1(C1:∞[CX0,ϵ])=f′↓pr1:n+1(C1:∞[