Proofs Theorem 4

Diffractor

Theorem 4: Pseudocausal IPOMDP's: If an infra-POMDP has a transition kernel $K : S \times A i k \to O \times S$ which fulfills the niceness conditions, and there's a starting infradistribution $ψ \in □ S$ , unrolling it into an infrakernel via $Θ (π) := p r_{(A \times O)^{ω} *} (ψ ⋉ K_{: \infty}^{π})$ has the infrakernel $Θ$ being pseudocausal and fulfilling all belief function conditions except for normalization.

This takes a whole lot of work to show. The proof breaks down into two phases. The first is showing that the $K_{n}^{π}$ fulfill the niceness conditions (which splits into four subphases of showing 1-Lipschitzness, lower-semicontinuity, compact-shared CAS, and moving constants up/mapping 1 to 1). This is the easy part to do. The second phase is much longer. It splits into five pieces, where we show our list of conditions for $Θ$ . Our list of conditions to show is:

1:The $Θ (π)$ have a uniform upper bound on their Lipschitz constants.

2: $π \mapsto Θ (π) (U)$ is lower-semicontinuous for all $U$

3: $Θ (π)$ is supported entirely on histories compatible with $π$ .

4: All the $Θ (π)$ agree on the value of 1 (or infinity).

5: $Θ$ is pseudocausal.

Parts 1 and 4 can be done with little trouble, but parts 2, 3, and 5 split into additional pieces. To show pseudocausality, ie, condition 5, we have to start with our proof goal and keep rewriting it into an easier form, until we get something we can knock out with an induction proof, which splits into a base case and an induction step. To show sensible supports, ie, part 3, we have to split it into three parts, there's one induction proof for the finite $K_{: n}^{π}$ , showing sensible supports for $K_{: \infty}^{π}$ , and then finally extending this to the result we actually want, which is fairly easy.

And then there's lower-semicontinuity, part 2, which is an absolute nightmare. This splits into three parts. One is explicitly constructing a sequence of compact sets to use in the Almost-Monotone Lemma for any policy whatsoever, and then there's trying to show that $π \mapsto (ψ ⋉ K_{: \infty}^{π}) (f)$ is lower-semimicontinuous which requires a massive amount of messing around with integrals and limits, and then it's pretty easy to show lower-semicontinuity for $Θ$ from there.

T4.1 Our first order of business is showing the five niceness conditions for all the $K_{n}^{π}$ infrakernels, so we can take the infinite semidirect product and show that $K_{: \infty}^{π}$ inherits the five niceness conditions (from the proof of Theorem 1).

Remember that $K_{n}^{π}$ is defined as

$K_{n}^{π} (s_{0}, a o s_{1 : n}) := δ_{π (a o_{1 : n})} ⋉ (λ a . K (s_{n}, a))$

Obviously it produces inframeasures, since $K$ does.

T4.1.1 For lower-semicontinuity in the input, we have

${liminf}_{m \to \infty} K_{n}^{π} (s_{0}^{m}, a o s_{1 : n}^{m}) (f)$

$= {liminf}_{m \to \infty} (δ_{π (a o_{1 : n}^{m})} ⋉ (λ a . K (s_{n}^{m}, a))) (f)$

$= {liminf}_{m \to \infty} K (s_{n}^{m}, π (a o_{1 : n}^{m})) (λ o, s . f (π (a o_{1 : n}^{m}), o, s))$

and then, as $a o s_{1 : n}^{m}$ limits to $a o s_{1 : n}^{\infty}$ , we have $a o_{1 : n}^{m} = a o_{1 : n}^{\infty}$ forever after some finite $m$ , because $\prod_{i = 1}^{i = n} (A \times O)$ is a finite space. So, it turns into

$= {liminf}_{m \to \infty} K (s_{n}^{m}, π (a o_{1 : n}^{\infty})) (λ o, s . f (π (a o_{1 : n}^{\infty}), o, s))$

and then, by lower-semicontinuity for K (one of the niceness conditions)

$\geq K (s_{n}^{\infty}, π (a o_{1 : n}^{\infty})) (λ o, s . f (π (a o_{1 : n}^{\infty}), o, s))$

and then we pack this back up as

$= δ_{π (a o_{1 : n}^{m})} ⋉ (λ a . K (s_{n}^{\infty}, a)) (f) = K_{n}^{π} (s_{0}^{\infty}, a o s_{1 : n}^{\infty}) (f)$

and lower-semicontinuity has been shown.

T4.1.2 For 1-Lipschitzness, observe that $δ_{π (a o_{1 : n})} ⋉ (λ a . K (s_{n}, a))$ is 1-Lipschitz because $K$ is 1-Lipschitz, and this is the semidirect product of a 1-Lipschitz (all probability distributions are 1-Lipschitz, and this is a dirac-delta distribution) infradistribution with a 1-Lipschitz infrakernel.

T4.1.3 For compact-shared compact-almost-support, observe that $(s_{0}, a o s_{1 : n}) \mapsto (s_{n}, π (a o_{1 : n}))$ is a continuous function, so any compact subset of $S \times (A \times O \times S)^{n}$ (input to $K_{n}^{π}$ ) maps to a compact subset of $S \times A$ (corresponding inputs for $K$ ). Then, we can apply compact-shared compact-almost-support for $K$ (one of the niceness conditions) to get a compact almost-support on $O \times S$ , and take the product of that subset with all of $A$ itself, to get a shared-compact almost-support for $K_{n}^{π}$ .

T4.1.4 For mapping constants to above constants, we have

$K_{n}^{π} (s_{0}, a o s_{1 : n}) (c) = (δ_{π (a o_{1 : n})} ⋉ (λ a . K (s_{n}, a))) (c)$

$= δ_{π (a o_{1 : n})} (λ a . K (s_{n}, a) (c)) = K (s_{n}, π (a o_{1 : n})) (c) \geq c$

By increasing constants for $K$ (one of the niceness conditions). This same proof works with equality when $c = 1$ , because of the "map 1 to 1" condition on the $[0, 1]$ type signature. So all the $K_{n}^{π}$ have the niceness properties, and we can form the infinite semidirect product at all, and the infinite semidirect product inherits these niceness conditions.

T4.2 Now we can get working on showing the belief function conditions.

T4.2.1 For showing a bounded Lipschitz constant, we have

$| Θ (π) (U) - Θ (π) (U^{'}) | = | p r_{(A \times O)^{ω} *} (ψ ⋉ K_{: \infty}^{π}) (U) - p r_{(A \times O)^{ω} *} (ψ ⋉ K_{: \infty}^{π}) (U^{'}) |$

$= | ψ (λ s_{0} . K_{: \infty}^{π} (s_{0}) (λ a o s_{1 : \infty} . U (a o_{1 : \infty}))) - ψ (λ s_{0} . K_{: \infty}^{π} (s_{0}) (λ a o s_{1 : \infty} . U^{'} (a o_{1 : \infty}))) |$

and then since $ψ$ is an infradistribution, it must have a finite Lipschitz constant, $λ^{⊙}$ . So we then get

$\leq λ^{⊙} \cdot {sup}_{s_{0}} | K_{: \infty}^{π} (s_{0}) (λ a o s_{1 : \infty} . U (a o_{1 : \infty})) - K_{: \infty}^{π} (s_{0}) (λ a o s_{1 : \infty} . U^{'} (a o_{1 : \infty})) |$

and then, since all the $K_{: \infty}^{π} (s_{0})$ are 1-Lipschitz (infinite semidirect product has niceness conditions), we get

$\leq λ^{⊙} {sup}_{a o s_{1 : \infty}} | U (a o_{1 : \infty}) - U^{'} (a o_{1 : \infty}) | = λ^{⊙} \cdot d (U, U^{'})$

and we're done, we showed a Lipschitz bound on the $Θ (π)$ that is uniform in $π$ .

T4.2.2 Now for lower-semicontinuity for $Θ$ , which is the extremely hard one.

The way this proof will work is that we'll first show a variant of the Almost-Monotone Lemma that works for all the $K_{: \infty}^{π}$ infrakernels simultaneously. Then, using that, we'll show that

$π \mapsto (ψ ⋉ K_{: \infty}^{π}) (f)$ is lower-semicontinuous. And then, it's pretty easy to wrap up and get that

$π \mapsto Θ (π) (U)$ is lower-semicontinuous, from that.

T4.2.2.1 Anyways, our first goal is a variant of the Almost-Monotone Lemma. The particular variant we're searching for, specialized to our particular case, is:

$\forall C^{S} \in K (S), ϵ > 0 : \exists ¯ ¯¯ ¯ C \in \prod_{i = 1}^{\infty} K (A \times O \times S) : \forall π \in Π, n, m \in N, s_{0} \in C^{S}, f \in C_{B} ((A \times O \times S)^{ω}) :$
$K_{: n + m}^{π} (s_{0}) (λ a o s_{1 : n + m + 1} . {inf}_{a o s_{n + m + 2 : \infty} \in \prod_{i = n + m + 2}^{\infty} C_{i}} f (a o s_{1 : n + m + 1}, a o s_{n + m + 2 : \infty}))$
$\geq K_{: n}^{π} (s_{0}) (λ a o s_{1 : n + 1} . {inf}_{a o s_{n + 2 : \infty} \in \prod_{i = n + 2}^{\infty} C_{i}} f (a o s_{1 : n + 1}, a o s_{n + 2 : \infty})) - 4 ϵ | | f | |$

We let our $C^{S}$ be an arbitrary compact subset of states, and $ϵ$ be arbitrary.

Now, let's assume there's a sequence of compact sets C $_{i}^{⊤} [C^{S}, ϵ]$ where, regardless of n or $π$ , $C_{1 : n + 1}^{⊤} [C^{S}, ϵ]$ is a shared $ϵ (1 - \frac{1}{2^{n + 1}})$ -almost-support for all the $K_{: n}^{π} (s_{0})$ inframeasures (where $s_{0} \in C^{S}$ ).

Then our proof goal becomes

$\forall π \in Π, n, m \in N, s_{0} \in C^{S}, f \in C_{B} ((A \times O \times S)^{ω}) :$
$K_{: n + m}^{π} (s_{0}) (λ a o s_{1 : n + m + 1} . {inf}_{a o s_{n + m + 2 : \infty} \in C_{n + m + 2 : \infty}^{⊤} [C^{S}, ϵ]} f (a o s_{1 : n + m + 1}, a o s_{n + m + 2 : \infty}))$
$\geq K_{: n}^{π} (s_{0}) (λ a o s_{1 : n + 1} . {inf}_{a o s_{n + 2 : \infty} \in C_{n + 2 : \infty}^{⊤} [C^{S}, ϵ]} f (a o s_{1 : n + 1}, a o s_{n + 2 : \infty})) - 4 ϵ | | f | |$

The proof of the Almost-Monotone Lemma goes through perfectly fine, the key part where our choice of compact sets matters is in the ability to make the assumption that $C_{1 : n + m + 1}^{⊤} [C^{S}, ϵ]$ is an $ϵ (1 - \frac{1}{2^{n + m + 1}})$ -almost-support for all the $K_{: n + m}^{π} (s_{0})$ with $s_{0} \in C^{S}$ , as our $s_{0}$ is. And we assumed our sequence of compact sets fulfilled that property.

So, where we're at is that our variant of the Almost-Monotone-Lemma works, as long as our assumption works out, that there's a sequence of compact sets $C_{i}^{⊤} [C^{S}, ϵ]$ where, regardless of n or $π$ or $s_{0} \in C^{S}$ , $C_{1 : n + 1}^{⊤} [C^{S}, ϵ]$ is a $ϵ (1 - \frac{1}{2^{n + 1}})$ -almost-support for $K_{: n}^{π} (s_{0})$ .

In order to get our variant of the AML to go through, we really need to prove that there is such a sequence, for any $ϵ$ and $C^{S}$ . For this, we'll be looking at a function

$Ξ : (0, \infty) \times A \times K (S) \to K (O, S)$

What this does is that $Ξ (ϵ, a, C^{S})$ is defined to return a compact subset of $O \times S$ which is an $ϵ$ -almost-support for all the $K (a, s)$ inframeasures, when $s \in C^{S}$ . There are always compact subsets like this for any input because of shared almost-compact-support for the infrakernel $K$ (one of the assumed niceness conditions), so there does indeed exist a function $Ξ$ with these properties.

Then, we recursively define the $C_{i}^{⊤} [C^{S}, ϵ]$ as:

$C_{1}^{⊤} [C^{S}, ϵ] := A \times ⋃_{a} Ξ (\frac{ϵ}{2}, a, C^{S})$

and

$C_{n + 1}^{⊤} [C^{S}, ϵ] := A \times ⋃_{a} Ξ (\frac{ϵ}{2^{n + 1}}, a, p r_{S_{n}} (C_{1 : n}^{⊤} [C^{S}, ϵ]))$

All these sets are compact, by induction. For the first one, since $Ξ$ always returns compact sets, we're taking a finite union of compact sets (is compact), and taking the product with a finite set (is compact). For induction up, since the product of compact sets is compact, $C_{1 : n}^{⊤} [C^{S}, ϵ]$ is compact, and then projections of compact sets are compact, so then $Ξ$ returns a compact set, and again, we take a finite union of compact sets and then the product with a compact set to make another compact set.

Now, let's get started on showing that C^{\top}_{1:n+1}[C^{S},\eps] is an \eps\left(1-\frac{1}{2^{n+1}}\right)-almost-support for K^{\pi}_{:n}(s_0), for arbitrary \pi and s_0\in C^{S}. This proof will proceed by induction.

For the base-case, we want that $C_{1}^{⊤} [C^{S}, ϵ]$ is a $\frac{ϵ}{2}$ -almost-support for $K_{: n}^{π} (s_{0})$ with $s_{0} \in C^{S}$ . Well, assume $f, f^{'}$ are equal on $C_{1}^{⊤} [C^{S}, ϵ]$ , and $s_{0} \in C^{S}$ .

$| K_{: 0}^{π} (s_{0}) (f) - K_{: 0}^{π} (s_{0}) (f^{'}) | = | K_{0}^{π} (s_{0}) (f) - K_{0}^{π} (s_{0}) (f^{'}) |$

$= | (δ_{π ()} ⋉ (λ a . K (s_{0}, a))) (λ a, o, s . f (a, o, s)) - (δ_{π ()} ⋉ (λ a . K (s_{0}, a))) (λ a, o, s . f^{'} (a, o, s)) |$

$= | K (s_{0}, π ()) (λ o, s . f (π (), o, s)) - K (s_{0}, π ()) (λ o, s . f^{'} (π (), o, s)) |$

Now, $Ξ (\frac{ϵ}{2}, π (), C^{S})$ is a $\frac{ϵ}{2}$ -almost-support for $K (s_{0}, π ())$ because $s_{0} \in C^{S}$ , so we can apply Lemma 2 from LBIT, and 1-Lipschitzness of $K$ to split this up as

$\leq {sup}_{o, s \in Ξ (\frac{ϵ}{2}, π (), C^{S})} | f (π (), o, s) - f^{'} (π (), o, s) | + \frac{ϵ}{2} {sup}_{o, s} | f (π (), o, s) - f^{'} (π (), o, s) |$

That second term can be upper bounded by $d (f, f^{'})$ , so we get an upper bound of

$\leq {sup}_{o, s \in Ξ (\frac{ϵ}{2}, π (), C^{S})} | f (π (), o, s) - f^{'} (π (), o, s) | + \frac{ϵ}{2} d (f, f^{'})$

and then we observe that since $f = f^{'}$ on $C_{1}^{⊤} [C^{S}, ϵ]$ , and that set is defined as $A \times ⋃_{a} Ξ (\frac{ϵ}{2}, a, C^{S})$ , we have that they agree on ${π ()} \times Ξ (\frac{ϵ}{2}, π (), C^{S})$

So that term turns into 0, the two functions are equal on our set of interest, so our net upper bound is

$\leq \frac{ϵ}{2} d (f, f^{'})$

Showing that $C_{1}^{⊤} [C^{S}, ϵ]$ is a $\frac{ϵ}{2}$ -almost support for all the $K_{: 0}^{π} (s_{0})$ , where $π$ is arbitrary and s_0\in C^{S}.

Now for induction. We want to show that $C_{1 : n + 2}^{⊤} [C^{S}, ϵ]$ is a $ϵ (1 - \frac{1}{2^{n + 2}})$ -almost-support for $K_{: n + 1}^{π} (s_{0})$ with $s_{0} \in C^{S}$ , assuming that $C_{1 : n + 1}^{⊤} [C^{S}, ϵ]$ is a $ϵ (1 - \frac{1}{2^{n + 1}})$ -almost-support for $K_{: n}^{π} (s_{0})$ with $s_{0} \in C^{S}$ .

To begin, assume $f, f^{'}$ are equal on $C_{1 : n + 2}^{⊤} [C^{S}, ϵ]$ and $s_{0} \in C^{S}$ . Then we can go:

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

$= | K_{: n}^{π} (s_{0}) (λ a o s_{1 : n + 1} . K_{n + 1}^{π} (s_{0}, a o s_{1 : n + 1}) (λ a, o, s . f (a o s_{1 : n + 1}, a, o, s)))$
$- K_{: n}^{π} (s_{0}) (λ a o s_{1 : n + 1} . K_{n + 1}^{π} (s_{0}, a o s_{1 : n + 1}) (λ a, o, s . f^{'} (a o s_{1 : n + 1}, a, o, s))) |$

and then unpack to get

$= | K_{: n}^{π} (s_{0}) (λ a o s_{1 : n + 1} . (δ_{π (a o_{1 : n + 1})} ⋉ (λ a . K (s_{n + 1}, a))) (λ a, o, s . f (a o s_{1 : n + 1}, a, o, s)))$
$- K_{: n}^{π} (s_{0}) (λ a o s_{1 : n + 1} . (δ_{π (a o_{1 : n + 1})} ⋉ (λ a . K (s_{n + 1}, a))) (λ a, o, s . f^{'} (a o s_{1 : n + 1}, a, o, s))) |$

and unpack the semidirect product and substitute the dirac-delta value in to get

$= | K_{: n}^{π} (s_{0}) (λ a o s_{1 : n + 1} . K (s_{n + 1}, π (a o_{1 : n + 1})) (λ o, s . f (a o s_{1 : n + 1}, π (a o_{1 : n + 1}), o, s)))$
$- K_{: n}^{π} (s_{0}) (λ a o s_{1 : n + 1} . K (s_{n + 1}, π (a o_{1 : n + 1})) (λ o, s . f^{'} (a o s_{1 : n + 1}, π (a o_{1 : n + 1}), o, s))) |$

We apply a Lemma 2 from LBIT decomposition, with $C_{1 : n + 1}^{⊤} [C^{S}, ϵ]$ as an $ϵ (1 - \frac{1}{2^{n + 1}})$ -almost support for $K_{: n}^{π} (s_{0})$ , which works by induction assumption. Since $K_{: n}^{π} (s_{0})$ is also 1-Lipschitz (the niceness conditions we already know), the Lemma 2 upper bound breaks down as

$\leq {sup}_{a o s_{1 : n + 1} \in C_{1 : n + 1}^{⊤} [C^{S}, ϵ]} | K (s_{n + 1}, π (a o_{1 : n + 1})) (λ o, s . f (a o s_{1 : n + 1}, π (a o_{1 : n + 1}), o, s))$
$- K (s_{n + 1}, π (a o_{1 : n + 1})) (λ o, s . f^{'} (a o s_{1 : n + 1}, π (a o_{1 : n + 1}), o, s)) |$
$+ ϵ (1 - \frac{1}{2^{n + 1}}) {sup}_{a o s_{1 : n + 1}} | K (s_{n + 1}, π (a o_{1 : n + 1})) (λ o, s . f (a o s_{1 : n + 1}, π (a o_{1 : n + 1}), o, s))$
$- K (s_{n + 1}, π (a o_{1 : n + 1})) (λ o, s . f^{'} (a o s_{1 : n + 1}, π (a o_{1 : n + 1}), o, s)) |$

By 1-Lipschitzness of $K$ , we get an upper-bound of

$\leq {sup}_{a o s_{1 : n + 1} \in C_{1 : n + 1}^{⊤} [C^{S}, ϵ]} | K (s_{n + 1}, π (a o_{1 : n + 1})) (λ o, s . f (a o s_{1 : n + 1}, π (a o_{1 : n + 1}), o, s))$
$- K (s_{n + 1}, π (a o_{1 : n + 1})) (λ o, s . f^{'} (a o s_{1 : n + 1}, π (a o_{1 : n + 1}), o, s)) |$
$+ ϵ (1 - \frac{1}{2^{n + 1}}) {sup}_{a o s_{1 : n + 1}} {sup}_{o, s} | f (a o s_{1 : n + 1}, π (a o_{1 : n + 1}), o, s) - f^{'} (a o s_{1 : n + 1}, π (a o_{1 : n + 1}), o, s) |$

And then this is upper-boundable by $d (f, f^{'})$ , so we get

Now, for that top term, we know that $s_{n + 1}$ comes from $p r_{S_{n + 1}} (C_{1 : n + 1}^{⊤} [C^{S}, ϵ])$ . We apply another Lemma 2 decomposition on $K$ this time, with the compact set of interest being

$Ξ (\frac{ϵ}{2^{n + 2}}, π (a o_{1 : n + 1}), p r_{S_{n + 1}} (C_{1 : n + 1}^{⊤} [C^{S}, ϵ]))$

which is a $ϵ (\frac{1}{2^{n + 2}})$ -almost-support for $K (s_{n + 1}, π (a o_{1 : n + 1}))$ . Pairing this with 1-Lipschitzness of $K$ , we have an upper bound of

$\leq {sup}_{a o s_{1 : n + 1} \in C_{1 : n + 1}^{⊤} [C^{S}, ϵ]} ({sup}_{o, s \in Ξ (\frac{ϵ}{2^{n + 2}}, π (a o_{1 : n + 1}), p r_{S_{n + 1}} (C_{1 : n + 1}^{⊤} [C^{S}, ϵ]))}$
$| f (a o s_{1 : n + 1}, π (a o_{1 : n + 1}), o, s) - f^{'} (a o s_{1 : n + 1}, π (a o_{1 : n + 1}), o, s) |$
$+ \frac{ϵ}{2^{n + 2}} {sup}_{o, s} | f (a o s_{1 : n + 1}, π (a o_{1 : n + 1}), o, s) - f^{'} (a o s_{1 : n + 1}, π (a o_{1 : n + 1}), o, s) |)$
$+ ϵ (1 - \frac{1}{2^{n + 1}}) d (f, f^{'})$

That second term is upper-bounded by $d (f, f^{'})$ no matter what, so we have

$\leq {sup}_{a o s_{1 : n + 1} \in C_{1 : n + 1}^{⊤} [C^{S}, ϵ]} ({sup}_{o, s \in Ξ (\frac{ϵ}{2^{n + 2}}, π (a o_{1 : n + 1}), p r_{S_{n + 1}} (C_{1 : n + 1}^{⊤} [C^{S}, ϵ]))}$
$| f (a o s_{1 : n + 1}, π (a o_{1 : n + 1}), o, s) - f^{'} (a o s_{1 : n + 1}, π (a o_{1 : n + 1}), o, s) |$
$+ \frac{ϵ}{2^{n + 2}} d (f, f^{'})) + ϵ (1 - \frac{1}{2^{n + 1}}) d (f, f^{'})$

Pull out the constant and combine, to get

$= {sup}_{a o s_{1 : n + 1} \in C_{1 : n + 1}^{⊤} [C^{S}, ϵ]} ({sup}_{o, s \in Ξ (\frac{ϵ}{2^{n + 2}}, π (a o_{1 : n + 1}), p r_{S_{n + 1}} (C_{1 : n + 1}^{⊤} [C^{S}, ϵ]))}$
$| f (a o s_{1 : n + 1}, π (a o_{1 : n + 1}), o, s) - f^{'} (a o s_{1 : n + 1}, π (a o_{1 : n + 1}), o, s) |)$
$+ ϵ (1 - \frac{1}{2^{n + 2}}) d (f, f^{'})$

Now, $f, f^{'}$ were assumed to agree on $C_{1 : n + 2}^{⊤} [C^{S}, ϵ]$ , which factors as

$C_{1 : n + 1}^{⊤} [C^{S}, ϵ] \times C_{n + 2}^{⊤} [C^{S}, ϵ]$

and then expands as

$C_{1 : n + 1}^{⊤} [C^{S}, ϵ] \times (A \times ⋃_{a} Ξ (\frac{ϵ}{2^{n + 2}}, a, p r_{S_{n + 1}} (C_{1 : n + 1}^{⊤} [C^{S}, ϵ])))$

which all our $a o s_{1 : n + 1}, π (a o_{1 : n + 1}), o, s$ we're feeding in lie within. So those functions are identical for those inputs, and our upper-bound just reduces to

$= ϵ (1 - \frac{1}{2^{n + 2}}) d (f, f^{'})$

Which witnesses that $C_{1 : n + 2}^{⊤} [C^{S}, ϵ]$ is a $ϵ (1 - \frac{1}{2^{n + 2}})$ -almost-support for any $K_{: n + 1}^{π} (s_{0})$ (arbitrary $π$ ) as long as $s_{0} \in C^{S}$ . So our induction step goes off without a hitch, and we now know that the $C_{i}^{⊤} [C^{S}, ϵ]$ sequence is suitable to get our modification of the Almost-Monotone-Lemma to work out. We have the result

In particular, since any defining sequence for $K_{: \infty}^{π} (s_{0})$ has an actual limit, this can be trivially reshuffled to attain the result:

$\forall π \in Π, n^{*} \in N, s_{0} \in C^{S}, f \in C_{B} ((A \times O \times S)^{ω}) :$
${lim}_{n \to \infty} K_{: n}^{π} (s_{0}) (λ a o s_{1 : n + 1} . {inf}_{a o s_{n + 2 : \infty} \in C_{n + 2 : \infty}^{⊤} [C^{S}, ϵ]} f (a o s_{1 : n + 1}, a o s_{n + 2 : \infty}))$
$\geq K_{: n^{*}}^{π} (s_{0}) (λ a o s_{1 : n^{*} + 1} . {inf}_{a o s_{n^{*} + 2 : \infty} \in C_{n^{*} + 2 : \infty}^{⊤} [C^{S}, ϵ]} f (a o s_{1 : n^{*} + 1}, a o s_{n^{*} + 2 : \infty})) - 4 ϵ | | f | |$

And remember, the sequence of compact sets only depends on $C^{S}$ and $ϵ$ , not on the policy. This works for any policy. Now that we have this result in the bag, we can move on to phase 2.

T4.2.2.2 For phase 2, we'll show that $π \mapsto (ψ ⋉ K_{: \infty}^{π}) (f)$ is lower-semicontinuous, and dear lord this is going to be hard and take a lot of integrals and limits to show. We start with

${liminf}_{m \to \infty} (ψ ⋉ K_{: \infty}^{π_{m}}) (f)$

Which unpacks as

$= {liminf}_{m \to \infty} ψ (λ s_{0} . K_{: \infty}^{π_{m}} (s_{0}) (λ a o s_{1 : \infty} . f (s_{0}, a o s_{1 : \infty})))$

If this liminf is infinity, we're just done, infinity beats everything. So we'll be assuming that it settles down to a finite value. We can unpack the $ψ$ as a challenge of picking points in $Ψ$ , so we get

$= {liminf}_{m \to \infty} ({inf}_{(m, b) \in Ψ} (m (λ s_{0} . K_{: \infty}^{π_{m}} (s_{0}) (λ a o s_{1 : \infty} . f (s_{0}, a o s_{1 : \infty}))) + b))$

And, since we can pick amongst minimal points, we can rewrite this as

$= {liminf}_{m \to \infty} ({inf}_{(m, b) \in Ψ^{min}} (m (λ s_{0} . K_{: \infty}^{π_{m}} (s_{0}) (λ a o s_{1 : \infty} . f (s_{0}, a o s_{1 : \infty}))) + b))$

In the $[0, 1]$ case, the set of minimal points is precompact. In the $R$ case, it may not be precompact, but the only way it fails to be precompact is having b values running off to infinity. Said $λ s_{0} . K_{: \infty}^{π_{m}} (s_{0}) (f)$ function can't be unbounded below, because it is above $K_{: \infty}^{π_{m}} (s_{0}) (- | | f | |)$ , and infinite semidirect products map constants to greater than their usual value, and $K_{: \infty}^{π_{m}} (s_{0})$ fulfills this condition. Thus, if the b value of a selected minimal point is far higher than the finite liminf value plus $λ^{⊙} | | f | |$ , the value said minimal point assigns to the function of interest is far higher than the true minimal value. So, when minimizing, we can restrict to a compact subset of $Ψ$ to attain the min, call it $C^{Ψ}$ . With this, we get

$= {liminf}_{m \to \infty} ({inf}_{(m, b) \in C^{Ψ}} (m (λ s_{0} . K_{: \infty}^{π_{m}} (s_{0}) (λ a o s_{1 : \infty} . f (s_{0}, a o s_{1 : \infty}))) + b))$

And then we unpack this as an integral.

$= liminf m \to \infty (inf (m, b) \in C^{Ψ} (\int_{S} (λ s_{0} . K_{: \infty}^{π_{m}} (s_{0}) (λ a o s_{1 : \infty} . f (s_{0}, a o s_{1 : \infty}))) d m + b))$

Now, we can pass to two subsequences. First, we can pass to a subsequence of the m that actually limits to the liminf value. On this subsequence, the policies still limit to $π_{\infty}$ . Also, for each member of this subsequence, we can find an true minimizing $(m, b)$ pair for it since we're minimizing the lower-semicontinuous function

$(m, b) \mapsto \int_{S} (λ s_{0} . K_{: \infty}^{π_{m}} (s_{0}) (λ a o s_{1 : \infty} . f (s_{0}, a o s_{1 : \infty}))) d m + b$

over a compact set. Said function is lower-semicontinuous because

$λ s_{0} . K_{: \infty}^{π_{m}} (s_{0}) (λ a o s_{1 : \infty} . f (s_{0}, a o s_{1 : \infty}))$

is lower-semicontinuous, it's one of the niceness properties that the infinite infrakernel inherits.

Since we're selecting a-measures from the compact set $C^{Ψ}$ , we can find a subsequence of our subsequence where the a-measures converge. Now we'll be using i as our index, and using it to index the $(m, b)$ pairs. The limit a-measure is $(m_{\infty}, b_{\infty})$ . So, we have a rewrite as

$= lim i \to \infty (\int_{S} (λ s_{0} . K_{: \infty}^{π_{i}} (s_{0}) (λ a o s_{1 : \infty} . f (s_{0}, a o s_{1 : \infty}))) d m_{i} + b_{i})$

Further, all numbers in this limit are finite, because we're operating in the case where the liminf is finite, and i indexes a subsequence which actually limits to the liminf. For said limit, $b_{i}$ limits to $b_{\infty}$ , so we can pull that out of the limit, to get

$= lim i \to \infty (\int_{S} (λ s_{0} . K_{: \infty}^{π_{i}} (s_{0}) (λ a o s_{1 : \infty} . f (s_{0}, a o s_{1 : \infty}))) d m_{i}) + b_{\infty}$

At this point, since the $m_{i}$ limit to $m_{\infty}$ , the set of the measure components ${m_{i}}_{i \in N ⊔ {\infty}}$ is compact in the space of measures on $S$ . In particular, this implies that there is some compact set $C^{S} \subseteq S$ where all the $m_{i}$ only have $ϵ$ or less measure outside said set (a necessary condition for precompactness of a set of measures)

Now, we split the measures $m_{i}$ into the component of measure on $C^{S}$ , and the component outside of it.

$= lim i \to \infty (\int_{S} (λ s_{0} . K_{: \infty}^{π_{i}} (s_{0}) (λ a o s_{1 : \infty} . f (s_{0}, a o s_{1 : \infty}))) d m_{i, C^{S}}$
$+ \int_{S} (λ s_{0} . K_{: \infty}^{π_{i}} (s_{0}) (λ a o s_{1 : \infty} . f (s_{0}, a o s_{1 : \infty}))) d m_{i, \neg C^{S}}) + b_{\infty}$

Because $C^{S}$ is a compact subset of $S$ , we can use it as a seed set for our $C_{n}^{⊤} [C^{S}, ϵ]$ sequence that attains almost-monotonicity. To economize on space for the lines to fit, we'll write

${inf}_{a o s_{n + 2 : \infty} \in C_{n + 2 : \infty}^{⊤} [C^{S}, ϵ]} f (s_{0}, a o s_{1 : n + 1}, a o s_{n + 2 : \infty})$

as just

${inf}_{C_{n + 2 : \infty}^{⊤} [C^{S}, ϵ]} f (s_{0}, a o s_{1 : n + 1}, a o s_{n + 2 : \infty})$

We unpack the defining limit of the infinite semidirect product with our relevant sequence of compact sets to get

We'll now be splitting up the second integral as two more integrals. Fix an arbitrary $n^{*}$ .

$= lim i \to \infty (\int_{S} (λ s_{0} . lim n \to \infty (K_{: n}^{π_{i}} (s_{0}) (λ a o s_{1 : n + 1} . inf C_{n + 2 : \infty}^{⊤} [C^{S}, ϵ] f (s_{0}, a o s_{1 : n + 1}, a o s_{n + 2 : \infty})))) d m_{i, C^{S}}$
$+ \int_{S} (λ s_{0} . K_{: n^{*}}^{π_{i}} (s_{0}) (λ a o s_{1 : n^{*} + 1} . inf C_{n^{*} + 2 : \infty}^{⊤} [C^{S}, ϵ] f (s_{0}, a o s_{1 : n^{*} + 1}, a o s_{n^{*} + 2 : \infty}))) d m_{i, \neg C^{S}}$
$+ \int_{S} (λ s_{0} . lim n \to \infty (K_{: n}^{π_{i}} (s_{0}) (λ a o s_{1 : n + 1} . inf C_{n + 2 : \infty}^{⊤} [C^{S}, ϵ] f (s_{0}, a o s_{1 : n + 1}, a o s_{n + 2 : \infty})))$
$- K_{: n^{*}}^{π_{i}} (s_{0}) (λ a o s_{1 : n^{*} + 1} . {inf}_{C_{n^{*} + 2 : \infty}^{⊤} [C^{S}, ϵ]} f (s_{0}, a o s_{1 : n^{*} + 1}, a o s_{n^{*} + 2 : \infty}))) d m_{i, \neg C^{S}}) + b_{\infty}$

We're really in the weeds here, let's see if we can make any dent whatsoever. What we'll be showing is that, regardless of $s_{0}$ ,

${lim}_{n \to \infty} (K_{: n}^{π_{i}} (s_{0}) (λ a o s_{1 : n + 1} . {inf}_{C_{n + 2 : \infty}^{⊤} [C^{S}, ϵ]} f (s_{0}, a o s_{1 : n + 1}, a o s_{n + 2 : \infty})))$
$- K_{: n^{*}}^{π_{i}} (s_{0}) (λ a o s_{1 : n^{*} + 1} . {inf}_{C_{n^{*} + 2 : \infty}^{⊤} [C^{S}, ϵ]} f (s_{0}, a o s_{1 : n^{*} + 1}, a o s_{n^{*} + 2 : \infty})) \geq - 2 | | f | |$

It is exceptionally important to note here that we can't just throw our variant of the Almost-Monotone Lemma at this, because we don't have a promise that $s_{0} \in C^{S}$ .

An easy way to show this is to show it for all $n \geq n^{*}$ . So let $n \geq n^{*}$ . Then, our proof goal is that

$K_{: n}^{π_{i}} (s_{0}) (λ a o s_{1 : n + 1} . {inf}_{C_{n + 2 : \infty}^{⊤} [C^{S}, ϵ]} f (s_{0}, a o s_{1 : n + 1}, a o s_{n + 2 : \infty}))$
$- K_{: n^{*}}^{π_{i}} (s_{0}) (λ a o s_{1 : n^{*} + 1} . {inf}_{C_{n^{*} + 2 : \infty}^{⊤} [C^{S}, ϵ]} f (s_{0}, a o s_{1 : n^{*} + 1}, a o s_{n^{*} + 2 : \infty})) \geq - 2 | | f | |$

First, observe that the functions

$λ a o s_{1 : n + 1} . {inf}_{C_{n + 2 : \infty}^{⊤} [C^{S}, ϵ]} f (s_{0}, a o s_{1 : n + 1}, a o s_{n + 2 : \infty})$

and

$λ a o s_{1 : n + 1} . {inf}_{C_{n^{*} + 2 : \infty}^{⊤} [C^{S}, ϵ]} f (s_{0}, a o s_{1 : n^{*} + 1}, a o s_{n^{*} + 2 : \infty})$

can only differ on the same input by at most $2 | | f | |$ . Since the finite stages are all 1-Lipschitz or less, we have

$\geq K_{: n}^{π_{i}} (s_{0}) (λ a o s_{1 : n + 1} . {inf}_{C_{n^{*} + 2 : \infty}^{⊤} [C^{S}, ϵ]} f (s_{0}, a o s_{1 : n^{*} + 1}, a o s_{n^{*} + 2 : \infty})) - 2 | | f | |$
$- K_{: n^{*}}^{π_{i}} (s_{0}) (λ a o s_{1 : n^{*} + 1} . {inf}_{C_{n^{*} + 2 : \infty}^{⊤} [C^{S}, ϵ]} f (s_{0}, a o s_{1 : n^{*} + 1}, a o s_{n^{*} + 2 : \infty}))$

And then, by monotonicity of the infrakernel stages for functions which cut off at a finite point (it was from Theorem 1), we have

$\geq K_{: n^{*}}^{π_{i}} (s_{0}) (λ a o s_{1 : n^{*} + 1} . {inf}_{C_{n^{*} + 2 : \infty}^{⊤} [C^{S}, ϵ]} f (s_{0}, a o s_{1 : n^{*} + 1}, a o s_{n^{*} + 2 : \infty})) - 2 | | f | |$
$- K_{: n^{*}}^{π_{i}} (s_{0}) (λ a o s_{1 : n^{*} + 1} . {inf}_{C_{n^{*} + 2 : \infty}^{⊤} [C^{S}, ϵ]} f (s_{0}, a o s_{1 : n^{*} + 1}, a o s_{n^{*} + 2 : \infty}))$

$= - 2 | | f | |$

And we're done, we have shown that, regardless of $s_{0}$ , we have

Now, applying this fact to our giant list of integrals, we can take

$lim i \to \infty (\int_{S} (λ s_{0} . lim n \to \infty (K_{: n}^{π_{i}} (s_{0}) (λ a o s_{1 : n + 1} . inf C_{n + 2 : \infty}^{⊤} [C^{S}, ϵ] f (s_{0}, a o s_{1 : n + 1}, a o s_{n + 2 : \infty})))) d m_{i, C^{S}}$
$+ \int_{S} (λ s_{0} . K_{: n^{*}}^{π_{i}} (s_{0}) (λ a o s_{1 : n^{*} + 1} . inf C_{n^{*} + 2 : \infty}^{⊤} [C^{S}, ϵ] f (s_{0}, a o s_{1 : n^{*} + 1}, a o s_{n^{*} + 2 : \infty}))) d m_{i, \neg C^{S}}$
$+ \int_{S} (λ s_{0} . lim n \to \infty (K_{: n}^{π_{i}} (s_{0}) (λ a o s_{1 : n + 1} . inf C_{n + 2 : \infty}^{⊤} [C^{S}, ϵ] f (s_{0}, a o s_{1 : n + 1}, a o s_{n + 2 : \infty})))$
$- K_{: n^{*}}^{π_{i}} (s_{0}) (λ a o s_{1 : n^{*} + 1} . {inf}_{C_{n^{*} + 2 : \infty}^{⊤} [C^{S}, ϵ]} f (s_{0}, a o s_{1 : n^{*} + 1}, a o s_{n^{*} + 2 : \infty}))) d m_{i, \neg C^{S}}) + b_{\infty}$

and apply our lower-bound to get

$\geq liminf i \to \infty (\int_{S} (λ s_{0} . lim n \to \infty (K_{: n}^{π_{i}} (s_{0}) (λ a o s_{1 : n + 1} . inf C_{n + 2 : \infty}^{⊤} [C^{S}, ϵ] f (s_{0}, a o s_{1 : n + 1}, a o s_{n + 2 : \infty})))) d m_{i, C^{S}}$
$+ \int_{S} (λ s_{0} . K_{: n^{*}}^{π_{i}} (s_{0}) (λ a o s_{1 : n^{*} + 1} . inf C_{n^{*} + 2 : \infty}^{⊤} [C^{S}, ϵ] f (s_{0}, a o s_{1 : n^{*} + 1}, a o s_{n^{*} + 2 : \infty}))) d m_{i, \neg C^{S}}$
$+ \int_{S} (- 2 | | f | |) d m_{i, \neg C^{S}}) + b_{\infty}$

Also, since we picked $C^{S}$ so $m_{i}$ only has $ϵ$ or less measure outside of it, regardless of i, we can impose a lower bound of:

Now, to break down the integral on the top. Since the behavior of the interior of that integral only depends on $s_{0} \in C^{S}$ , we can apply our good old Almost-Monotone-Lemma variation, and lower-bound the limit by the $n^{*}$ finite stage, minus $4 ϵ | | f | |$ (independently of the choice of $π_{i}$ ) yielding

$\geq liminf i \to \infty (\int_{S} (λ s_{0} . K_{: n^{*}}^{π_{i}} (s_{0}) (λ a o s_{1 : n^{*} + 1} . inf C_{n^{*} + 2 : \infty}^{⊤} [C^{S}, ϵ] f (s_{0}, a o s_{1 : n^{*} + 1}, a o s_{n^{*} + 2 : \infty})) - 4 ϵ | | f | |) d m_{i, C^{S}}$
$+ \int_{S} (λ s_{0} . K_{: n^{*}}^{π_{i}} (s_{0}) (λ a o s_{1 : n^{*} + 1} . inf C_{n^{*} + 2 : \infty}^{⊤} [C^{S}, ϵ] f (s_{0}, a o s_{1 : n^{*} + 1}, a o s_{n^{*} + 2 : \infty}))) d m_{i, \neg C^{S}}) - 2 ϵ | | f | | + b_{\infty}$

Now, we pull that constant piece out of the integral, and since both functions in the integral are now identical, we can stitch the measure components back together to get:

$= liminf i \to \infty (\int_{S} (λ s_{0} . K_{: n^{*}}^{π_{i}} (s_{0}) (λ a o s_{1 : n^{*} + 1} . inf C_{n^{*} + 2 : \infty}^{⊤} [C^{S}, ϵ] f (s_{0}, a o s_{1 : n^{*} + 1}, a o s_{n^{*} + 2 : \infty}))) d m_{i}$
$+ \int_{S} (- 4 ϵ | | f | |) d m_{i, C^{S}}) - 2 ϵ | | f | | + b_{\infty}$

Now, $m_{i, C^{S}}$ is a fragment of $m_{i}$ , which came from a minimal point in $Ψ$ or a limit of such, so the maximal amount of measure present would be $λ^{⊙}$ . This lets us get a lower bound of

$\geq liminf i \to \infty \int_{S} (λ s_{0} . K_{: n^{*}}^{π_{i}} (s_{0}) (λ a o s_{1 : n^{*} + 1} . inf C_{n^{*} + 2 : \infty}^{⊤} [C^{S}, ϵ] f (s_{0}, a o s_{1 : n^{*} + 1}, a o s_{n^{*} + 2 : \infty}))) d m_{i}$
$- 4 ϵ λ^{⊙} | | f | | - 2 ϵ | | f | | + b_{\infty}$

Doing a little bit of regrouping, we have

$= liminf i \to \infty \int_{S} (λ s_{0} . K_{: n^{*}}^{π_{i}} (s_{0}) (λ a o s_{1 : n^{*} + 1} . inf C_{n^{*} + 2 : \infty}^{⊤} [C^{S}, ϵ] f (s_{0}, a o s_{1 : n^{*} + 1}, a o s_{n^{*} + 2 : \infty}))) d m_{i}$
$- 2 ϵ | | f | | (2 λ^{⊙} + 1) + b_{\infty}$

Recapping what we've done so far, we showed that

${liminf}_{m \to \infty} (ψ ⋉ K_{: \infty}^{π_{m}}) (f)$

For all $n^{*}$ . Regardless of $n^{*}$ , this liminf value in i is finite because it's upper-bounded by the liminf in m, which is assumed to be finite (we disposed of the infinite case already). Because the sequence $m_{i}$ and the compact sets $C_{n}^{⊤} [C^{S}, ϵ]$ were fixed before we picked $n^{*}$ , we can take a limit of the $n^{*}$ without worrying about it affecting any of the stuff on the inside of the integral, to get

${liminf}_{m \to \infty} (ψ ⋉ K_{: \infty}^{π_{m}}) (f)$

$\geq liminf n \to \infty liminf i \to \infty \int_{S} (λ s_{0} . K_{: n}^{π_{i}} (s_{0}) (λ a o s_{1 : n + 1} . inf C_{n + 2 : \infty}^{⊤} [C^{S}, ϵ] f (s_{0}, a o s_{1 : n + 1}, a o s_{n + 2 : \infty}))) d m_{i}$
$- 2 ϵ | | f | | (2 λ^{⊙} + 1) + b_{\infty}$

This liminf in i of the integral is finite for all n. At this point, we can notice something interesting. For fixed n, when we take the limit as i approaches infinity, eventually $K_{: n}^{π_{i}}$ will become $K_{: n}^{π_{\infty}}$ and never go back, because of convergence of the policies, and the fact that the infrakernel has a cutoff at time n, so the behavior of the policies before that time will stabilize on a partial policy. So, we can rewrite our lower bound as:

$= liminf n \to \infty liminf i \to \infty \int_{S} (λ s_{0} . K_{: n}^{π_{\infty}} (s_{0}) (λ a o s_{1 : n + 1} . inf C_{n + 2 : \infty}^{⊤} [C^{S}, ϵ] f (s_{0}, a o s_{1 : n + 1}, a o s_{n + 2 : \infty}))) d m_{i}$
$- 2 ϵ | | f | | (2 λ^{⊙} + 1) + b_{\infty}$

Again, for all n, this liminf in i quantity is finite. Now, the function

$λ s_{0} . K_{: n}^{π_{\infty}} (s_{0}) (λ a o s_{1 : n + 1} . {inf}_{C_{n + 2 : \infty} [C^{S}, ϵ]} f (s_{0}, a o s_{1 : n + 1}, a o s_{n + 2 : \infty}))$

is lower-semicontinuous in $s_{0}$ (as all the finite stages of the infinite infrakernel have that niceness property). And $m \mapsto m (f^{*})$ is lower-semicontinuous when $f^{*}$ is. Also, by now, the only thing i is controlling is the measure term. Therefore, that liminf of the integral (in i) is greater than what you'd get if you just passed to $m_{\infty}$ . So, we get

$\geq liminf n \to \infty \int_{S} (λ s_{0} . K_{: n}^{π_{\infty}} (s_{0}) (λ a o s_{1 : n + 1} . inf C_{n + 2 : \infty}^{⊤} [C^{S}, ϵ] f (s_{0}, a o s_{1 : n + 1}, a o s_{n + 2 : \infty}))) d m_{\infty}$
$+ b_{\infty} - 2 ϵ | | f | | (2 λ^{⊙} + 1)$

Again, for all n, the integral is finite. Now, since the functions

$λ s_{0} . K_{: n}^{π_{\infty}} (s_{0}) (λ a o s_{1 : n + 1} . {inf}_{C_{n + 2 : \infty}^{⊤} [C^{S}, ϵ]} f (s_{0}, a o s_{1 : n + 1}, a o s_{n + 2 : \infty}))$

converge pointwise in n to the function

$λ s_{0} . K_{: \infty}^{π_{\infty}} (s_{0}) (λ a o s_{1 : \infty} . f (s_{0}, a o s_{1 : \infty}))$

(any sequence of compact sets works to define the infinite semidirect product) and for all n, the integrals are finite (this is why we kept restating it over and over!), we can apply Fatou's Lemma to move the liminf into the integral, to get

$\geq \int_{S} (λ s_{0} . liminf n \to \infty K_{: n}^{π_{\infty}} (s_{0}) (λ a o s_{1 : n + 1} . inf C_{n + 2 : \infty}^{⊤} [C^{S}, ϵ] f (s_{0}, a o s_{1 : n + 1}, a o s_{n + 2 : \infty}))) d m_{\infty}$
$+ b_{\infty} - 2 ϵ | | f | | (2 λ^{⊙} + 1)$

And since we have pointwise limiting, this is

$= \int_{S} (λ s_{0} . lim n \to \infty K_{: n}^{π_{\infty}} (s_{0}) (λ a o s_{1 : n + 1} . inf C_{n + 2 : \infty}^{⊤} [C^{S}, ϵ] f (s_{0}, a o s_{1 : n + 1}, a o s_{n + 2 : \infty}))) d m_{\infty}$
$+ b_{\infty} - 2 ϵ | | f | | (2 λ^{⊙} + 1)$

and then, packing it up,

$= \int_{S} (λ s_{0} . K_{: \infty}^{π_{\infty}} (s_{0}) (λ a o s_{1 : \infty} . f (s_{0}, a o s_{1 : \infty}))) d m_{\infty} + b_{\infty} - 2 ϵ | | f | | (2 λ^{⊙} + 1)$

And then, pack it up as

$= m_{\infty} (λ s_{0} . K_{: \infty}^{π_{\infty}} (s_{0}) (λ a o s_{1 : \infty} . f (s_{0}, a o s_{1 : \infty}))) + b_{\infty} - 2 ϵ | | f | | (2 λ^{⊙} + 1)$

and one last step. Since $(m_{\infty}, b_{\infty})$ lies in $Ψ$ , we can get

$\geq {inf}_{(m, b) \in Ψ} (m (λ s_{0} . K_{: \infty}^{π_{\infty}} (s_{0}) (λ a o s_{1 : \infty} . f (s_{0}, a o s_{1 : \infty}))) + b) - 2 ϵ | | f | | (2 λ^{⊙} + 1)$

which reexpresses as

$= ψ (λ s_{0} . K_{: \infty}^{π_{\infty}} (s_{0}) (λ a o s_{1 : \infty} . f (s_{0}, a o s_{1 : \infty}))) - 2 ϵ | | f | | (2 λ^{⊙} + 1)$

$= (ψ ⋉ K_{: \infty}^{π_{\infty}}) (f) - 2 ϵ | | f | | (2 λ^{⊙} + 1)$

Our net result is

${liminf}_{m \to \infty} (ψ ⋉ K_{: \infty}^{π_{m}}) (f) \geq (ψ ⋉ K_{: \infty}^{π_{\infty}}) (f) - 2 ϵ | | f | | (2 λ^{⊙} + 1)$

But because $ϵ$ was arbitrary and $| | f | |$ and $λ^{⊙}$ are finite, we have our desired net result of

${liminf}_{m \to \infty} (ψ ⋉ K_{: \infty}^{π_{m}}) (f) \geq (ψ ⋉ K_{: \infty}^{π_{\infty}}) (f)$

And lower-semicontinuity is shown for $π \mapsto (ψ ⋉ K_{: \infty}^{π}) (f)$

T4.2.2.3 Now for our phase 3, getting lower-semicontinuity of $π \mapsto Θ (π) (U)$ . Let $π_{m}$ limit to $π_{\infty}$ . We have

${liminf}_{m \to \infty} Θ (π_{m}) (U)$

and then this unpacks as

$= {liminf}_{m \to \infty} p r_{(A \times O)^{ω} *} (ψ ⋉ K_{: \infty}^{π_{m}}) (U)$

Reexpressing the projection, we have:

$= {liminf}_{m \to \infty} (ψ ⋉ K_{: \infty}^{π_{m}}) (λ s_{0}, a o s_{1 : \infty} . U (a o_{1 : \infty}))$

And then, we can apply lower-semicontinuity of $π \mapsto (ψ ⋉ K_{: \infty}^{π}) (f)$ which we've shown in phase 2, to get

$\geq (ψ ⋉ K_{: \infty}^{π_{\infty}}) (λ s_{0}, a o s_{1 : \infty} . U (a o_{1 : \infty}))$

Which then packs up as

$= p r_{(A \times O)^{ω} *} (ψ ⋉ K_{: \infty}^{π_{\infty}}) (U)$

and then

$= Θ (π_{\infty}) (U)$

and we have lower-semicontinuity for $Θ$ ! Finally!

T4.2.3 Time to return to easier fare. We need that $Θ (π)$ is supported entirely on histories compatible with $π$ . To do this, we proceed in three steps.

First, we do an induction proof that, for any given $π$ and $s_{0}$ , $K_{: n}^{π} (s_{0})$ is supported on the subset of $(A \times O \times S)^{n + 1}$ where the actions and observations so far are compatible with $π$ .

Second, we use our first result to show that for any two continuous bounded utility functions $U, U^{'}$ which only depend on the action/observation sequence, and agree on all histories compatible with $π$ ,

$K_{: \infty}^{π} (s_{0}) (λ a o s_{1 : \infty} . U (a o_{1 : \infty})) = K_{: \infty}^{π} (s_{0}) (λ a o s_{1 : \infty} . U^{'} (a o_{1 : \infty}))$

Finally, we use this result to show that if $U, U^{'}$ agree on all histories compatible with $π$ , $Θ (π) (U) = Θ (π) (U^{'})$ , showing that $Θ (π)$ is supported on histories compatible with $π$ .

T4.2.3.1 Let's start with the induction proof that $K_{: n}^{π} (s_{0})$ has the subset of $(A \times O \times S)^{n + 1}$ where the history of actions and observations is compatible with $π$ as a support. The way to do that is to pick two functions that are identical on said subset, and show they have equal expectation values. For the base case of the induction proof, fix an $f$ and $f^{'}$ which are identical on ${π ()} \times O \times S$ (as that's the subset of $A \times O \times S$ which is compatible with $π$ ), and observe:

$K_{: 0}^{π} (s_{0}) (f) = K_{0}^{π} (s_{0}) (λ a, o, s . f (a, o, s))$

and then by how $K_{0}^{π} (s_{0})$ is defined, we have

$= (δ_{π ()} ⋉ (λ a . K (s_{0}, a))) (λ a^{'}, o, s . f (a^{'}, o, s))$

Which, by unpacking the semidirect product and subsituting the dirac-delta value in, we have

$= K (s_{0}, π ()) (λ o, s . f (π (), o, s))$

and then since $f = f^{'}$ when the initial action equals $π ()$ , we have

$= K (s_{0}, π ()) (λ o, s . f^{'} (π (), o, s))$

and then this just wraps back up by our sequence of rewrite steps in reverse as

$= K_{: 0}^{π} (s_{0}) (f^{'})$

Now that we have the base case out of the way, we'll attempt to show the induction step. Let $f$ and $f^{'}$ be identical on the subset of $(A \times O \times S)^{n + 2}$ which is compatible with $π$ , and we'll show they have equal expectation value. Our job is to unpack

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

this unpacks, by how sequences of semidirect products are defined, as

Now, since, by induction assumption, $K_{: n}^{π} (s_{0})$ is supported on the subset of $(A \times O \times S)^{n + 1}$ where the history is compatible with $π$ , we just need to show that the inner functions are identical on that subset to get that the difference is 0, so our proof goal is now

$\forall a o s_{1 : n + 1} \sim π : K_{n + 1}^{π} (s_{0}, a o s_{1 : n + 1}) (λ a, o, s . f (a o s_{1 : n + 1}, a, o, s))$
$= K_{n + 1}^{π} (s_{0}, a o s_{1 : n + 1}) (λ a, o, s . f^{'} (a o s_{1 : n + 1}, a, o, s))$

We now unpack $K_{n + 1}^{π} (s_{0}, a o s_{1 : n + 1})$ as $δ_{π (a o_{1 : n + 1})} ⋉ (λ a . K (s_{n + 1}, a))$ to get our new proof goal of:

$\forall a o s_{1 : n + 1} \sim π : (δ_{π (a o_{1 : n + 1})} ⋉ (λ a . K (s_{n + 1}, a))) (λ a^{'}, o, s . f (a o s_{1 : n + 1}, a^{'}, o, s))$
$= (δ_{π (a o_{1 : n + 1})} ⋉ (λ a . K (s_{n + 1}, a))) (λ a^{'}, o, s . f^{'} (a o s_{1 : n + 1}, a^{'}, o, s))$

We unpack the semidirect product and substitute the dirac-delta value in to get a proof goal of

$\forall a o s_{1 : n + 1} \sim π : K (s_{n + 1}, π (a o_{1 : n + 1})) (λ o, s . f (a o s_{1 : n + 1}, π (a o_{1 : n + 1}), o, s))$
$= K (s_{n + 1}, π (a o_{1 : n + 1})) (λ o, s . f^{'} (a o s_{1 : n + 1}, π (a o_{1 : n + 1}), o, s))$

at this point, we realize that if $a o s_{1 : n + 1}$ is compatible with $π$ , then regardless of $o$ and $s$ , $a o s_{1 : n + 1}, π (a o_{1 : n + 1}), o, s$ is compatible with $π$ , so the functions

$λ o, s . f (a o s_{1 : n + 1}, π (a o_{1 : n + 1}), o, s)$

and

$λ o, s . f^{'} (a o s_{1 : n + 1}, π (a o_{1 : n + 1}), o, s)$

are equal, and we get our desired proof goal. So the induction goes through, and the subset of $(A \times O \times S)^{n + 1}$ where the history is compatible with $π$ will always be a support of $K_{: n}^{π}$ for all n.

T4.2.3.2 Now that's in place, we'll show that any two continuous bounded functions $U$ and $U^{'}$ which only depend on the action/observation sequence and are identical on histories compatible with $π$ will be assigned equal value by $K_{: \infty}^{π} (s_{0})$ . Assume $U$ and $U^{'}$ only depend on action/observation sequences and are identical on histories compatible with $π$ . We have a desired proof target of

$K_{: \infty}^{π} (s_{0}) (λ a o s_{1 : \infty} . U (a o_{1 : \infty})) = K_{: \infty}^{π} (s_{0}) (λ a o s_{1 : \infty} . U^{'} (a o_{1 : \infty}))$

and, unpacking the limit, it turns into

${lim}_{n \to \infty} K_{: n}^{π} (s_{0}) (λ a o s_{1 : n + 1} . {inf}_{a o_{n + 2 : \infty}} U (a o_{1 : n + 1}, a o_{n + 2 : \infty}))$
$= {lim}_{n \to \infty} K_{: n}^{π} (s_{0}) (λ a o s_{1 : n + 1} . {inf}_{a o_{n + 2 : \infty}} U^{'} (a o_{1 : n + 1}, a o_{n + 2 : \infty}))$

The limits exist, so we'd be able to show that if we were able to show that

${limsup}_{n \to \infty} | K_{: n}^{π} (s_{0}) (λ a o s_{1 : n + 1} . {inf}_{a o_{n + 2 : \infty}} U (a o_{1 : n + 1}, a o_{n + 2 : \infty}))$
$- K_{: n}^{π} (s_{0}) (λ a o s_{1 : n + 1} . {inf}_{a o_{n + 2 : \infty}} U^{'} (a o_{1 : n + 1}, a o_{n + 2 : \infty})) | = 0$

Now, we can use the Lemma 2 from LBIT decomposition on $K_{: n}^{π} (s_{0})$ , since we know that the subset of $(A \times O \times S)^{n + 1}$ where the history is compatible with $π$ is a support of $K_{: n}^{π} (s_{0})$ , to get an upper bound on

$\leq {limsup}_{n \to \infty} (1 \cdot {sup}_{a o s_{1 : n + 1} \sim π} | {inf}_{a o_{n + 2 : \infty}} U (a o_{1 : n + 1}, a o_{n + 2 : \infty})$
$- {inf}_{a o_{n + 2 : \infty}} U^{'} (a o_{1 : n + 1}, a o_{n + 2 : \infty}) | + 0 \cdot d (U, U^{'}))$

For the first part, the 1 is there because all the infrakernels are 1-Lipschitz, and we're assessing distance of the inner functions on the support. For the second part, it's there because we don't care how different the two functions are outside the support, they must be assigned equal value. So anyways, this upper bound reduces to

$= {limsup}_{n \to \infty} {sup}_{a o s_{1 : n + 1} \sim π} | {inf}_{a o_{n + 2 : \infty}} U (a o_{1 : n + 1}, a o_{n + 2 : \infty}) - {inf}_{a o_{n + 2 : \infty}} U^{'} (a o_{1 : n + 1}, a o_{n + 2 : \infty}) |$

Now, for all choices of n and $a o s_{1 : n + 1} \sim π$ , fix an arbitrary extension $a o_{n + 2 : \infty}^{\sim π}$ which is compatible with $π$ (which can always be done). Then use the triangle inequality twice to get an upper-bound of

$\leq {limsup}_{n \to \infty} {sup}_{a o s_{1 : n + 1} \sim π} (| {inf}_{a o_{n + 2 : \infty}} U (a o_{1 : n + 1}, a o_{n + 2 : \infty}) - U (a o_{1 : n + 1}, a o_{n + 2 : \infty}^{\sim π}) |$
$+ | U (a o_{1 : n + 1}, a o_{n + 2 : \infty}^{\sim π}) - U^{'} (a o_{1 : n + 1}, a o_{n + 2 : \infty}^{\sim π}) |$
$+ | U^{'} (a o_{1 : n + 1}, a o_{n + 2 : \infty}^{\sim π}) - {inf}_{a o_{n + 2 : \infty}} U^{'} (a o_{1 : n + 1}, a o_{n + 2 : \infty}) |)$

We can observe that, since $U$ and $U^{'}$ are equal on all histories compatible with $π$ , and $a o_{n + 2 : \infty}^{\sim π}$ was picked specifically to have $a o_{1 : n + 1}, a o_{n + 2 : \infty}^{\sim π} \sim π$ , that second absolute value term must always be 0, to get

$= {limsup}_{n \to \infty} {sup}_{a o s_{1 : n + 1} \sim π} (| {inf}_{a o_{n + 2 : \infty}} U (a o_{1 : n + 1}, a o_{n + 2 : \infty}) - U (a o_{1 : n + 1}, a o_{n + 2 : \infty}^{\sim π}) |$
$+ | U^{'} (a o_{1 : n + 1}, a o_{n + 2 : \infty}^{\sim π}) - {inf}_{a o_{n + 2 : \infty}} U^{'} (a o_{1 : n + 1}, a o_{n + 2 : \infty}) |)$

and then distribute the sups and limsups into the addition to get

$\leq {limsup}_{n \to \infty} ({sup}_{a o s_{1 : n + 1} \sim π} | {inf}_{a o_{n + 2 : \infty}} U (a o_{1 : n + 1}, a o_{n + 2 : \infty}) - U (a o_{1 : n + 1}, a o_{n + 2 : \infty}^{\sim π}) |)$
$+ {limsup}_{n \to \infty} ({sup}_{a o s_{1 : n + 1} \sim π} | U^{'} (a o_{1 : n + 1}, a o_{n + 2 : \infty}^{\sim π}) - {inf}_{a o_{n + 2 : \infty}} U^{'} (a o_{1 : n + 1}, a o_{n + 2 : \infty}) |)$

Since this quantity is an upper bound on the

quantity we wanted to show equals 0 to hit our proof target, we just need to show that it equals 0.

Here's what we do now. Since $U$ and $U^{'}$ are defined over $(A \times O)^{ω}$ , a compact space, they must both be uniformly continuous. You can take any $ϵ$ , and find some $δ$ where two histories that only differ by $δ$ are assigned values $ϵ$ or less apart. And for any $δ$ , there's some n where any two histories that agree on the first n steps only differ by $δ$ . So, in the limit, both of these terms become 0, and our result that

$K_{: \infty}^{π} (s_{0}) (λ a o s_{1 : \infty} . U (a o_{1 : \infty})) = K_{: \infty}^{π} (s_{0}) (λ a o s_{1 : \infty} . U^{'} (a o_{1 : \infty}))$

for any $s_{0}$ and $U, U^{'}$ which agree on all histories compatible with $π$ follows since we hit our proof target.

T4.2.3.3 Finally, it's time to apply this result to get that $Θ (π)$ is supported only on histories compatible with $π$ . Fix any $π$ , and $U, U^{'}$ which are identical on histories compatible with $π$ . We can start unpacking.

$| Θ (π) (U) - Θ (π) (U^{'}) | = | p r_{(A \times O)^{ω} *} (ψ ⋉ K_{: \infty}^{π}) (U) - p r_{(A \times O)^{ω} *} (ψ ⋉ K_{: \infty}^{π}) (U^{'}) |$

$= | ψ (λ s_{0} . K_{: \infty}^{π} (s_{0}) (λ a o s_{1 : \infty} . U (a o_{1 : \infty}))) - ψ (λ s_{0} . K_{: \infty}^{π} (s_{0}) (λ a o s_{1 : \infty} . U^{'} (a o_{1 : \infty}))) |$

And then, for all $s_{0}$ ,

$K_{: \infty}^{π} (s_{0}) (λ a o s_{1 : \infty} . U (a o_{1 : \infty})) = K_{: \infty}^{π} (s_{0}) (λ a o s_{1 : \infty} . U^{'} (a o_{1 : \infty}))$

as we've already shown, since $U$ and $U^{'}$ agree on histories compatible with $π$ . Thus the functions in $ψ$ are identical, and we have

$| Θ (π) (U) - Θ (π) (U^{'}) | = 0$

and so we're done.

T4.2.4 The next belief function condition to check is agreement on max value. For the $[0, 1]$ type signature, fixing any $π$ and $π^{'}$

$| Θ (π) (1) - Θ (π^{'}) (1) | = | p r_{(A \times O)^{ω} *} (ψ ⋉ K_{: \infty}^{π}) (1) - p r_{(A \times O)^{ω} *} (ψ ⋉ K_{: \infty}^{π^{'}}) (1) |$

$= | ψ (λ s_{0} . K_{: \infty}^{π} (s_{0}) (1)) - ψ (λ s_{0} . K_{: \infty}^{π^{'}} (s_{0}) (1)) |$

And for the $[0, 1]$ type signature, any infinite semidirect product fulfilling the niceness conditions (which is the case) must map 1 to 1, so this turns into

$= | ψ (1) - ψ (1) | = 0$

And we're done, and in fact get the stronger result that $Θ (π) (1) = 1$ regardless of $π$ because $ψ (1) = 1$ because we assumed $ψ$ was an infradistribution. For the $R$ type signature, fixing any $π$ and $π^{'}$ , we have

$| Θ (π) (\infty) - Θ (π^{'}) (\infty) | = | p r_{(A \times O)^{ω} *} (ψ ⋉ K_{: \infty}^{π}) (\infty) - p r_{(A \times O)^{ω} *} (ψ ⋉ K_{: \infty}^{π^{'}}) (\infty) |$

$= | ψ (λ s_{0} . K_{: \infty}^{π} (s_{0}) (\infty)) - ψ (λ s_{0} . K_{: \infty}^{π^{'}} (s_{0}) (\infty)) |$

Regardless of type signature, an infinite semidirect product fulfilling the niceness conditions (which we're assuming) must map constants to an equal or greater constant, and infinity can be regarded as the supremum of putting constants in, so we get

$= | ψ (\infty) - ψ (\infty) | = 0$

Importantly, this does not mean that $Θ (π) (\infty)$ must be $\infty$ .

T4.2.5 Now for the very last condition, checking that $Θ$ is pseudocausal. This takes a whole lot of work (though less than lower-semicontinuity), and we'll do it by repeatedly showing equivalence of our desired result to some slightly simpler result, until we ground out in an induction proof we clean up in the same way, which splits into a base case and induction step.

T4.2.5.1 We want to show that

$\forall U : u_{\sim π^{'}}^{1} (Θ (π)) (U) \geq Θ (π^{'}) (U)$

We can unpack $Θ (π)$ and $Θ (π^{'})$ , to get the equivalent proof target of:

$u_{\sim π^{'}}^{1} (p r_{(A \times O)^{ω} *} (ψ ⋉ K_{: \infty}^{π})) (U) \geq p r_{(A \times O)^{ω} *} (ψ ⋉ K_{: \infty}^{π^{'}}) (U)$

First, we expand the update, to get the equivalent proof target of:

$p r_{(A \times O)^{ω} *} (ψ ⋉ K_{: \infty}^{π}) (λ a o_{: \infty} . 1_{a o_{1 : \infty} \sim π^{'}} U (a o_{1 : \infty}) + 1_{a o_{1 : \infty} ≁ π^{'}})$
$\geq p r_{(A \times O)^{ω} *} (ψ ⋉ K_{: \infty}^{π^{'}}) (λ a o_{1 : \infty} . U (a o_{1 : \infty}))$

Then we rewrite the projections to get the equivalent proof target of

$(ψ ⋉ K_{: \infty}^{π}) (λ s_{0}, a o s_{1 : \infty} . 1_{a o_{1 : \infty} \sim π^{'}} U (a o_{1 : \infty}) + 1_{a o_{1 : \infty} ≁ π^{'}}) \geq (ψ ⋉ K_{: \infty}^{π^{'}}) (λ s_{0}, a o s_{1 : \infty} . U (a o_{1 : \infty}))$

Then we rewrite the semidirect products to get the equivalent proof target of

$ψ (λ s_{0} . K_{: \infty}^{π} (s_{0}) (λ a o s_{: \infty} . 1_{a o_{1 : \infty} \sim π^{'}} U (a o_{1 : \infty}) + 1_{a o_{1 : \infty} ≁ π^{'}})) \geq ψ (λ s_{0} . K_{: \infty}^{π^{'}} (s_{0}) (λ a o s_{1 : \infty} . U (a o_{1 : \infty})))$

By monotonicity for $ψ$ , we'd be able to prove this if, for any $s_{0}$ initial state, we had

$K_{: \infty}^{π} (s_{0}) (λ a o s_{1 : \infty} . 1_{a o_{1 : \infty} \sim π^{'}} U (a o_{1 : \infty}) + 1_{a o_{1 : \infty} ≁ π^{'}}) \geq K_{: \infty}^{π^{'}} (s_{0}) (λ a o s_{1 : \infty} . U (a o_{1 : \infty}))$

So we'll now try to prove this, let $s_{0}$ be arbitrary. We can explicitly unpack the infinite semidirect product, and get a proof target of

${lim}_{n \to \infty} K_{: n}^{π} (s_{0}) (λ a o s_{1 : n + 1} . {inf}_{a o_{n + 2 : \infty}} (1_{a o_{1 : n + 1}, a o_{n + 2 : \infty} \sim π^{'}} U (a o_{1 : n + 1}, a o_{n + 2 : \infty}) + 1_{a o_{1 : n + 1}, a o_{n + 2 : \infty} ≁ π^{'}}))$
$\geq {lim}_{n \to \infty} K_{: n}^{π^{'}} (s_{0}) (λ a o s_{1 : n + 1} . {inf}_{a o_{n + 2 : \infty}} U (a o_{1 : n + 1}, a o_{n + 2 : \infty}))$

We'd be able to prove this if we could prove the inequality for all the n individually, as then the inequality would carry over to the limit. So, our new proof target is, for arbitrary n,

$K_{: n}^{π} (s_{0}) (λ a o s_{1 : n + 1} . {inf}_{a o_{n + 2 : \infty}} (1_{a o_{1 : n + 1}, a o_{n + 2 : \infty} \sim π^{'}} U (a o_{1 : n + 1}, a o_{n + 2 : \infty}) + 1_{a o_{1 : n + 1}, a o_{n + 2 : \infty} ≁ π^{'}}))$
$\geq K_{: n}^{π^{'}} (s_{0}) (λ a o s_{1 : n + 1} . {inf}_{a o_{n + 2 : \infty}} U (a o_{1 : n + 1}, a o_{n + 2 : \infty}))$

We can observe something interesting here for the update. if $a o_{1 : n + 1}$ is compatible with $π^{'}$ , then the inf can be modeled as always picking some continuation compatible with $π^{'}$ , because doing otherwise would make the function equal 1 (or infinity). In such a case, the inner function of the top would turn into ${inf}_{a o_{n + 2 : \infty}} U (a o_{1 : n + 1}, a o_{n + 2 : \infty})$ . If $a o_{1 : n + 1}$ is incompatible with $π^{'}$ , then it doesn't matter the extension, any extension will always be incompatible with $π^{'}$ , and return 1 (or infinity). So, this can be rephrased as

$K_{: n}^{π} (s_{0}) (λ a o s_{1 : n + 1} . 1_{a o_{1 : n + 1} \sim π^{'}} {inf}_{a o_{n + 2 : \infty}} U (a o_{1 : n + 1}, a o_{n + 2 : \infty}) + 1_{a o_{1 : n + 1} ≁ π^{'}})$
$\geq K_{: n}^{π^{'}} (s_{0}) (λ a o s_{1 : n + 1} . {inf}_{a o_{n + 2 : \infty}} U (a o_{1 : n + 1}, a o_{n + 2 : \infty}))$

Now, we can pack up the fact that we're updating on "partial history is compatible with $π^{'}$ " to get an equivalent proof target of

$u_{\sim π^{'}}^{1} (K_{: n}^{π} (s_{0})) (λ a o s_{1 : n + 1} . {inf}_{a o_{n + 2 : \infty}} U (a o_{1 : n + 1}, a o_{n + 2 : \infty}))$
$\geq K_{: n}^{π^{'}} (s_{0}) (λ a o s_{1 : n + 1} . {inf}_{a o_{n + 2 : \infty}} U (a o_{1 : n + 1}, a o_{n + 2 : \infty}))$

Now, since these inner functions are identical, we'd be able to prove this proof target if we proved the following for arbitrary functions $f_{n + 1} : (A \times O \times S)^{n + 1} \to [0, 1]$ (or $R$ ), and arbitrary $n, π^{'}, π, s_{0}$ as before.

$u_{\sim π^{'}}^{1} (K_{: n}^{π} (s_{0})) (f_{n + 1}) \geq K_{: n}^{π^{'}} (s_{0}) (f_{n + 1})$

So, since we're trying to prove this result for arbitrary n, the obvious thing to do is an induction proof. If we can show this by induction, we hit our proof target and we're done.

T4.2.5.2 For our base case, we'd want to show

$u_{\sim π^{'}}^{1} (K_{: 0}^{π} (s_{0})) (f_{1}) \geq K_{: 0}^{π^{'}} (s_{0}) (f_{1})$

We reexpress the update to get a proof target of

$K_{: 0}^{π} (s_{0}) (λ a, o, s . 1_{a, o \sim π^{'}} f_{1} (a, o, s) + 1_{a, o ≁ π^{'}}) \geq K_{: 0}^{π^{'}} (s_{0}) (λ a, o, s . f_{1} (a, o, s))$

Now, the only way for $a, o$ to be incompatible with $π^{'}$ is if $a \neq π^{'} ()$ . Doing that reexpression, we get

$K_{: 0}^{π} (s_{0}) (λ a, o, s . 1_{a = π^{'} ()} f_{1} (a, o, s) + 1_{a \neq π^{'} ()}) \geq K_{: 0}^{π^{'}} (s_{0}) (λ a, o, s . f_{1} (a, o, s))$

We recall that for the iterated semidirect product, the $: 0$ thing is just $K_{0}^{π}$ , and $K_{0}^{π} (s_{0}) = δ_{π ()} ⋉ (λ a . K (s_{0}, a))$ . Making these substitutions, we get an equivalent proof target of

$(δ_{π ()} ⋉ (λ a . K (s_{0}, a))) (λ a, o, s . 1_{a = π^{'} ()} f_{1} (a, o, s) + 1_{a \neq π^{'} ()})$
$\geq (δ_{π^{'} ()} ⋉ (λ a . K (s_{0}, a))) (λ a, o, s . f_{1} (a, o, s))$

Reexpressing the semidirect product and subsituting the dirac-delta value in, we get the equivalent

$K (s_{0}, π ()) (λ o, s . 1_{π () = π^{'} ()} f_{1} (π (), o, s) + 1_{π () \neq π^{'} ()}) \geq K (s_{0}, π^{'} ()) (λ o, s . f_{1} (π^{'} (), o, s))$

We have two possible cases. In case 1, $π () = π^{'} ()$ , and then our proof target turns into

$K (s_{0}, π^{'} ()) (λ o, s . f_{1} (π^{'} (), o, s)) \geq K (s_{0}, π^{'} ()) (λ o, s . f_{1} (π^{'} (), o, s))$

Which is just true, they're equal. In case 2, $π () \neq π^{'} ()$ , and we then get the proof target of

$K (s_{0}, π ()) (1) \geq K (s_{0}, π^{'} ()) (λ o, s . f_{1} (π^{'} (), o, s))$

Which is true because

$K (s_{0}, π ()) (1) = 1 \geq K (s_{0}, π^{'} ()) (λ o, s . f_{1} (π^{'} (), o, s))$

Because of mapping 1 to 1. Or, for the $R$ type signature, we'd have

$K (s_{0}, π ()) (\infty) = \infty \geq K (s_{0}, π^{'} ()) (λ o, s . f_{1} (π^{'} (), o, s))$

By Constants Increase for $K$ . So, we've finally finished up our proof target, setting up the base case for the induction.

T4.2.5.3 Now for the induction step, which is all we need to finish up the proof. We need to somehow show that

$u_{\sim π^{'}}^{1} (K_{: n + 1}^{π} (s_{0})) (f_{n + 2}) \geq K_{: n + 1}^{π^{'}} (s_{0}) (f_{n + 2})$

For all functions $f_{n + 2} : (A \times O \times S)^{n + 2} \to [0, 1]$ , assuming that

$u_{\sim π^{'}}^{1} (K_{: n}^{π} (s_{0})) (f_{n + 1}) \geq K_{: n}^{π^{'}} (s_{0}) (f_{n + 1})$

holds for all functions $f_{n + 1} : (A \times O \times S)^{n + 1} \to [0, 1]$ . Let's begin. Our proof target is

$u_{\sim π^{'}}^{1} (K_{: n + 1}^{π} (s_{0})) (f_{n + 2}) \geq K_{: n + 1}^{π^{'}} (s_{0}) (f_{n + 2})$

We reexpress the update, to get the equivalent statement

$K_{: n + 1}^{π} (s_{0}) (λ a o s_{1 : n + 2} . 1_{a o_{1 : n + 2} \sim π^{'}} f_{n + 2} (a o s_{1 : n + 2}) + 1_{a o_{1 : n + 2} ≁ π^{'}})$
$\geq K_{: n + 1}^{π^{'}} (s_{0}) (λ a o s_{1 : n + 2} . f_{n + 2} (a o s_{1 : n + 2}))$

We unpack the definition of $K_{: n + 1}^{π} (s_{0})$ to get

$K_{: n}^{π} (s_{0}) (λ a o s_{1 : n + 1} . K_{n + 1}^{π} (s_{0}, a o s_{1 : n + 1})$
$(λ a, o, s . 1_{a o_{1 : n + 1}, a, o \sim π^{'}} f_{n + 2} (a o s_{1 : n + 1}, a, o, s) + 1_{a o_{1 : n + 1}, a, o ≁ π^{'}}))$
$\geq K_{: n}^{π^{'}} (s_{0}) (λ a o s_{1 : n + 1} . K_{n + 1}^{π^{'}} (s_{0}, a o s_{: n + 1}) (λ a, o, s . f_{n + 2} (a o s_{1 : n + 1}, a, o, s)))$

And then substitute in the definition of $K_{n + 1}^{π}$ to get

$K_{: n}^{π} (s_{0}) (λ a o s_{1 : n + 1} . (δ_{π (a o_{1 : n + 1})} ⋉ (λ a . K (s_{n + 1}, a)))$
$(λ a, o, s . 1_{a o_{1 : n + 1}, a, o \sim π^{'}} f_{n + 2} (a o s_{1 : n + 1}, a, o, s) + 1_{a o_{1 : n + 1}, a, o ≁ π^{'}}))$
$\geq K_{: n}^{π^{'}} (s_{0}) (λ a o s_{1 : n + 1} . (δ_{π^{'} (a o_{1 : n + 1})} ⋉ (λ a . K (s_{n + 1}, a))) (λ a, o, s . f_{n + 2} (a o s_{1 : n + 1}, a, o, s)))$

And unpack the semidirect product and substitute in the dirac-delta value to get the proof target of

$K_{: n}^{π} (s_{0}) (λ a o s_{1 : n + 1} . K (s_{n + 1}, π (a o_{1 : n + 1}))$
$(λ o, s . 1_{a o_{1 : n + 1}, π (a o_{1 : n + 1}), o \sim π^{'}} f_{n + 2} (a o s_{1 : n + 1}, π (a o_{1 : n + 1}), o, s) + 1_{a o_{1 : n + 1}, π (a o_{1 : n + 1}), o ≁ π^{'}}))$
$\geq K_{: n}^{π^{'}} (s_{0}) (λ a o s_{1 : n + 1} . K (s_{n + 1}, π^{'} (a o_{1 : n + 1})) (λ o, s . f_{n + 2} (a o s_{1 : n + 1}, π^{'} (a o_{1 : n + 1}), o, s)))$

Now, looking at that gigantic first term... if $a o_{1 : n + 1}$ is incompatible with $π^{'}$ , then the really big function is just going to turn into 1 (or infinity), which is assigned a value of 1 (or infinity) by $K$ , from the usual constants increase/1-normalization argument.

If $a o_{1 : n + 1} \sim π^{'}$ , then we're back in the usual business except we don't need to worry about incompatibilities of the history with $π^{'}$ within $a o_{1 : n + 1}$ , we only need to worry about those incompatiblities for the final action, $π (a o_{1 : n + 1})$ . So, we can rewrite that first term with indicator functions.

$K_{: n}^{π} (s_{0}) (λ a o s_{1 : n + 1} . 1_{a o_{1 : n + 1} \sim π^{'}} (K (s_{n + 1}, π (a o_{: n + 1}))$
$(λ o, s . 1_{π (a o_{: n + 1}) = π^{'} (a o_{: n + 1})} f_{n + 2} (a o s_{1 : n + 1}, π (a o_{1 : n + 1}), o, s) + 1_{π (a o_{1 : n + 1}) \neq π^{'} (a o_{1 : n + 1})}))$
$+ 1_{a o_{1 : n + 1} ≁ π^{'}})$
$\geq K_{: n}^{π^{'}} (s_{0}) (λ a o s_{1 : n + 1} . K (s_{n + 1}, π^{'} (a o_{1 : n + 1})) (λ o, s . f_{n + 2} (a o s_{1 : n + 1}, π^{'} (a o_{: n + 1}), o, s)))$

And then rewrite this as just an update on $K_{: n}^{π} (s_{0})$ , getting the equivalent proof goal

$u_{\sim π^{'}}^{1} (K_{: n}^{π} (s_{0})) (λ a o s_{1 : n + 1} . K (s_{n + 1}, π (a o_{: n + 1}))$
$(λ o, s . 1_{π (a o_{: n + 1}) = π^{'} (a o_{: n + 1})} f_{n + 2} (a o s_{1 : n + 1}, π (a o_{1 : n + 1}), o, s) + 1_{π (a o_{1 : n + 1}) \neq π^{'} (a o_{1 : n + 1})}))$
$\geq K_{: n}^{π^{'}} (s_{0}) (λ a o s_{1 : n + 1} . K (s_{n + 1}, π^{'} (a o_{1 : n + 1})) (λ o, s . f_{n + 2} (a o s_{1 : n + 1}, π^{'} (a o_{: n + 1}), o, s)))$

Now, we can define our $f_{n + 1}$ as

$λ a o s_{1 : n + 1} . K (s_{n + 1}, π (a o_{: n + 1}))$
$(λ o, s . 1_{π (a o_{: n + 1}) = π^{'} (a o_{: n + 1})} f_{n + 2} (a o s_{1 : n + 1}, π (a o_{1 : n + 1}), o, s) + 1_{π (a o_{1 : n + 1}) \neq π^{'} (a o_{1 : n + 1})})$

To derive, from our induction assumption, that

$= u_{\sim π^{'}}^{1} (K_{: n}^{π} (s_{0})) (f_{n + 1}) \geq K_{: n}^{π^{'}} (s_{0}) (f_{n + 1})$

$= K_{: n}^{π^{'}} (s_{0}) (λ a o s_{1 : n + 1} . K (s_{n + 1}, π (a o_{: n + 1}))$
$(λ o, s . 1_{π (a o_{: n + 1}) = π^{'} (a o_{: n + 1})} f_{n + 2} (a o s_{1 : n + 1}, π (a o_{1 : n + 1}), o, s) + 1_{π (a o_{1 : n + 1}) \neq π^{'} (a o_{1 : n + 1})}))$

So, as long as we're able to show that this quantity still lies above

$K_{: n}^{π^{'}} (s_{0}) (λ a o s_{1 : n + 1} . K (s_{n + 1}, π^{'} (a o_{1 : n + 1})) (λ o, s . f_{n + 2} (a o s_{1 : n + 1}, π^{'} (a o_{: n + 1}), o, s)))$

,we can just put the two inequalities together, and we'll attain our proof target and the induction will go through and we'll be done. So, our new proof target is

$K_{: n}^{π^{'}} (s_{0}) (λ a o s_{1 : n + 1} . K (s_{n + 1}, π (a o_{: n + 1}))$
$(λ o, s . 1_{π (a o_{: n + 1}) = π^{'} (a o_{: n + 1})} f_{n + 2} (a o s_{1 : n + 1}, π (a o_{1 : n + 1}), o, s) + 1_{π (a o_{1 : n + 1}) \neq π^{'} (a o_{1 : n + 1})}))$
$\geq K_{: n}^{π^{'}} (s_{0}) (λ a o s_{1 : n + 1} . K (s_{n + 1}, π^{'} (a o_{1 : n + 1})) (λ o, s . f_{n + 2} (a o s_{1 : n + 1}, π^{'} (a o_{: n + 1}), o, s)))$

Splitting into two cases, it could be that $π (a o_{1 : n + 1}) \neq π^{'} (a o_{1 : n + 1})$ . In this case that big inner function in the attempted upper bound turns into just 1, and then $K (s_{n + 1}, π (a o_{1 : n + 1})) (1) = 1$ . Or, for the $R$ type signature, we'd get $K (s_{n + 1}, π (a o_{1 : n + 1})) (\infty) = \infty$ .

In the second case where $π (a o_{1 : n + 1}) = π^{'} (a o_{1 : n + 1})$ , we'd get
$K (s_{n + 1}, π^{'} (a o_{1 : n + 1})) (λ o, s . f_{n + 2} (a o s_{1 : n + 1}, π^{'} (a o_{1 : n + 1}), o, s))$
as the value of the function inside $K_{: n}^{π^{'}} (s_{0})$ , due to the indicator function working out appropriately, and $π^{'}$ matching up with what $π$ does. This ability to break stuff up into an indicator function yields a new equivalent proof target of

$K_{: n}^{π^{'}} (s_{0}) (λ a o s_{1 : n + 1} .$
$1_{π (a o_{1 : n + 1}) = π^{'} (a o_{1 : n + 1})} K (s_{n + 1}, π^{'} (a o_{1 : n + 1})) (λ o, s . f_{n + 2} (a o s_{1 : n + 1}, π^{'} (a o_{1 : n + 1}), o, s))$
$+ 1_{π (a o_{1 : n + 1}) \neq π^{'} (a o_{1 : n + 1})})$
$\geq K_{: n}^{π^{'}} (s_{0}) (λ a o s_{1 : n + 1} . K (s_{n + 1}, π^{'} (a o_{1 : n + 1})) (λ o, s . f_{n + 2} (a o s_{1 : n + 1}, π^{'} (a o_{1 : n + 1}), o, s)))$

We would be able to show this via inframeasure monotonicity (as the starting inframeasures are equal now) if, for all $a o s_{1 : n + 1}$ , the first function was larger than the second one. Let $a o s_{1 : n + 1}$ be arbitrary, and our proof goal is now

$1_{π (a o_{1 : n + 1}) = π^{'} (a o_{1 : n + 1})} K (s_{n + 1}, π^{'} (a o_{1 : n + 1})) (λ o, s . f_{n + 2} (a o s_{1 : n + 1}, π^{'} (a o_{1 : n + 1}), o, s))$
$+ 1_{π (a o_{1 : n + 1}) \neq π^{'} (a o_{1 : n + 1})}$
$\geq K (s_{n + 1}, π^{'} (a o_{1 : n + 1})) (λ o, s . f_{n + 2} (a o s_{1 : n + 1}, π^{'} (a o_{1 : n + 1}), o, s))$

In the first subcase, where $π (a o_{1 : n + 1}) \neq π^{'} (a o_{1 : n + 1})$ , because of 1-normalization (or constants moving up), our goal would be that

$1 \geq K (s_{n + 1}, π^{'} (a o_{1 : n + 1})) (λ o, s . f_{n + 2} (a o s_{1 : n + 1}, π^{'} (a o_{1 : n + 1}), o, s))$

(or infinity). Infinity beats everything, and the inframeasures in the $[0, 1]$ type signature can report a maximum value of 1, so this proof goal is just obviously true.

In the second subcase, where $π (a o_{1 : n + 1}) = π^{'} (a o_{1 : n + 1})$ , our proof goal would turn into:

$K (s_{n + 1}, π^{'} (a o_{1 : n + 1})) (λ o, s . f_{n + 2} (a o s_{1 : n + 1}, π^{'} (a o_{1 : n + 1}), o, s))$
$\geq K (s_{n + 1}, π^{'} (a o_{1 : n + 1})) (λ o, s . f_{n + 2} (a o s_{1 : n + 1}, π^{'} (a o_{1 : n + 1}), o, s))$

But they're equal. We hit our proof goal, the induction goes through, and this hits the proof goal for establishing pseudocausality, which was the last condition we needed to show our result. We're done!