Proofs Theorem 4

post by Diffractor · 2021-12-03T18:48:07.952Z · LW · GW · 0 comments

Contents

No comments

Theorem 4: Pseudocausal IPOMDP's: If an infra-POMDP has a transition kernel $K:S\times A\stackrel{ik}{\to }O\times S$ which fulfills the niceness conditions, and there's a starting infradistribution $\psi \in \square S$, unrolling it into an infrakernel via $\Theta \left(\pi \right):=p{r}_{(A\times O{)}^{\omega }\ast }(\psi ⋉K_{:\infty }^{\pi })$ has the infrakernel $\Theta$ 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^{\pi }$ 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 $\Theta$.  Our list of conditions to show is: 

1:The $\Theta \left(\pi \right)$ have a uniform upper bound on their Lipschitz constants.

2: $\pi \mapsto \Theta \left(\pi \right)\left(U\right)$ is lower-semicontinuous for all $U$

3: $\Theta \left(\pi \right)$ is supported entirely on histories compatible with $\pi$.

4: All the $\Theta \left(\pi \right)$ agree on the value of 1 (or infinity).

5: $\Theta$ 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}^{\pi }$, showing sensible supports for $K_{:\infty }^{\pi }$, 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 $\pi \mapsto (\psi ⋉K_{:\infty }^{\pi })\left(f\right)$ 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 $\Theta$ from there.

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

Remember that $K_n^{\pi }$ is defined as

$K_n^{\pi }(s_0,ao{s}_{1:n}):={\delta }_{\pi \left(a{o}_{1:n}\right)}⋉(\lambda a.K(s_n,a\left)\right)$

Obviously it produces inframeasures, since $K$ does. 

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

${liminf}_{m\to \infty }{K}_n^{\pi }(s_0^m,ao{s}_{1:n}^m)\left(f\right)$

$={liminf}_{m\to \infty }({\delta }_{\pi \left(a{o}_{1:n}^m\right)}⋉(\lambda a.K(s_n^m,a)\left)\right)\left(f\right)$

$={liminf}_{m\to \infty }K(s_n^m,\pi (a{o}_{1:n}^m\left)\right)(\lambda o,s.f(\pi \left(a{o}_{1:n}^m\right),o,s\left)\right)$

and then, as $ao{s}_{1:n}^m$ limits to $ao{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,\pi (a{o}_{1:n}^{\infty }\left)\right)(\lambda o,s.f(\pi \left(a{o}_{1:n}^{\infty }\right),o,s\left)\right)$

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

$\ge K(s_n^{\infty },\pi (a{o}_{1:n}^{\infty }\left)\right)(\lambda o,s.f(\pi \left(a{o}_{1:n}^{\infty }\right),o,s\left)\right)$

and then we pack this back up as

$={\delta }_{\pi \left(a{o}_{1:n}^m\right)}⋉(\lambda a.K(s_n^{\infty },a\left)\right)\left(f\right)=K_n^{\pi }(s_0^{\infty },ao{s}_{1:n}^{\infty })\left(f\right)$

and lower-semicontinuity has been shown.

T4.1.2 For 1-Lipschitzness, observe that ${\delta }_{\pi \left(a{o}_{1:n}\right)}⋉(\lambda a.K(s_n,a\left)\right)$ 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,ao{s}_{1:n})\mapsto (s_n,\pi (a{o}_{1:n}\left)\right)$ is a continuous function, so any compact subset of $S\times (A\times O\times S{)}^n$ (input to $K_n^{\pi }$) 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^{\pi }$.

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

$K_n^{\pi }(s_0,ao{s}_{1:n})\left(c\right)=({\delta }_{\pi \left(a{o}_{1:n}\right)}⋉(\lambda a.K(s_n,a)\left)\right)\left(c\right)$

$={\delta }_{\pi \left(a{o}_{1:n}\right)}(\lambda a.K(s_n,a\left)\right(c\left)\right)=K(s_n,\pi (a{o}_{1:n}\left)\right)\left(c\right)\ge 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^{\pi }$ 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

$|\Theta \left(\pi \right)\left(U\right)-\Theta \left(\pi \right)\left(U^{\prime }\right)|=|p{r}_{(A\times O{)}^{\omega }\ast }(\psi ⋉K_{:\infty }^{\pi })\left(U\right)-p{r}_{(A\times O{)}^{\omega }\ast }(\psi ⋉K_{:\infty }^{\pi })\left(U^{\prime }\right)|$

$=|\psi (\lambda s_0.K_{:\infty }^{\pi }(s_0\left)\right(\lambda ao{s}_{1:\infty }.U\left(a{o}_{1:\infty }\right)\left)\right)-\psi (\lambda s_0.K_{:\infty }^{\pi }(s_0\left)\right(\lambda ao{s}_{1:\infty }.U^{\prime }\left(a{o}_{1:\infty }\right)\left)\right)|$

and then since $\psi$ is an infradistribution, it must have a finite Lipschitz constant, ${\lambda }^{\odot }$. So we then get

$\le {\lambda }^{\odot }\cdot {sup}_{s_0}|K_{:\infty }^{\pi }\left(s_0\right)(\lambda ao{s}_{1:\infty }.U(a{o}_{1:\infty }\left)\right)-K_{:\infty }^{\pi }\left(s_0\right)(\lambda ao{s}_{1:\infty }.U^{\prime }(a{o}_{1:\infty }\left)\right)|$

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

$\le {\lambda }^{\odot }{sup}_{ao{s}_{1:\infty }}|U\left(a{o}_{1:\infty }\right)-U^{\prime }\left(a{o}_{1:\infty }\right)|={\lambda }^{\odot }\cdot d(U,U^{\prime })$

and we're done, we showed a Lipschitz bound on the $\Theta \left(\pi \right)$ that is uniform in $\pi$.

T4.2.2 Now for lower-semicontinuity for $\Theta$, 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 }^{\pi }$ infrakernels simultaneously. Then, using that, we'll show that

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

$\pi \mapsto \Theta \left(\pi \right)\left(U\right)$ 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\left(S\right),ϵ>0:\exists \overline{C}\in {\prod }_{i=1}^{\infty }K(A\times O\times S):\forall \pi \in \Pi ,n,m\in N,s_0\in C^S,f\in C_B\left(\right(A\times O\times S{)}^{\omega }):$
$K_{:n+m}^{\pi }\left(s_0\right)(\lambda ao{s}_{1:n+m+1}.{inf}_{ao{s}_{n+m+2:\infty }\in {\prod }_{i=n+m+2}^{\infty }{C}_i}f(ao{s}_{1:n+m+1},ao{s}_{n+m+2:\infty }\left)\right)$
$\ge K_{:n}^{\pi }\left(s_0\right)(\lambda ao{s}_{1:n+1}.{inf}_{ao{s}_{n+2:\infty }\in {\prod }_{i=n+2}^{\infty }{C}_i}f(ao{s}_{1:n+1},ao{s}_{n+2:\infty }\left)\right)-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^{\top }[C^S,ϵ]$ where, regardless of n or $\pi$, $C_{1:n+1}^{\top }[C^S,ϵ]$ is a shared $ϵ(1-\frac{1}{2^{n+1}})$-almost-support for all the $K_{:n}^{\pi }\left(s_0\right)$ inframeasures (where $s_0\in C^S$).

Then our proof goal becomes

$\forall \pi \in \Pi ,n,m\in N,s_0\in C^S,f\in C_B\left(\right(A\times O\times S{)}^{\omega }):$
$K_{:n+m}^{\pi }\left(s_0\right)(\lambda ao{s}_{1:n+m+1}.{inf}_{ao{s}_{n+m+2:\infty }\in C_{n+m+2:\infty }^{\top }[C^S,ϵ]}f(ao{s}_{1:n+m+1},ao{s}_{n+m+2:\infty }\left)\right)$
$\ge K_{:n}^{\pi }\left(s_0\right)(\lambda ao{s}_{1:n+1}.{inf}_{ao{s}_{n+2:\infty }\in C_{n+2:\infty }^{\top }[C^S,ϵ]}f(ao{s}_{1:n+1},ao{s}_{n+2:\infty }\left)\right)-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}^{\top }[C^S,ϵ]$ is an $ϵ(1-\frac{1}{2^{n+m+1}})$-almost-support for all the $K_{:n+m}^{\pi }\left(s_0\right)$ 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^{\top }[C^S,ϵ]$ where, regardless of n or $\pi$ or $s_0\in C^S$, $C_{1:n+1}^{\top }[C^S,ϵ]$ is a $ϵ(1-\frac{1}{2^{n+1}})$-almost-support for $K_{:n}^{\pi }\left(s_0\right)$.

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

$\Xi :(0,\infty )\times A\times K\left(S\right)\to K(O,S)$

What this does is that $\Xi (ϵ,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 $\Xi$ with these properties.

Then, we recursively define the $C_i^{\top }[C^S,ϵ]$ as:

$C_1^{\top }[C^S,ϵ]:=A\times {\bigcup }_a\Xi (\frac{ϵ}{2},a,C^S)$

and

$C_{n+1}^{\top }[C^S,ϵ]:=A\times {\bigcup }_a\Xi (\frac{ϵ}{2^{n+1}},a,p{r}_{S_n}(C_{1:n}^{\top }[C^S,ϵ]\left)\right)$

All these sets are compact, by induction. For the first one, since $\Xi$ 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}^{\top }[C^S,ϵ]$ is compact, and then projections of compact sets are compact, so then $\Xi$ 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^{\top }[C^S,ϵ]$ is a $\frac{ϵ}{2}$-almost-support for $K_{:n}^{\pi }\left(s_0\right)$ with $s_0\in C^S$. Well, assume $f,f^{\prime }$ are equal on $C_1^{\top }[C^S,ϵ]$, and $s_0\in C^S$.

$|K_{:0}^{\pi }\left(s_0\right)\left(f\right)-K_{:0}^{\pi }\left(s_0\right)\left(f^{\prime }\right)|=|K_0^{\pi }\left(s_0\right)\left(f\right)-K_0^{\pi }\left(s_0\right)\left(f^{\prime }\right)|$

$=|({\delta }_{\pi \left(\right)}⋉(\lambda a.K(s_0,a)\left)\right)(\lambda a,o,s.f(a,o,s\left)\right)-({\delta }_{\pi \left(\right)}⋉(\lambda a.K(s_0,a)\left)\right)(\lambda a,o,s.f^{\prime }(a,o,s\left)\right)|$

$=|K(s_0,\pi (\left)\right)(\lambda o,s.f(\pi \left(\right),o,s\left)\right)-K(s_0,\pi (\left)\right)(\lambda o,s.f^{\prime }(\pi \left(\right),o,s\left)\right)|$

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

$\le {sup}_{o,s\in \Xi (\frac{ϵ}{2},\pi (),C^S)}|f\left(\pi \right(),o,s)-f^{\prime }\left(\pi \right(),o,s)|+\frac{ϵ}{2}{sup}_{o,s}|f\left(\pi \right(),o,s)-f^{\prime }\left(\pi \right(),o,s)|$

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

$\le {sup}_{o,s\in \Xi (\frac{ϵ}{2},\pi (),C^S)}|f\left(\pi \right(),o,s)-f^{\prime }\left(\pi \right(),o,s)|+\frac{ϵ}{2}d(f,f^{\prime })$

and then we observe that since $f=f^{\prime }$ on $C_1^{\top }[C^S,ϵ]$, and that set is defined as $A\times {\bigcup }_a\Xi (\frac{ϵ}{2},a,C^S)$ , we have that they agree on $\left\{\pi \right(\left)\right\}\times \Xi (\frac{ϵ}{2},\pi (),C^S)$

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

$\le \frac{ϵ}{2}d(f,f^{\prime })$

Showing that $C_1^{\top }[C^S,ϵ]$ is a $\frac{ϵ}{2}$-almost support for all the $K_{:0}^{\pi }\left(s_0\right)$, where $\pi$ is arbitrary and s_0\in C^{S}.

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

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

$|K_{:n+1}^{\pi }\left(s_0\right)\left(f\right)-K_{:n+1}^{\pi }\left(s_0\right)\left(f^{\prime }\right)|$

$=|K_{:n}^{\pi }\left(s_0\right)(\lambda ao{s}_{1:n+1}.K_{n+1}^{\pi }(s_0,ao{s}_{1:n+1}\left)\right(\lambda a,o,s.f(ao{s}_{1:n+1},a,o,s)\left)\right)$
$-K_{:n}^{\pi }\left(s_0\right)(\lambda ao{s}_{1:n+1}.K_{n+1}^{\pi }(s_0,ao{s}_{1:n+1}\left)\right(\lambda a,o,s.f^{\prime }(ao{s}_{1:n+1},a,o,s)\left)\right)|$

and then unpack to get

$=|K_{:n}^{\pi }\left(s_0\right)(\lambda ao{s}_{1:n+1}.({\delta }_{\pi \left(a{o}_{1:n+1}\right)}⋉(\lambda a.K(s_{n+1},a\left)\right)\left)\right(\lambda a,o,s.f(ao{s}_{1:n+1},a,o,s)\left)\right)$
$-K_{:n}^{\pi }\left(s_0\right)(\lambda ao{s}_{1:n+1}.({\delta }_{\pi \left(a{o}_{1:n+1}\right)}⋉(\lambda a.K(s_{n+1},a\left)\right)\left)\right(\lambda a,o,s.f^{\prime }(ao{s}_{1:n+1},a,o,s)\left)\right)|$

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

$=|K_{:n}^{\pi }\left(s_0\right)(\lambda ao{s}_{1:n+1}.K(s_{n+1},\pi \left(a{o}_{1:n+1}\right)\left)\right(\lambda o,s.f(ao{s}_{1:n+1},\pi (a{o}_{1:n+1}),o,s)\left)\right)$
$-K_{:n}^{\pi }\left(s_0\right)(\lambda ao{s}_{1:n+1}.K(s_{n+1},\pi \left(a{o}_{1:n+1}\right)\left)\right(\lambda o,s.f^{\prime }(ao{s}_{1:n+1},\pi (a{o}_{1:n+1}),o,s)\left)\right)|$

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

$\le {sup}_{ao{s}_{1:n+1}\in C_{1:n+1}^{\top }[C^S,ϵ]}|K(s_{n+1},\pi (a{o}_{1:n+1}\left)\right)(\lambda o,s.f(ao{s}_{1:n+1},\pi \left(a{o}_{1:n+1}\right),o,s\left)\right)$
$-K(s_{n+1},\pi (a{o}_{1:n+1}\left)\right)(\lambda o,s.f^{\prime }(ao{s}_{1:n+1},\pi \left(a{o}_{1:n+1}\right),o,s\left)\right)|$
$+ϵ(1-\frac{1}{2^{n+1}}){sup}_{ao{s}_{1:n+1}}|K(s_{n+1},\pi (a{o}_{1:n+1}\left)\right)(\lambda o,s.f(ao{s}_{1:n+1},\pi \left(a{o}_{1:n+1}\right),o,s\left)\right)$
$-K(s_{n+1},\pi (a{o}_{1:n+1}\left)\right)(\lambda o,s.f^{\prime }(ao{s}_{1:n+1},\pi \left(a{o}_{1:n+1}\right),o,s\left)\right)|$

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

$\le {sup}_{ao{s}_{1:n+1}\in C_{1:n+1}^{\top }[C^S,ϵ]}|K(s_{n+1},\pi (a{o}_{1:n+1}\left)\right)(\lambda o,s.f(ao{s}_{1:n+1},\pi \left(a{o}_{1:n+1}\right),o,s\left)\right)$
$-K(s_{n+1},\pi (a{o}_{1:n+1}\left)\right)(\lambda o,s.f^{\prime }(ao{s}_{1:n+1},\pi \left(a{o}_{1:n+1}\right),o,s\left)\right)|$
$+ϵ(1-\frac{1}{2^{n+1}}){sup}_{ao{s}_{1:n+1}}{sup}_{o,s}|f(ao{s}_{1:n+1},\pi (a{o}_{1:n+1}),o,s)-f^{\prime }(ao{s}_{1:n+1},\pi (a{o}_{1:n+1}),o,s)|$

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

$\le {sup}_{ao{s}_{1:n+1}\in C_{1:n+1}^{\top }[C^S,ϵ]}|K(s_{n+1},\pi (a{o}_{1:n+1}\left)\right)(\lambda o,s.f(ao{s}_{1:n+1},\pi \left(a{o}_{1:n+1}\right),o,s\left)\right)$
$-K(s_{n+1},\pi (a{o}_{1:n+1}\left)\right)(\lambda o,s.f^{\prime }(ao{s}_{1:n+1},\pi \left(a{o}_{1:n+1}\right),o,s\left)\right)|+ϵ(1-\frac{1}{2^{n+1}})d(f,f^{\prime })$

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

$\Xi (\frac{ϵ}{2^{n+2}},\pi (a{o}_{1:n+1}),p{r}_{S_{n+1}}(C_{1:n+1}^{\top }[C^S,ϵ]\left)\right)$

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

$\le {sup}_{ao{s}_{1:n+1}\in C_{1:n+1}^{\top }[C^S,ϵ]}({sup}_{o,s\in \Xi (\frac{ϵ}{2^{n+2}},\pi (a{o}_{1:n+1}),p{r}_{S_{n+1}}(C_{1:n+1}^{\top }[C^S,ϵ]\left)\right)}$
$|f(ao{s}_{1:n+1},\pi (a{o}_{1:n+1}),o,s)-f^{\prime }(ao{s}_{1:n+1},\pi (a{o}_{1:n+1}),o,s)|$
$+\frac{ϵ}{2^{n+2}}{sup}_{o,s}|f(ao{s}_{1:n+1},\pi (a{o}_{1:n+1}),o,s)-f^{\prime }(ao{s}_{1:n+1},\pi (a{o}_{1:n+1}),o,s)|)$
$+ϵ(1-\frac{1}{2^{n+1}})d(f,f^{\prime })$

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

$\le {sup}_{ao{s}_{1:n+1}\in C_{1:n+1}^{\top }[C^S,ϵ]}({sup}_{o,s\in \Xi (\frac{ϵ}{2^{n+2}},\pi (a{o}_{1:n+1}),p{r}_{S_{n+1}}(C_{1:n+1}^{\top }[C^S,ϵ]\left)\right)}$
$|f(ao{s}_{1:n+1},\pi (a{o}_{1:n+1}),o,s)-f^{\prime }(ao{s}_{1:n+1},\pi (a{o}_{1:n+1}),o,s)|$
$+\frac{ϵ}{2^{n+2}}d(f,f^{\prime }))+ϵ(1-\frac{1}{2^{n+1}})d(f,f^{\prime })$

Pull out the constant and combine, to get

$={sup}_{ao{s}_{1:n+1}\in C_{1:n+1}^{\top }[C^S,ϵ]}({sup}_{o,s\in \Xi (\frac{ϵ}{2^{n+2}},\pi (a{o}_{1:n+1}),p{r}_{S_{n+1}}(C_{1:n+1}^{\top }[C^S,ϵ]\left)\right)}$
$|f(ao{s}_{1:n+1},\pi (a{o}_{1:n+1}),o,s)-f^{\prime }(ao{s}_{1:n+1},\pi (a{o}_{1:n+1}),o,s)|)$
$+ϵ(1-\frac{1}{2^{n+2}})d(f,f^{\prime })$

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

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

and then expands as

$C_{1:n+1}^{\top }[C^S,ϵ]\times (A\times {\bigcup }_a\Xi (\frac{ϵ}{2^{n+2}},a,p{r}_{S_{n+1}}(C_{1:n+1}^{\top }[C^S,ϵ]\left)\right))$

which all our $ao{s}_{1:n+1},\pi \left(a{o}_{1:n+1}\right),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^{\prime })$

Which witnesses that $C_{1:n+2}^{\top }[C^S,ϵ]$ is a $ϵ(1-\frac{1}{2^{n+2}})$-almost-support for any $K_{:n+1}^{\pi }\left(s_0\right)$ (arbitrary $\pi$) 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^{\top }[C^S,ϵ]$sequence is suitable to get our modification of the Almost-Monotone-Lemma to work out. We have the result 

$\forall \pi \in \Pi ,n,m\in N,s_0\in C^S,f\in C_B\left(\right(A\times O\times S{)}^{\omega }):$
$K_{:n+m}^{\pi }\left(s_0\right)(\lambda ao{s}_{1:n+m+1}.{inf}_{ao{s}_{n+m+2:\infty }\in C_{n+m+2:\infty }^{\top }[C^S,ϵ]}f(ao{s}_{1:n+m+1},ao{s}_{n+m+2:\infty }\left)\right)$
$\ge K_{:n}^{\pi }\left(s_0\right)(\lambda ao{s}_{1:n+1}.{inf}_{ao{s}_{n+2:\infty }\in C_{n+2:\infty }^{\top }[C^S,ϵ]}f(ao{s}_{1:n+1},ao{s}_{n+2:\infty }\left)\right)-4ϵ||f||$

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

$\forall \pi \in \Pi ,n^{\ast }\in N,s_0\in C^S,f\in C_B\left(\right(A\times O\times S{)}^{\omega }):$
${lim}_{n\to \infty }{K}_{:n}^{\pi }\left(s_0\right)(\lambda ao{s}_{1:n+1}.{inf}_{ao{s}_{n+2:\infty }\in C_{n+2:\infty }^{\top }[C^S,ϵ]}f(ao{s}_{1:n+1},ao{s}_{n+2:\infty }\left)\right)$
$\ge K_{:n^{\ast }}^{\pi }\left(s_0\right)(\lambda ao{s}_{1:n^{\ast }+1}.{inf}_{ao{s}_{n^{\ast }+2:\infty }\in C_{n^{\ast }+2:\infty }^{\top }[C^S,ϵ]}f(ao{s}_{1:n^{\ast }+1},ao{s}_{n^{\ast }+2:\infty }\left)\right)-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 $\pi \mapsto (\psi ⋉K_{:\infty }^{\pi })\left(f\right)$ 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 }(\psi ⋉K_{:\infty }^{{\pi }_m})\left(f\right)$

Which unpacks as

$={liminf}_{m\to \infty }\psi (\lambda s_0.K_{:\infty }^{{\pi }_m}(s_0\left)\right(\lambda ao{s}_{1:\infty }.f(s_0,ao{s}_{1:\infty })\left)\right)$

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 $\psi$ as a challenge of picking points in $\Psi$, so we get

$={liminf}_{m\to \infty }\left({inf}_{(m,b)\in \Psi }\left(m\right(\lambda s_0.K_{:\infty }^{{\pi }_m}\left(s_0\right)(\lambda ao{s}_{1:\infty }.f(s_0,ao{s}_{1:\infty }\left)\right))+b)\right)$

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

$={liminf}_{m\to \infty }\left({inf}_{(m,b)\in {\Psi }^{min}}\left(m\right(\lambda s_0.K_{:\infty }^{{\pi }_m}\left(s_0\right)(\lambda ao{s}_{1:\infty }.f(s_0,ao{s}_{1:\infty }\left)\right))+b)\right)$

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 $\lambda s_0.K_{:\infty }^{{\pi }_m}\left(s_0\right)\left(f\right)$ function can't be unbounded below, because it is above $K_{:\infty }^{{\pi }_m}\left(s_0\right)(-||f||)$, and infinite semidirect products map constants to greater than their usual value, and $K_{:\infty }^{{\pi }_m}\left(s_0\right)$ fulfills this condition. Thus, if the b value of a selected minimal point is far higher than the finite liminf value plus ${\lambda }^{\odot }||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 $\Psi$ to attain the min, call it $C^{\Psi }$. With this, we get

$={liminf}_{m\to \infty }\left({inf}_{(m,b)\in C^{\Psi }}\left(m\right(\lambda s_0.K_{:\infty }^{{\pi }_m}\left(s_0\right)(\lambda ao{s}_{1:\infty }.f(s_0,ao{s}_{1:\infty }\left)\right))+b)\right)$

And then we unpack this as an integral.

$=\underset{m\to \infty }{liminf}\left(\underset{(m,b)\in C^{\Psi }}{inf}\left({\int }_S\right(\lambda s_0.K_{:\infty }^{{\pi }_m}\left(s_0\right)(\lambda ao{s}_{1:\infty }.f(s_0,ao{s}_{1:\infty }\left)\right))dm+b)\right)$

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 ${\pi }_{\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(\lambda s_0.K_{:\infty }^{{\pi }_m}(s_0\left)\right(\lambda ao{s}_{1:\infty }.f(s_0,ao{s}_{1:\infty })\left)\right)dm+b$

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

$\lambda s_0.K_{:\infty }^{{\pi }_m}\left(s_0\right)(\lambda ao{s}_{1:\infty }.f(s_0,ao{s}_{1:\infty }\left)\right)$

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^{\Psi }$, 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

$=\underset{i\to \infty }{lim}\left({\int }_S\right(\lambda s_0.K_{:\infty }^{{\pi }_i}\left(s_0\right)(\lambda ao{s}_{1:\infty }.f(s_0,ao{s}_{1:\infty }\left)\right))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

$=\underset{i\to \infty }{lim}\left({\int }_S\right(\lambda s_0.K_{:\infty }^{{\pi }_i}\left(s_0\right)(\lambda ao{s}_{1:\infty }.f(s_0,ao{s}_{1:\infty }\left)\right)\left)d{m}_i\right)+b_{\infty }$

At this point, since the $m_i$ limit to $m_{\infty }$, the set of the measure components $\{m_i{\}}_{i\in N\bigsqcup \left\{\infty \right\}}$ 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.

$=\underset{i\to \infty }{lim}\left({\int }_S\right(\lambda s_0.K_{:\infty }^{{\pi }_i}\left(s_0\right)(\lambda ao{s}_{1:\infty }.f(s_0,ao{s}_{1:\infty }\left)\right))d{m}_{i,C^S}$
$+{\int }_S(\lambda s_0.K_{:\infty }^{{\pi }_i}(s_0\left)\right(\lambda ao{s}_{1:\infty }.f(s_0,ao{s}_{1:\infty })\left)\right)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^{\top }[C^S,ϵ]$ sequence that attains almost-monotonicity. To economize on space for the lines to fit, we'll write 

${inf}_{ao{s}_{n+2:\infty }\in C_{n+2:\infty }^{\top }[C^S,ϵ]}f(s_0,ao{s}_{1:n+1},ao{s}_{n+2:\infty })$

as just

${inf}_{C_{n+2:\infty }^{\top }[C^S,ϵ]}f(s_0,ao{s}_{1:n+1},ao{s}_{n+2:\infty })$

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

$=\underset{i\to \infty }{lim}\left({\int }_S\right(\lambda s_0.\underset{n\to \infty }{lim}\left(K_{:n}^{{\pi }_i}\right(s_0\left)\right(\lambda ao{s}_{1:n+1}.\underset{C_{n+2:\infty }^{\top }[C^S,ϵ]}{inf}f(s_0,ao{s}_{1:n+1},ao{s}_{n+2:\infty })\left)\right))d{m}_{i,C^S}$
$+{\int }_S(\lambda s_0.\underset{n\to \infty }{lim}(K_{:n}^{{\pi }_m}\left(s_0\right)(\lambda ao{s}_{1:n+1}.\underset{C_{n+2:\infty }^{\top }[C^S,ϵ]}{inf}f(s_0,ao{s}_{1:n+1},ao{s}_{n+2:\infty }\left)\right)\left)\right)d{m}_{i,\neg C^S})+b_{\infty }$

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

$=\underset{i\to \infty }{lim}\left({\int }_S\right(\lambda s_0.\underset{n\to \infty }{lim}\left(K_{:n}^{{\pi }_i}\right(s_0\left)\right(\lambda ao{s}_{1:n+1}.\underset{C_{n+2:\infty }^{\top }[C^S,ϵ]}{inf}f(s_0,ao{s}_{1:n+1},ao{s}_{n+2:\infty })\left)\right))d{m}_{i,C^S}$
$+{\int }_S(\lambda s_0.K_{:n^{\ast }}^{{\pi }_i}(s_0\left)\right(\lambda ao{s}_{1:n^{\ast }+1}.\underset{C_{n^{\ast }+2:\infty }^{\top }[C^S,ϵ]}{inf}f(s_0,ao{s}_{1:n^{\ast }+1},ao{s}_{n^{\ast }+2:\infty })\left)\right)d{m}_{i,\neg C^S}$
$+{\int }_S(\lambda s_0.\underset{n\to \infty }{lim}(K_{:n}^{{\pi }_i}\left(s_0\right)(\lambda ao{s}_{1:n+1}.\underset{C_{n+2:\infty }^{\top }[C^S,ϵ]}{inf}f(s_0,ao{s}_{1:n+1},ao{s}_{n+2:\infty }\left)\right))$
$-K_{:n^{\ast }}^{{\pi }_i}\left(s_0\right)(\lambda ao{s}_{1:n^{\ast }+1}.{inf}_{C_{n^{\ast }+2:\infty }^{\top }[C^S,ϵ]}f(s_0,ao{s}_{1:n^{\ast }+1},ao{s}_{n^{\ast }+2:\infty }\left)\right)\left)d{m}_{i,\neg C^S}\right)+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 }\left(K_{:n}^{{\pi }_i}\right(s_0\left)\right(\lambda ao{s}_{1:n+1}.{inf}_{C_{n+2:\infty }^{\top }[C^S,ϵ]}f(s_0,ao{s}_{1:n+1},ao{s}_{n+2:\infty })\left)\right)$
$-K_{:n^{\ast }}^{{\pi }_i}\left(s_0\right)(\lambda ao{s}_{1:n^{\ast }+1}.{inf}_{C_{n^{\ast }+2:\infty }^{\top }[C^S,ϵ]}f(s_0,ao{s}_{1:n^{\ast }+1},ao{s}_{n^{\ast }+2:\infty }\left)\right)\ge -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\ge n^{\ast }$. So let $n\ge n^{\ast }$. Then, our proof goal is that

$K_{:n}^{{\pi }_i}\left(s_0\right)(\lambda ao{s}_{1:n+1}.{inf}_{C_{n+2:\infty }^{\top }[C^S,ϵ]}f(s_0,ao{s}_{1:n+1},ao{s}_{n+2:\infty }\left)\right)$
$-K_{:n^{\ast }}^{{\pi }_i}\left(s_0\right)(\lambda ao{s}_{1:n^{\ast }+1}.{inf}_{C_{n^{\ast }+2:\infty }^{\top }[C^S,ϵ]}f(s_0,ao{s}_{1:n^{\ast }+1},ao{s}_{n^{\ast }+2:\infty }\left)\right)\ge -2||f||$

First, observe that the functions

$\lambda ao{s}_{1:n+1}.{inf}_{C_{n+2:\infty }^{\top }[C^S,ϵ]}f(s_0,ao{s}_{1:n+1},ao{s}_{n+2:\infty })$

and

$\lambda ao{s}_{1:n+1}.{inf}_{C_{n^{\ast }+2:\infty }^{\top }[C^S,ϵ]}f(s_0,ao{s}_{1:n^{\ast }+1},ao{s}_{n^{\ast }+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

$K_{:n}^{{\pi }_i}\left(s_0\right)(\lambda ao{s}_{1:n+1}.{inf}_{C_{n+2:\infty }^{\top }[C^S,ϵ]}f(s_0,ao{s}_{1:n+1},ao{s}_{n+2:\infty }\left)\right)$
$-K_{:n^{\ast }}^{{\pi }_i}\left(s_0\right)(\lambda ao{s}_{1:n^{\ast }+1}.{inf}_{C_{n^{\ast }+2:\infty }^{\top }[C^S,ϵ]}f(s_0,ao{s}_{1:n^{\ast }+1},ao{s}_{n^{\ast }+2:\infty }\left)\right)$

$\ge K_{:n}^{{\pi }_i}\left(s_0\right)(\lambda ao{s}_{1:n+1}.{inf}_{C_{n^{\ast }+2:\infty }^{\top }[C^S,ϵ]}f(s_0,ao{s}_{1:n^{\ast }+1},ao{s}_{n^{\ast }+2:\infty }\left)\right)-2||f||$
$-K_{:n^{\ast }}^{{\pi }_i}\left(s_0\right)(\lambda ao{s}_{1:n^{\ast }+1}.{inf}_{C_{n^{\ast }+2:\infty }^{\top }[C^S,ϵ]}f(s_0,ao{s}_{1:n^{\ast }+1},ao{s}_{n^{\ast }+2:\infty }\left)\right)$

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

$\ge K_{:n^{\ast }}^{{\pi }_i}\left(s_0\right)(\lambda ao{s}_{1:n^{\ast }+1}.{inf}_{C_{n^{\ast }+2:\infty }^{\top }[C^S,ϵ]}f(s_0,ao{s}_{1:n^{\ast }+1},ao{s}_{n^{\ast }+2:\infty }\left)\right)-2||f||$
$-K_{:n^{\ast }}^{{\pi }_i}\left(s_0\right)(\lambda ao{s}_{1:n^{\ast }+1}.{inf}_{C_{n^{\ast }+2:\infty }^{\top }[C^S,ϵ]}f(s_0,ao{s}_{1:n^{\ast }+1},ao{s}_{n^{\ast }+2:\infty }\left)\right)$

$=-2||f||$

And we're done, we have shown that, regardless of $s_0$, we have

${lim}_{n\to \infty }\left(K_{:n}^{{\pi }_i}\right(s_0\left)\right(\lambda ao{s}_{1:n+1}.{inf}_{C_{n+2:\infty }^{\top }[C^S,ϵ]}f(s_0,ao{s}_{1:n+1},ao{s}_{n+2:\infty })\left)\right)$
$-K_{:n^{\ast }}^{{\pi }_i}\left(s_0\right)(\lambda ao{s}_{1:n^{\ast }+1}.{inf}_{C_{n^{\ast }+2:\infty }^{\top }[C^S,ϵ]}f(s_0,ao{s}_{1:n^{\ast }+1},ao{s}_{n^{\ast }+2:\infty }\left)\right)\ge -2||f||$

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

$\underset{i\to \infty }{lim}\left({\int }_S\right(\lambda s_0.\underset{n\to \infty }{lim}\left(K_{:n}^{{\pi }_i}\right(s_0\left)\right(\lambda ao{s}_{1:n+1}.\underset{C_{n+2:\infty }^{\top }[C^S,ϵ]}{inf}f(s_0,ao{s}_{1:n+1},ao{s}_{n+2:\infty })\left)\right))d{m}_{i,C^S}$
$+{\int }_S(\lambda s_0.K_{:n^{\ast }}^{{\pi }_i}(s_0\left)\right(\lambda ao{s}_{1:n^{\ast }+1}.\underset{C_{n^{\ast }+2:\infty }^{\top }[C^S,ϵ]}{inf}f(s_0,ao{s}_{1:n^{\ast }+1},ao{s}_{n^{\ast }+2:\infty })\left)\right)d{m}_{i,\neg C^S}$
$+{\int }_S(\lambda s_0.\underset{n\to \infty }{lim}(K_{:n}^{{\pi }_i}\left(s_0\right)(\lambda ao{s}_{1:n+1}.\underset{C_{n+2:\infty }^{\top }[C^S,ϵ]}{inf}f(s_0,ao{s}_{1:n+1},ao{s}_{n+2:\infty }\left)\right))$
$-K_{:n^{\ast }}^{{\pi }_i}\left(s_0\right)(\lambda ao{s}_{1:n^{\ast }+1}.{inf}_{C_{n^{\ast }+2:\infty }^{\top }[C^S,ϵ]}f(s_0,ao{s}_{1:n^{\ast }+1},ao{s}_{n^{\ast }+2:\infty }\left)\right)\left)d{m}_{i,\neg C^S}\right)+b_{\infty }$

and apply our lower-bound to get

$\ge \underset{i\to \infty }{liminf}\left({\int }_S\right(\lambda s_0.\underset{n\to \infty }{lim}\left(K_{:n}^{{\pi }_i}\right(s_0\left)\right(\lambda ao{s}_{1:n+1}.\underset{C_{n+2:\infty }^{\top }[C^S,ϵ]}{inf}f(s_0,ao{s}_{1:n+1},ao{s}_{n+2:\infty })\left)\right))d{m}_{i,C^S}$
$+{\int }_S(\lambda s_0.K_{:n^{\ast }}^{{\pi }_i}(s_0\left)\right(\lambda ao{s}_{1:n^{\ast }+1}.\underset{C_{n^{\ast }+2:\infty }^{\top }[C^S,ϵ]}{inf}f(s_0,ao{s}_{1:n^{\ast }+1},ao{s}_{n^{\ast }+2:\infty })\left)\right)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:

$\ge \underset{i\to \infty }{liminf}\left({\int }_S\right(\lambda s_0.\underset{n\to \infty }{lim}\left(K_{:n}^{{\pi }_i}\right(s_0\left)\right(\lambda ao{s}_{1:n+1}.\underset{C_{n+2:\infty }^{\top }[C^S,ϵ]}{inf}f(s_0,ao{s}_{1:n+1},ao{s}_{n+2:\infty })\left)\right))d{m}_{i,C^S}$
$+{\int }_S(\lambda s_0.K_{:n^{\ast }}^{{\pi }_i}(s_0\left)\right(\lambda ao{s}_{1:n^{\ast }+1}.\underset{C_{n^{\ast }+2:\infty }^{\top }[C^S,ϵ]}{inf}f(s_0,ao{s}_{1:n^{\ast }+1},ao{s}_{n^{\ast }+2:\infty })\left)\right)d{m}_{i,\neg C^S})-2ϵ||f||+b_{\infty }$

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^{\ast }$ finite stage, minus $4ϵ||f||$ (independently of the choice of ${\pi }_i$) yielding

$\ge \underset{i\to \infty }{liminf}\left({\int }_S\right(\lambda s_0.K_{:n^{\ast }}^{{\pi }_i}\left(s_0\right)(\lambda ao{s}_{1:n^{\ast }+1}.\underset{C_{n^{\ast }+2:\infty }^{\top }[C^S,ϵ]}{inf}f(s_0,ao{s}_{1:n^{\ast }+1},ao{s}_{n^{\ast }+2:\infty }\left)\right)-4ϵ||f||)d{m}_{i,C^S}$
$+{\int }_S(\lambda s_0.K_{:n^{\ast }}^{{\pi }_i}(s_0\left)\right(\lambda ao{s}_{1:n^{\ast }+1}.\underset{C_{n^{\ast }+2:\infty }^{\top }[C^S,ϵ]}{inf}f(s_0,ao{s}_{1:n^{\ast }+1},ao{s}_{n^{\ast }+2:\infty })\left)\right)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:

$=\underset{i\to \infty }{liminf}\left({\int }_S\right(\lambda s_0.K_{:n^{\ast }}^{{\pi }_i}\left(s_0\right)(\lambda ao{s}_{1:n^{\ast }+1}.\underset{C_{n^{\ast }+2:\infty }^{\top }[C^S,ϵ]}{inf}f(s_0,ao{s}_{1:n^{\ast }+1},ao{s}_{n^{\ast }+2:\infty }\left)\right))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 $\Psi$ or a limit of such, so the maximal amount of measure present would be ${\lambda }^{\odot }$. This lets us get a lower bound of

$\ge \underset{i\to \infty }{liminf}{\int }_S(\lambda s_0.K_{:n^{\ast }}^{{\pi }_i}(s_0\left)\right(\lambda ao{s}_{1:n^{\ast }+1}.\underset{C_{n^{\ast }+2:\infty }^{\top }[C^S,ϵ]}{inf}f(s_0,ao{s}_{1:n^{\ast }+1},ao{s}_{n^{\ast }+2:\infty })\left)\right)d{m}_i$
$-4ϵ{\lambda }^{\odot }||f||-2ϵ||f||+b_{\infty }$

Doing a little bit of regrouping, we have

$=\underset{i\to \infty }{liminf}{\int }_S(\lambda s_0.K_{:n^{\ast }}^{{\pi }_i}(s_0\left)\right(\lambda ao{s}_{1:n^{\ast }+1}.\underset{C_{n^{\ast }+2:\infty }^{\top }[C^S,ϵ]}{inf}f(s_0,ao{s}_{1:n^{\ast }+1},ao{s}_{n^{\ast }+2:\infty })\left)\right)d{m}_i$
$-2ϵ||f||(2{\lambda }^{\odot }+1)+b_{\infty }$

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

${liminf}_{m\to \infty }(\psi ⋉K_{:\infty }^{{\pi }_m})\left(f\right)$

$\ge \underset{i\to \infty }{liminf}{\int }_S(\lambda s_0.K_{:n^{\ast }}^{{\pi }_i}(s_0\left)\right(\lambda ao{s}_{1:n^{\ast }+1}.\underset{C_{n^{\ast }+2:\infty }^{\top }[C^S,ϵ]}{inf}f(s_0,ao{s}_{1:n^{\ast }+1},ao{s}_{n^{\ast }+2:\infty })\left)\right)d{m}_i$
$-2ϵ||f||(2{\lambda }^{\odot }+1)+b_{\infty }$

For all $n^{\ast }$. Regardless of $n^{\ast }$, 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^{\top }[C^S,ϵ]$ were fixed before we picked $n^{\ast }$, we can take a limit of the $n^{\ast }$ without worrying about it affecting any of the stuff on the inside of the integral, to get

${liminf}_{m\to \infty }(\psi ⋉K_{:\infty }^{{\pi }_m})\left(f\right)$

$\ge \underset{n\to \infty }{liminf}\underset{i\to \infty }{liminf}{\int }_S(\lambda s_0.K_{:n}^{{\pi }_i}(s_0\left)\right(\lambda ao{s}_{1:n+1}.\underset{C_{n+2:\infty }^{\top }[C^S,ϵ]}{inf}f(s_0,ao{s}_{1:n+1},ao{s}_{n+2:\infty })\left)\right)d{m}_i$
$-2ϵ||f||(2{\lambda }^{\odot }+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}^{{\pi }_i}$ will become $K_{:n}^{{\pi }_{\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:

$=\underset{n\to \infty }{liminf}\underset{i\to \infty }{liminf}{\int }_S(\lambda s_0.K_{:n}^{{\pi }_{\infty }}(s_0\left)\right(\lambda ao{s}_{1:n+1}.\underset{C_{n+2:\infty }^{\top }[C^S,ϵ]}{inf}f(s_0,ao{s}_{1:n+1},ao{s}_{n+2:\infty })\left)\right)d{m}_i$
$-2ϵ||f||(2{\lambda }^{\odot }+1)+b_{\infty }$

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

$\lambda s_0.K_{:n}^{{\pi }_{\infty }}\left(s_0\right)(\lambda ao{s}_{1:n+1}.{inf}_{C_{n+2:\infty }[C^S,ϵ]}f(s_0,ao{s}_{1:n+1},ao{s}_{n+2:\infty }\left)\right)$

is lower-semicontinuous in $s_0$ (as all the finite stages of the infinite infrakernel have that niceness property). And $m\mapsto m\left(f^{\ast }\right)$ is lower-semicontinuous when $f^{\ast }$ 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

$\ge \underset{n\to \infty }{liminf}{\int }_S(\lambda s_0.K_{:n}^{{\pi }_{\infty }}(s_0\left)\right(\lambda ao{s}_{1:n+1}.\underset{C_{n+2:\infty }^{\top }[C^S,ϵ]}{inf}f(s_0,ao{s}_{1:n+1},ao{s}_{n+2:\infty })\left)\right)d{m}_{\infty }$
$+b_{\infty }-2ϵ||f||(2{\lambda }^{\odot }+1)$

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

$\lambda s_0.K_{:n}^{{\pi }_{\infty }}\left(s_0\right)(\lambda ao{s}_{1:n+1}.{inf}_{C_{n+2:\infty }^{\top }[C^S,ϵ]}f(s_0,ao{s}_{1:n+1},ao{s}_{n+2:\infty }\left)\right)$

converge pointwise in n to the function

$\lambda s_0.K_{:\infty }^{{\pi }_{\infty }}\left(s_0\right)(\lambda ao{s}_{1:\infty }.f(s_0,ao{s}_{1:\infty }\left)\right)$

(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

$\ge {\int }_S(\lambda s_0.\underset{n\to \infty }{liminf}{K}_{:n}^{{\pi }_{\infty }}(s_0\left)\right(\lambda ao{s}_{1:n+1}.\underset{C_{n+2:\infty }^{\top }[C^S,ϵ]}{inf}f(s_0,ao{s}_{1:n+1},ao{s}_{n+2:\infty })\left)\right)d{m}_{\infty }$
$+b_{\infty }-2ϵ||f||(2{\lambda }^{\odot }+1)$

And since we have pointwise limiting, this is

$={\int }_S(\lambda s_0.\underset{n\to \infty }{lim}{K}_{:n}^{{\pi }_{\infty }}(s_0\left)\right(\lambda ao{s}_{1:n+1}.\underset{C_{n+2:\infty }^{\top }[C^S,ϵ]}{inf}f(s_0,ao{s}_{1:n+1},ao{s}_{n+2:\infty })\left)\right)d{m}_{\infty }$
$+b_{\infty }-2ϵ||f||(2{\lambda }^{\odot }+1)$

and then, packing it up,

$={\int }_S(\lambda s_0.K_{:\infty }^{{\pi }_{\infty }}(s_0\left)\right(\lambda ao{s}_{1:\infty }.f(s_0,ao{s}_{1:\infty })\left)\right)d{m}_{\infty }+b_{\infty }-2ϵ||f||(2{\lambda }^{\odot }+1)$

And then, pack it up as

$=m_{\infty }(\lambda s_0.K_{:\infty }^{{\pi }_{\infty }}(s_0\left)\right(\lambda ao{s}_{1:\infty }.f(s_0,ao{s}_{1:\infty })\left)\right)+b_{\infty }-2ϵ||f||(2{\lambda }^{\odot }+1)$

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

$\ge {inf}_{(m,b)\in \Psi }\left(m\right(\lambda s_0.K_{:\infty }^{{\pi }_{\infty }}\left(s_0\right)(\lambda ao{s}_{1:\infty }.f(s_0,ao{s}_{1:\infty }\left)\right))+b)-2ϵ||f||(2{\lambda }^{\odot }+1)$

which reexpresses as

$=\psi (\lambda s_0.K_{:\infty }^{{\pi }_{\infty }}(s_0\left)\right(\lambda ao{s}_{1:\infty }.f(s_0,ao{s}_{1:\infty })\left)\right)-2ϵ||f||(2{\lambda }^{\odot }+1)$

$=(\psi ⋉K_{:\infty }^{{\pi }_{\infty }})\left(f\right)-2ϵ||f||(2{\lambda }^{\odot }+1)$

Our net result is

${liminf}_{m\to \infty }(\psi ⋉K_{:\infty }^{{\pi }_m})\left(f\right)\ge (\psi ⋉K_{:\infty }^{{\pi }_{\infty }})\left(f\right)-2ϵ||f||(2{\lambda }^{\odot }+1)$

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

${liminf}_{m\to \infty }(\psi ⋉K_{:\infty }^{{\pi }_m})\left(f\right)\ge (\psi ⋉K_{:\infty }^{{\pi }_{\infty }})\left(f\right)$

And lower-semicontinuity is shown for $\pi \mapsto (\psi ⋉K_{:\infty }^{\pi })\left(f\right)$

T4.2.2.3 Now for our phase 3, getting lower-semicontinuity of $\pi \mapsto \Theta \left(\pi \right)\left(U\right)$. Let ${\pi }_m$ limit to ${\pi }_{\infty }$. We have

${liminf}_{m\to \infty }\Theta \left({\pi }_m\right)\left(U\right)$

and then this unpacks as

$={liminf}_{m\to \infty }p{r}_{(A\times O{)}^{\omega }\ast }(\psi ⋉K_{:\infty }^{{\pi }_m})\left(U\right)$

Reexpressing the projection, we have:

$={liminf}_{m\to \infty }(\psi ⋉K_{:\infty }^{{\pi }_m})(\lambda s_0,ao{s}_{1:\infty }.U(a{o}_{1:\infty }\left)\right)$

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

$\ge (\psi ⋉K_{:\infty }^{{\pi }_{\infty }})(\lambda s_0,ao{s}_{1:\infty }.U(a{o}_{1:\infty }\left)\right)$

Which then packs up as

$=p{r}_{(A\times O{)}^{\omega }\ast }(\psi ⋉K_{:\infty }^{{\pi }_{\infty }})\left(U\right)$

and then

$=\Theta \left({\pi }_{\infty }\right)\left(U\right)$

and we have lower-semicontinuity for $\Theta$! Finally!

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

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

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

$K_{:\infty }^{\pi }\left(s_0\right)(\lambda ao{s}_{1:\infty }.U(a{o}_{1:\infty }\left)\right)=K_{:\infty }^{\pi }\left(s_0\right)(\lambda ao{s}_{1:\infty }.U^{\prime }(a{o}_{1:\infty }\left)\right)$

Finally, we use this result to show that if $U,U^{\prime }$ agree on all histories compatible with $\pi$, $\Theta \left(\pi \right)\left(U\right)=\Theta \left(\pi \right)\left(U^{\prime }\right)$, showing that $\Theta \left(\pi \right)$ is supported on histories compatible with $\pi$.

T4.2.3.1 Let's start with the induction proof that $K_{:n}^{\pi }\left(s_0\right)$ has the subset of $(A\times O\times S{)}^{n+1}$ where the history of actions and observations is compatible with $\pi$ 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^{\prime }$ which are identical on $\left\{\pi \right(\left)\right\}\times O\times S$ (as that's the subset of $A\times O\times S$ which is compatible with $\pi$), and observe:

$K_{:0}^{\pi }\left(s_0\right)\left(f\right)=K_0^{\pi }\left(s_0\right)(\lambda a,o,s.f(a,o,s\left)\right)$

and then by how $K_0^{\pi }\left(s_0\right)$ is defined, we have

$=({\delta }_{\pi \left(\right)}⋉(\lambda a.K(s_0,a)\left)\right)(\lambda a^{\prime },o,s.f(a^{\prime },o,s\left)\right)$

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

$=K(s_0,\pi (\left)\right)(\lambda o,s.f(\pi \left(\right),o,s\left)\right)$

and then since $f=f^{\prime }$ when the initial action equals $\pi \left(\right)$, we have

$=K(s_0,\pi (\left)\right)(\lambda o,s.f^{\prime }(\pi \left(\right),o,s\left)\right)$

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

$=K_{:0}^{\pi }\left(s_0\right)\left(f^{\prime }\right)$

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

$|K_{:n+1}^{\pi }\left(s_0\right)\left(f\right)-K_{:n+1}^{\pi }\left(s_0\right)\left(f^{\prime }\right)|$

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

$=|K_{:n}^{\pi }\left(s_0\right)(\lambda ao{s}_{1:n+1}.K_{n+1}^{\pi }(s_0,ao{s}_{1:n+1}\left)\right(\lambda a,o,s.f(ao{s}_{1:n+1},a,o,s)\left)\right)$
$-K_{:n}^{\pi }\left(s_0\right)(\lambda ao{s}_{1:n+1}.K_{n+1}^{\pi }(s_0,ao{s}_{1:n+1}\left)\right(\lambda a,o,s.f^{\prime }(ao{s}_{1:n+1},a,o,s)\left)\right)|$

Now, since, by induction assumption, $K_{:n}^{\pi }\left(s_0\right)$ is supported on the subset of $(A\times O\times S{)}^{n+1}$ where the history is compatible with $\pi$, 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 ao{s}_{1:n+1}\sim \pi :K_{n+1}^{\pi }(s_0,ao{s}_{1:n+1})(\lambda a,o,s.f(ao{s}_{1:n+1},a,o,s\left)\right)$
$=K_{n+1}^{\pi }(s_0,ao{s}_{1:n+1})(\lambda a,o,s.f^{\prime }(ao{s}_{1:n+1},a,o,s\left)\right)$

We now unpack $K_{n+1}^{\pi }(s_0,ao{s}_{1:n+1})$ as ${\delta }_{\pi \left(a{o}_{1:n+1}\right)}⋉(\lambda a.K(s_{n+1},a\left)\right)$ to get our new proof goal of:

$\forall ao{s}_{1:n+1}\sim \pi :({\delta }_{\pi \left(a{o}_{1:n+1}\right)}⋉(\lambda a.K(s_{n+1},a)\left)\right)(\lambda a^{\prime },o,s.f(ao{s}_{1:n+1},a^{\prime },o,s\left)\right)$
$=({\delta }_{\pi \left(a{o}_{1:n+1}\right)}⋉(\lambda a.K(s_{n+1},a)\left)\right)(\lambda a^{\prime },o,s.f^{\prime }(ao{s}_{1:n+1},a^{\prime },o,s\left)\right)$

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

$\forall ao{s}_{1:n+1}\sim \pi :K(s_{n+1},\pi (a{o}_{1:n+1}\left)\right)(\lambda o,s.f(ao{s}_{1:n+1},\pi \left(a{o}_{1:n+1}\right),o,s\left)\right)$
$=K(s_{n+1},\pi (a{o}_{1:n+1}\left)\right)(\lambda o,s.f^{\prime }(ao{s}_{1:n+1},\pi \left(a{o}_{1:n+1}\right),o,s\left)\right)$

at this point, we realize that if $ao{s}_{1:n+1}$ is compatible with $\pi$, then regardless of $o$ and $s$, $ao{s}_{1:n+1},\pi \left(a{o}_{1:n+1}\right),o,s$ is compatible with $\pi$, so the functions

$\lambda o,s.f(ao{s}_{1:n+1},\pi (a{o}_{1:n+1}),o,s)$

and

$\lambda o,s.f^{\prime }(ao{s}_{1:n+1},\pi (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 $\pi$ will always be a support of $K_{:n}^{\pi }$ for all n.

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

$K_{:\infty }^{\pi }\left(s_0\right)(\lambda ao{s}_{1:\infty }.U(a{o}_{1:\infty }\left)\right)=K_{:\infty }^{\pi }\left(s_0\right)(\lambda ao{s}_{1:\infty }.U^{\prime }(a{o}_{1:\infty }\left)\right)$

and, unpacking the limit, it turns into

${lim}_{n\to \infty }{K}_{:n}^{\pi }\left(s_0\right)(\lambda ao{s}_{1:n+1}.{inf}_{a{o}_{n+2:\infty }}U(a{o}_{1:n+1},a{o}_{n+2:\infty }\left)\right)$
$={lim}_{n\to \infty }{K}_{:n}^{\pi }\left(s_0\right)(\lambda ao{s}_{1:n+1}.{inf}_{a{o}_{n+2:\infty }}{U}^{\prime }(a{o}_{1:n+1},a{o}_{n+2:\infty }\left)\right)$

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

${limsup}_{n\to \infty }|K_{:n}^{\pi }\left(s_0\right)(\lambda ao{s}_{1:n+1}.{inf}_{a{o}_{n+2:\infty }}U(a{o}_{1:n+1},a{o}_{n+2:\infty }\left)\right)$
$-K_{:n}^{\pi }\left(s_0\right)(\lambda ao{s}_{1:n+1}.{inf}_{a{o}_{n+2:\infty }}{U}^{\prime }(a{o}_{1:n+1},a{o}_{n+2:\infty }\left)\right)|=0$

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

${limsup}_{n\to \infty }|K_{:n}^{\pi }\left(s_0\right)(\lambda ao{s}_{1:n+1}.{inf}_{a{o}_{n+2:\infty }}U(a{o}_{1:n+1},a{o}_{n+2:\infty }\left)\right)$
$-K_{:n}^{\pi }\left(s_0\right)(\lambda ao{s}_{1:n+1}.{inf}_{a{o}_{n+2:\infty }}{U}^{\prime }(a{o}_{1:n+1},a{o}_{n+2:\infty }\left)\right)|$

of

$\le {limsup}_{n\to \infty }(1\cdot {sup}_{ao{s}_{1:n+1}\sim \pi }|{inf}_{a{o}_{n+2:\infty }}U(a{o}_{1:n+1},a{o}_{n+2:\infty })$
$-{inf}_{a{o}_{n+2:\infty }}{U}^{\prime }(a{o}_{1:n+1},a{o}_{n+2:\infty })|+0\cdot d(U,U^{\prime }))$

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}_{ao{s}_{1:n+1}\sim \pi }|{inf}_{a{o}_{n+2:\infty }}U(a{o}_{1:n+1},a{o}_{n+2:\infty })-{inf}_{a{o}_{n+2:\infty }}{U}^{\prime }(a{o}_{1:n+1},a{o}_{n+2:\infty })|$

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

$\le {limsup}_{n\to \infty }{sup}_{ao{s}_{1:n+1}\sim \pi }\left(|{inf}_{a{o}_{n+2:\infty }}U\right(a{o}_{1:n+1},a{o}_{n+2:\infty })-U(a{o}_{1:n+1},a{o}_{n+2:\infty }^{\sim \pi })|$
$+|U(a{o}_{1:n+1},a{o}_{n+2:\infty }^{\sim \pi })-U^{\prime }(a{o}_{1:n+1},a{o}_{n+2:\infty }^{\sim \pi })|$
$+|U^{\prime }(a{o}_{1:n+1},a{o}_{n+2:\infty }^{\sim \pi })-{inf}_{a{o}_{n+2:\infty }}{U}^{\prime }(a{o}_{1:n+1},a{o}_{n+2:\infty })|)$

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

$={limsup}_{n\to \infty }{sup}_{ao{s}_{1:n+1}\sim \pi }\left(|{inf}_{a{o}_{n+2:\infty }}U\right(a{o}_{1:n+1},a{o}_{n+2:\infty })-U(a{o}_{1:n+1},a{o}_{n+2:\infty }^{\sim \pi })|$
$+|U^{\prime }(a{o}_{1:n+1},a{o}_{n+2:\infty }^{\sim \pi })-{inf}_{a{o}_{n+2:\infty }}{U}^{\prime }(a{o}_{1:n+1},a{o}_{n+2:\infty })|)$

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

$\le {limsup}_{n\to \infty }\left({sup}_{ao{s}_{1:n+1}\sim \pi }|{inf}_{a{o}_{n+2:\infty }}U\right(a{o}_{1:n+1},a{o}_{n+2:\infty })-U(a{o}_{1:n+1},a{o}_{n+2:\infty }^{\sim \pi }\left)|\right)$
$+{limsup}_{n\to \infty }\left({sup}_{ao{s}_{1:n+1}\sim \pi }|U^{\prime }\right(a{o}_{1:n+1},a{o}_{n+2:\infty }^{\sim \pi })-{inf}_{a{o}_{n+2:\infty }}{U}^{\prime }(a{o}_{1:n+1},a{o}_{n+2:\infty }\left)|\right)$

Since this quantity is an upper bound on the 

${limsup}_{n\to \infty }|K_{:n}^{\pi }\left(s_0\right)(\lambda ao{s}_{1:n+1}.{inf}_{a{o}_{n+2:\infty }}U(a{o}_{1:n+1},a{o}_{n+2:\infty }\left)\right)$
$-K_{:n}^{\pi }\left(s_0\right)(\lambda ao{s}_{1:n+1}.{inf}_{a{o}_{n+2:\infty }}{U}^{\prime }(a{o}_{1:n+1},a{o}_{n+2:\infty }\left)\right)|$

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^{\prime }$ are defined over $(A\times O{)}^{\omega }$, a compact space, they must both be uniformly continuous. You can take any $ϵ$, and find some $\delta$ where two histories that only differ by $\delta$ are assigned values $ϵ$ or less apart. And for any $\delta$, there's some n where any two histories that agree on the first n steps only differ by $\delta$. So, in the limit, both of these terms become 0, and our result that

$K_{:\infty }^{\pi }\left(s_0\right)(\lambda ao{s}_{1:\infty }.U(a{o}_{1:\infty }\left)\right)=K_{:\infty }^{\pi }\left(s_0\right)(\lambda ao{s}_{1:\infty }.U^{\prime }(a{o}_{1:\infty }\left)\right)$

for any $s_0$ and $U,U^{\prime }$ which agree on all histories compatible with $\pi$ follows since we hit our proof target. 

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

$|\Theta \left(\pi \right)\left(U\right)-\Theta \left(\pi \right)\left(U^{\prime }\right)|=|p{r}_{(A\times O{)}^{\omega }\ast }(\psi ⋉K_{:\infty }^{\pi })\left(U\right)-p{r}_{(A\times O{)}^{\omega }\ast }(\psi ⋉K_{:\infty }^{\pi })\left(U^{\prime }\right)|$

$=|\psi (\lambda s_0.K_{:\infty }^{\pi }(s_0\left)\right(\lambda ao{s}_{1:\infty }.U\left(a{o}_{1:\infty }\right)\left)\right)-\psi (\lambda s_0.K_{:\infty }^{\pi }(s_0\left)\right(\lambda ao{s}_{1:\infty }.U^{\prime }\left(a{o}_{1:\infty }\right)\left)\right)|$

And then, for all $s_0$,

$K_{:\infty }^{\pi }\left(s_0\right)(\lambda ao{s}_{1:\infty }.U(a{o}_{1:\infty }\left)\right)=K_{:\infty }^{\pi }\left(s_0\right)(\lambda ao{s}_{1:\infty }.U^{\prime }(a{o}_{1:\infty }\left)\right)$

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

$|\Theta \left(\pi \right)\left(U\right)-\Theta \left(\pi \right)\left(U^{\prime }\right)|=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 $\pi$ and ${\pi }^{\prime }$

$|\Theta \left(\pi \right)\left(1\right)-\Theta \left({\pi }^{\prime }\right)\left(1\right)|=|p{r}_{(A\times O{)}^{\omega }\ast }(\psi ⋉K_{:\infty }^{\pi })\left(1\right)-p{r}_{(A\times O{)}^{\omega }\ast }(\psi ⋉K_{:\infty }^{{\pi }^{\prime }})\left(1\right)|$

$=|\psi (\lambda s_0.K_{:\infty }^{\pi }(s_0\left)\right(1\left)\right)-\psi (\lambda s_0.K_{:\infty }^{{\pi }^{\prime }}(s_0\left)\right(1\left)\right)|$

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

$=|\psi \left(1\right)-\psi \left(1\right)|=0$

And we're done, and in fact get the stronger result that $\Theta \left(\pi \right)\left(1\right)=1$ regardless of $\pi$ because $\psi \left(1\right)=1$ because we assumed $\psi$ was an infradistribution. For the $R$ type signature, fixing any $\pi$ and ${\pi }^{\prime }$, we have

$|\Theta \left(\pi \right)\left(\infty \right)-\Theta \left({\pi }^{\prime }\right)\left(\infty \right)|=|p{r}_{(A\times O{)}^{\omega }\ast }(\psi ⋉K_{:\infty }^{\pi })\left(\infty \right)-p{r}_{(A\times O{)}^{\omega }\ast }(\psi ⋉K_{:\infty }^{{\pi }^{\prime }})\left(\infty \right)|$

$=|\psi (\lambda s_0.K_{:\infty }^{\pi }(s_0\left)\right(\infty \left)\right)-\psi (\lambda s_0.K_{:\infty }^{{\pi }^{\prime }}(s_0\left)\right(\infty \left)\right)|$

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

$=|\psi \left(\infty \right)-\psi \left(\infty \right)|=0$

Importantly, this does not mean that $\Theta \left(\pi \right)\left(\infty \right)$ must be $\infty$.

T4.2.5 Now for the very last condition, checking that $\Theta$ 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 {\pi }^{\prime }}^1\left(\Theta \right(\pi \left)\right)\left(U\right)\ge \Theta \left({\pi }^{\prime }\right)\left(U\right)$

We can unpack $\Theta \left(\pi \right)$ and $\Theta \left({\pi }^{\prime }\right)$, to get the equivalent proof target of:

$u_{\sim {\pi }^{\prime }}^1\left(p{r}_{(A\times O{)}^{\omega }\ast }\right(\psi ⋉K_{:\infty }^{\pi }\left)\right)\left(U\right)\ge p{r}_{(A\times O{)}^{\omega }\ast }(\psi ⋉K_{:\infty }^{{\pi }^{\prime }})\left(U\right)$

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

$p{r}_{(A\times O{)}^{\omega }\ast }(\psi ⋉K_{:\infty }^{\pi })(\lambda a{o}_{:\infty }.{\text{1}}_{a{o}_{1:\infty }\sim {\pi }^{\prime }}U(a{o}_{1:\infty })+{\text{1}}_{a{o}_{1:\infty }\nsim {\pi }^{\prime }})$
$\ge p{r}_{(A\times O{)}^{\omega }\ast }(\psi ⋉K_{:\infty }^{{\pi }^{\prime }})(\lambda a{o}_{1:\infty }.U(a{o}_{1:\infty }\left)\right)$

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

$(\psi ⋉K_{:\infty }^{\pi })(\lambda s_0,ao{s}_{1:\infty }.{\text{1}}_{a{o}_{1:\infty }\sim {\pi }^{\prime }}U(a{o}_{1:\infty })+{\text{1}}_{a{o}_{1:\infty }\nsim {\pi }^{\prime }})\ge (\psi ⋉K_{:\infty }^{{\pi }^{\prime }})(\lambda s_0,ao{s}_{1:\infty }.U(a{o}_{1:\infty }\left)\right)$

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

$\psi (\lambda s_0.K_{:\infty }^{\pi }(s_0\left)\right(\lambda ao{s}_{:\infty }.{\text{1}}_{a{o}_{1:\infty }\sim {\pi }^{\prime }}U\left(a{o}_{1:\infty }\right)+{\text{1}}_{a{o}_{1:\infty }\nsim {\pi }^{\prime }}\left)\right)\ge \psi (\lambda s_0.K_{:\infty }^{{\pi }^{\prime }}(s_0\left)\right(\lambda ao{s}_{1:\infty }.U\left(a{o}_{1:\infty }\right)\left)\right)$

By monotonicity for $\psi$, we'd be able to prove this if, for any $s_0$ initial state, we had

$K_{:\infty }^{\pi }\left(s_0\right)(\lambda ao{s}_{1:\infty }.{\text{1}}_{a{o}_{1:\infty }\sim {\pi }^{\prime }}U(a{o}_{1:\infty })+{\text{1}}_{a{o}_{1:\infty }\nsim {\pi }^{\prime }})\ge K_{:\infty }^{{\pi }^{\prime }}\left(s_0\right)(\lambda ao{s}_{1:\infty }.U(a{o}_{1:\infty }\left)\right)$

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}^{\pi }\left(s_0\right)(\lambda ao{s}_{1:n+1}.{inf}_{a{o}_{n+2:\infty }}({\text{1}}_{a{o}_{1:n+1},a{o}_{n+2:\infty }\sim {\pi }^{\prime }}U(a{o}_{1:n+1},a{o}_{n+2:\infty })+{\text{1}}_{a{o}_{1:n+1},a{o}_{n+2:\infty }\nsim {\pi }^{\prime }}\left)\right)$
$\ge {lim}_{n\to \infty }{K}_{:n}^{{\pi }^{\prime }}\left(s_0\right)(\lambda ao{s}_{1:n+1}.{inf}_{a{o}_{n+2:\infty }}U(a{o}_{1:n+1},a{o}_{n+2:\infty }\left)\right)$

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}^{\pi }\left(s_0\right)(\lambda ao{s}_{1:n+1}.{inf}_{a{o}_{n+2:\infty }}({\text{1}}_{a{o}_{1:n+1},a{o}_{n+2:\infty }\sim {\pi }^{\prime }}U(a{o}_{1:n+1},a{o}_{n+2:\infty })+{\text{1}}_{a{o}_{1:n+1},a{o}_{n+2:\infty }\nsim {\pi }^{\prime }}\left)\right)$
$\ge K_{:n}^{{\pi }^{\prime }}\left(s_0\right)(\lambda ao{s}_{1:n+1}.{inf}_{a{o}_{n+2:\infty }}U(a{o}_{1:n+1},a{o}_{n+2:\infty }\left)\right)$

We can observe something interesting here for the update. if $a{o}_{1:n+1}$ is compatible with ${\pi }^{\prime }$, then the inf can be modeled as always picking some continuation compatible with ${\pi }^{\prime }$, 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 ${\pi }^{\prime }$, then it doesn't matter the extension, any extension will always be incompatible with ${\pi }^{\prime }$, and return 1 (or infinity). So, this can be rephrased as

$K_{:n}^{\pi }\left(s_0\right)(\lambda ao{s}_{1:n+1}.{\text{1}}_{a{o}_{1:n+1}\sim {\pi }^{\prime }}{inf}_{a{o}_{n+2:\infty }}U(a{o}_{1:n+1},a{o}_{n+2:\infty })+{\text{1}}_{a{o}_{1:n+1}\nsim {\pi }^{\prime }})$
$\ge K_{:n}^{{\pi }^{\prime }}\left(s_0\right)(\lambda ao{s}_{1:n+1}.{inf}_{a{o}_{n+2:\infty }}U(a{o}_{1:n+1},a{o}_{n+2:\infty }\left)\right)$

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

$u_{\sim {\pi }^{\prime }}^1\left(K_{:n}^{\pi }\right(s_0\left)\right)(\lambda ao{s}_{1:n+1}.{inf}_{a{o}_{n+2:\infty }}U(a{o}_{1:n+1},a{o}_{n+2:\infty }\left)\right)$
$\ge K_{:n}^{{\pi }^{\prime }}\left(s_0\right)(\lambda ao{s}_{1:n+1}.{inf}_{a{o}_{n+2:\infty }}U(a{o}_{1:n+1},a{o}_{n+2:\infty }\left)\right)$

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,{\pi }^{\prime },\pi ,s_0$ as before.

$u_{\sim {\pi }^{\prime }}^1\left(K_{:n}^{\pi }\right(s_0\left)\right)\left(f_{n+1}\right)\ge K_{:n}^{{\pi }^{\prime }}\left(s_0\right)\left(f_{n+1}\right)$

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 {\pi }^{\prime }}^1\left(K_{:0}^{\pi }\right(s_0\left)\right)\left(f_1\right)\ge K_{:0}^{{\pi }^{\prime }}\left(s_0\right)\left(f_1\right)$

We reexpress the update to get a proof target of

$K_{:0}^{\pi }\left(s_0\right)(\lambda a,o,s.{\text{1}}_{a,o\sim {\pi }^{\prime }}{f}_1(a,o,s)+{\text{1}}_{a,o\nsim {\pi }^{\prime }})\ge K_{:0}^{{\pi }^{\prime }}\left(s_0\right)(\lambda a,o,s.f_1(a,o,s\left)\right)$

Now, the only way for $a,o$ to be incompatible with ${\pi }^{\prime }$ is if $a\ne {\pi }^{\prime }\left(\right)$. Doing that reexpression, we get

$K_{:0}^{\pi }\left(s_0\right)(\lambda a,o,s.{\text{1}}_{a={\pi }^{\prime }\left(\right)}{f}_1(a,o,s)+{\text{1}}_{a\ne {\pi }^{\prime }\left(\right)})\ge K_{:0}^{{\pi }^{\prime }}\left(s_0\right)(\lambda a,o,s.f_1(a,o,s\left)\right)$

We recall that for the iterated semidirect product, the $:0$ thing is just $K_0^{\pi }$, and $K_0^{\pi }\left(s_0\right)={\delta }_{\pi \left(\right)}⋉(\lambda a.K(s_0,a\left)\right)$. Making these substitutions, we get an equivalent proof target of

$({\delta }_{\pi \left(\right)}⋉(\lambda a.K(s_0,a)\left)\right)(\lambda a,o,s.{\text{1}}_{a={\pi }^{\prime }\left(\right)}{f}_1(a,o,s)+{\text{1}}_{a\ne {\pi }^{\prime }\left(\right)})$
$\ge ({\delta }_{{\pi }^{\prime }\left(\right)}⋉(\lambda a.K(s_0,a)\left)\right)(\lambda a,o,s.f_1(a,o,s\left)\right)$

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

$K(s_0,\pi (\left)\right)(\lambda o,s.{\text{1}}_{\pi \left(\right)={\pi }^{\prime }\left(\right)}{f}_1(\pi \left(\right),o,s)+{\text{1}}_{\pi \left(\right)\ne {\pi }^{\prime }\left(\right)})\ge K(s_0,{\pi }^{\prime }(\left)\right)(\lambda o,s.f_1({\pi }^{\prime }\left(\right),o,s\left)\right)$

We have two possible cases. In case 1, $\pi \left(\right)={\pi }^{\prime }\left(\right)$, and then our proof target turns into

$K(s_0,{\pi }^{\prime }(\left)\right)(\lambda o,s.f_1({\pi }^{\prime }\left(\right),o,s\left)\right)\ge K(s_0,{\pi }^{\prime }(\left)\right)(\lambda o,s.f_1({\pi }^{\prime }\left(\right),o,s\left)\right)$

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

$K(s_0,\pi (\left)\right)\left(1\right)\ge K(s_0,{\pi }^{\prime }(\left)\right)(\lambda o,s.f_1({\pi }^{\prime }\left(\right),o,s\left)\right)$

Which is true because

$K(s_0,\pi (\left)\right)\left(1\right)=1\ge K(s_0,{\pi }^{\prime }(\left)\right)(\lambda o,s.f_1({\pi }^{\prime }\left(\right),o,s\left)\right)$

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

$K(s_0,\pi (\left)\right)\left(\infty \right)=\infty \ge K(s_0,{\pi }^{\prime }(\left)\right)(\lambda o,s.f_1({\pi }^{\prime }\left(\right),o,s\left)\right)$

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 {\pi }^{\prime }}^1\left(K_{:n+1}^{\pi }\right(s_0\left)\right)\left(f_{n+2}\right)\ge K_{:n+1}^{{\pi }^{\prime }}\left(s_0\right)\left(f_{n+2}\right)$

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

$u_{\sim {\pi }^{\prime }}^1\left(K_{:n}^{\pi }\right(s_0\left)\right)\left(f_{n+1}\right)\ge K_{:n}^{{\pi }^{\prime }}\left(s_0\right)\left(f_{n+1}\right)$

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 {\pi }^{\prime }}^1\left(K_{:n+1}^{\pi }\right(s_0\left)\right)\left(f_{n+2}\right)\ge K_{:n+1}^{{\pi }^{\prime }}\left(s_0\right)\left(f_{n+2}\right)$

We reexpress the update, to get the equivalent statement

$K_{:n+1}^{\pi }\left(s_0\right)(\lambda ao{s}_{1:n+2}.{\text{1}}_{a{o}_{1:n+2}\sim {\pi }^{\prime }}{f}_{n+2}(ao{s}_{1:n+2})+{\text{1}}_{a{o}_{1:n+2}\nsim {\pi }^{\prime }})$
$\ge K_{:n+1}^{{\pi }^{\prime }}\left(s_0\right)(\lambda ao{s}_{1:n+2}.f_{n+2}(ao{s}_{1:n+2}\left)\right)$

We unpack the definition of $K_{:n+1}^{\pi }\left(s_0\right)$ to get

$K_{:n}^{\pi }\left(s_0\right)(\lambda ao{s}_{1:n+1}.K_{n+1}^{\pi }(s_0,ao{s}_{1:n+1})$
$(\lambda a,o,s.{\text{1}}_{a{o}_{1:n+1},a,o\sim {\pi }^{\prime }}{f}_{n+2}(ao{s}_{1:n+1},a,o,s)+{\text{1}}_{a{o}_{1:n+1},a,o\nsim {\pi }^{\prime }}))$
$\ge K_{:n}^{{\pi }^{\prime }}\left(s_0\right)(\lambda ao{s}_{1:n+1}.K_{n+1}^{{\pi }^{\prime }}(s_0,ao{s}_{:n+1}\left)\right(\lambda a,o,s.f_{n+2}(ao{s}_{1:n+1},a,o,s)\left)\right)$

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

$K_{:n}^{\pi }\left(s_0\right)(\lambda ao{s}_{1:n+1}.({\delta }_{\pi \left(a{o}_{1:n+1}\right)}⋉(\lambda a.K(s_{n+1},a\left)\right))$
$(\lambda a,o,s.{\text{1}}_{a{o}_{1:n+1},a,o\sim {\pi }^{\prime }}{f}_{n+2}(ao{s}_{1:n+1},a,o,s)+{\text{1}}_{a{o}_{1:n+1},a,o\nsim {\pi }^{\prime }}))$
$\ge K_{:n}^{{\pi }^{\prime }}\left(s_0\right)(\lambda ao{s}_{1:n+1}.({\delta }_{{\pi }^{\prime }\left(a{o}_{1:n+1}\right)}⋉(\lambda a.K(s_{n+1},a\left)\right)\left)\right(\lambda a,o,s.f_{n+2}(ao{s}_{1:n+1},a,o,s)\left)\right)$

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

$K_{:n}^{\pi }\left(s_0\right)(\lambda ao{s}_{1:n+1}.K(s_{n+1},\pi \left(a{o}_{1:n+1}\right))$
$(\lambda o,s.{\text{1}}_{a{o}_{1:n+1},\pi \left(a{o}_{1:n+1}\right),o\sim {\pi }^{\prime }}{f}_{n+2}(ao{s}_{1:n+1},\pi \left(a{o}_{1:n+1}\right),o,s)+{\text{1}}_{a{o}_{1:n+1},\pi \left(a{o}_{1:n+1}\right),o\nsim {\pi }^{\prime }}))$
$\ge K_{:n}^{{\pi }^{\prime }}\left(s_0\right)(\lambda ao{s}_{1:n+1}.K(s_{n+1},{\pi }^{\prime }\left(a{o}_{1:n+1}\right)\left)\right(\lambda o,s.f_{n+2}(ao{s}_{1:n+1},{\pi }^{\prime }(a{o}_{1:n+1}),o,s)\left)\right)$

Now, looking at that gigantic first term... if $a{o}_{1:n+1}$ is incompatible with ${\pi }^{\prime }$, 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 {\pi }^{\prime }$, then we're back in the usual business except we don't need to worry about incompatibilities of the history with ${\pi }^{\prime }$ within $a{o}_{1:n+1}$, we only need to worry about those incompatiblities for the final action, $\pi \left(a{o}_{1:n+1}\right)$. So, we can rewrite that first term with indicator functions.

$K_{:n}^{\pi }\left(s_0\right)(\lambda ao{s}_{1:n+1}.{\text{1}}_{a{o}_{1:n+1}\sim {\pi }^{\prime }}(K(s_{n+1},\pi (a{o}_{:n+1}\left)\right)$
$(\lambda o,s.{\text{1}}_{\pi \left(a{o}_{:n+1}\right)={\pi }^{\prime }\left(a{o}_{:n+1}\right)}{f}_{n+2}(ao{s}_{1:n+1},\pi \left(a{o}_{1:n+1}\right),o,s)+{\text{1}}_{\pi \left(a{o}_{1:n+1}\right)\ne {\pi }^{\prime }\left(a{o}_{1:n+1}\right)}))$
$+{\text{1}}_{a{o}_{1:n+1}\nsim {\pi }^{\prime }})$
$\ge K_{:n}^{{\pi }^{\prime }}\left(s_0\right)(\lambda ao{s}_{1:n+1}.K(s_{n+1},{\pi }^{\prime }\left(a{o}_{1:n+1}\right)\left)\right(\lambda o,s.f_{n+2}(ao{s}_{1:n+1},{\pi }^{\prime }(a{o}_{:n+1}),o,s)\left)\right)$

And then rewrite this as just an update on $K_{:n}^{\pi }\left(s_0\right)$, getting the equivalent proof goal

$u_{\sim {\pi }^{\prime }}^1\left(K_{:n}^{\pi }\right(s_0\left)\right)(\lambda ao{s}_{1:n+1}.K(s_{n+1},\pi \left(a{o}_{:n+1}\right))$
$(\lambda o,s.{\text{1}}_{\pi \left(a{o}_{:n+1}\right)={\pi }^{\prime }\left(a{o}_{:n+1}\right)}{f}_{n+2}(ao{s}_{1:n+1},\pi \left(a{o}_{1:n+1}\right),o,s)+{\text{1}}_{\pi \left(a{o}_{1:n+1}\right)\ne {\pi }^{\prime }\left(a{o}_{1:n+1}\right)}))$
$\ge K_{:n}^{{\pi }^{\prime }}\left(s_0\right)(\lambda ao{s}_{1:n+1}.K(s_{n+1},{\pi }^{\prime }\left(a{o}_{1:n+1}\right)\left)\right(\lambda o,s.f_{n+2}(ao{s}_{1:n+1},{\pi }^{\prime }(a{o}_{:n+1}),o,s)\left)\right)$

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

$\lambda ao{s}_{1:n+1}.K(s_{n+1},\pi (a{o}_{:n+1}\left)\right)$
$(\lambda o,s.{\text{1}}_{\pi \left(a{o}_{:n+1}\right)={\pi }^{\prime }\left(a{o}_{:n+1}\right)}{f}_{n+2}(ao{s}_{1:n+1},\pi \left(a{o}_{1:n+1}\right),o,s)+{\text{1}}_{\pi \left(a{o}_{1:n+1}\right)\ne {\pi }^{\prime }\left(a{o}_{1:n+1}\right)})$

To derive, from our induction assumption, that

$u_{\sim {\pi }^{\prime }}^1\left(K_{:n}^{\pi }\right(s_0\left)\right)(\lambda ao{s}_{1:n+1}.K(s_{n+1},\pi \left(a{o}_{:n+1}\right))$
$(\lambda o,s.{\text{1}}_{\pi \left(a{o}_{:n+1}\right)={\pi }^{\prime }\left(a{o}_{:n+1}\right)}{f}_{n+2}(ao{s}_{1:n+1},\pi \left(a{o}_{1:n+1}\right),o,s)+{\text{1}}_{\pi \left(a{o}_{1:n+1}\right)\ne {\pi }^{\prime }\left(a{o}_{1:n+1}\right)}))$

$=u_{\sim {\pi }^{\prime }}^1\left(K_{:n}^{\pi }\right(s_0\left)\right)\left(f_{n+1}\right)\ge K_{:n}^{{\pi }^{\prime }}\left(s_0\right)\left(f_{n+1}\right)$

$=K_{:n}^{{\pi }^{\prime }}\left(s_0\right)(\lambda ao{s}_{1:n+1}.K(s_{n+1},\pi \left(a{o}_{:n+1}\right))$
$(\lambda o,s.{\text{1}}_{\pi \left(a{o}_{:n+1}\right)={\pi }^{\prime }\left(a{o}_{:n+1}\right)}{f}_{n+2}(ao{s}_{1:n+1},\pi \left(a{o}_{1:n+1}\right),o,s)+{\text{1}}_{\pi \left(a{o}_{1:n+1}\right)\ne {\pi }^{\prime }\left(a{o}_{1:n+1}\right)}))$

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

$K_{:n}^{{\pi }^{\prime }}\left(s_0\right)(\lambda ao{s}_{1:n+1}.K(s_{n+1},{\pi }^{\prime }\left(a{o}_{1:n+1}\right)\left)\right(\lambda o,s.f_{n+2}(ao{s}_{1:n+1},{\pi }^{\prime }(a{o}_{:n+1}),o,s)\left)\right)$

,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}^{{\pi }^{\prime }}\left(s_0\right)(\lambda ao{s}_{1:n+1}.K(s_{n+1},\pi \left(a{o}_{:n+1}\right))$
$(\lambda o,s.{\text{1}}_{\pi \left(a{o}_{:n+1}\right)={\pi }^{\prime }\left(a{o}_{:n+1}\right)}{f}_{n+2}(ao{s}_{1:n+1},\pi \left(a{o}_{1:n+1}\right),o,s)+{\text{1}}_{\pi \left(a{o}_{1:n+1}\right)\ne {\pi }^{\prime }\left(a{o}_{1:n+1}\right)}))$
$\ge K_{:n}^{{\pi }^{\prime }}\left(s_0\right)(\lambda ao{s}_{1:n+1}.K(s_{n+1},{\pi }^{\prime }\left(a{o}_{1:n+1}\right)\left)\right(\lambda o,s.f_{n+2}(ao{s}_{1:n+1},{\pi }^{\prime }(a{o}_{:n+1}),o,s)\left)\right)$

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

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

$K_{:n}^{{\pi }^{\prime }}\left(s_0\right)(\lambda ao{s}_{1:n+1}.$
${\text{1}}_{\pi \left(a{o}_{1:n+1}\right)={\pi }^{\prime }\left(a{o}_{1:n+1}\right)}K(s_{n+1},{\pi }^{\prime }(a{o}_{1:n+1}\left)\right)(\lambda o,s.f_{n+2}(ao{s}_{1:n+1},{\pi }^{\prime }\left(a{o}_{1:n+1}\right),o,s\left)\right)$
$+{\text{1}}_{\pi \left(a{o}_{1:n+1}\right)\ne {\pi }^{\prime }\left(a{o}_{1:n+1}\right)})$
$\ge K_{:n}^{{\pi }^{\prime }}\left(s_0\right)(\lambda ao{s}_{1:n+1}.K(s_{n+1},{\pi }^{\prime }\left(a{o}_{1:n+1}\right)\left)\right(\lambda o,s.f_{n+2}(ao{s}_{1:n+1},{\pi }^{\prime }(a{o}_{1:n+1}),o,s)\left)\right)$

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

${\text{1}}_{\pi \left(a{o}_{1:n+1}\right)={\pi }^{\prime }\left(a{o}_{1:n+1}\right)}K(s_{n+1},{\pi }^{\prime }(a{o}_{1:n+1}\left)\right)(\lambda o,s.f_{n+2}(ao{s}_{1:n+1},{\pi }^{\prime }\left(a{o}_{1:n+1}\right),o,s\left)\right)$
$+{\text{1}}_{\pi \left(a{o}_{1:n+1}\right)\ne {\pi }^{\prime }\left(a{o}_{1:n+1}\right)}$
$\ge K(s_{n+1},{\pi }^{\prime }(a{o}_{1:n+1}\left)\right)(\lambda o,s.f_{n+2}(ao{s}_{1:n+1},{\pi }^{\prime }\left(a{o}_{1:n+1}\right),o,s\left)\right)$

In the first subcase, where $\pi \left(a{o}_{1:n+1}\right)\ne {\pi }^{\prime }\left(a{o}_{1:n+1}\right)$, because of 1-normalization (or constants moving up), our goal would be that

$1\ge K(s_{n+1},{\pi }^{\prime }(a{o}_{1:n+1}\left)\right)(\lambda o,s.f_{n+2}(ao{s}_{1:n+1},{\pi }^{\prime }\left(a{o}_{1:n+1}\right),o,s\left)\right)$

(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 $\pi \left(a{o}_{1:n+1}\right)={\pi }^{\prime }\left(a{o}_{1:n+1}\right)$, our proof goal would turn into:

$K(s_{n+1},{\pi }^{\prime }(a{o}_{1:n+1}\left)\right)(\lambda o,s.f_{n+2}(ao{s}_{1:n+1},{\pi }^{\prime }\left(a{o}_{1:n+1}\right),o,s\left)\right)$
$\ge K(s_{n+1},{\pi }^{\prime }(a{o}_{1:n+1}\left)\right)(\lambda o,s.f_{n+2}(ao{s}_{1:n+1},{\pi }^{\prime }\left(a{o}_{1:n+1}\right),o,s\left)\right)$

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!

0 comments

Comments sorted by top scores.