Proofs Theorem 5

[Diffractor]

Theorem 5: Causal Commutative Square: The following diagram commutes for any choice of causal $\Theta$. Any choice of infradistribution $E\in \square E$ where $E={\bigwedge }_{\pi }(\pi \cdot {)}^{\ast }((\pi \cdot {)}_{\ast }(E\left)\right)$ also makes this diagram commute.

Again, like usual, this proof consists of doing preliminary work (section 0) where we clarify some stuff and find 4 conditions for the 4 corners that correspond to “maximal representative of a causal belief function”. Section 1.1-8 is showing that these properties are preserved under all eight morphisms, where as usual, the complicated part of translating between a belief function and infradistribution is shoved in the first two sections. Sections 2.1-8 are then showing the 8 identities needed to establish 4 isomorphisms assuming the relevant properties, and then section 3 is going in two directions from one corner to another and showing equality to rule out nontrivial automorphisms.

T5.0 First, preliminaries. We use suprema over: probability distributions $\zeta$ on the space of policies, and utility functions $U_{\pi }$ we associate with each policy $\pi$, which fulfill the following constraint for some function $f$.

$\forall e:E_{\pi \sim \zeta }\left[U_{\pi }\right(\pi \cdot e\left)\right]\le f\left(e\right)$

To avoid writing all this out each time, we observe that for the purposes of the proof, all that varies in this format is the function $f:E\to [0,1]$ that we’re using as an upper-bound, we always select probability distributions over policies and utility functions linked with the same policy, and impose upper bounds of that “for all copolicies” form on a mix of the relevant utility functions interacting with the copolicy. So we’ll suppress all this in the notation and just say

${sup}_{\zeta ,U_{\pi },f}$

as our abbreviation, with $\bullet$ for when we need a function to have an empty slot for copolicies. So something like $U({\pi }^{\prime }\cdot \bullet )$ would be “the function from copolicies to $[0,1]$ given by letting ${\pi }^{\prime }$ interact with the copolicy to get a history, and then applying $U$ to it”.

The defining property for the third-person static view is that $E$ is an infradistribution, and, for all functions $f:E\to [0,1]$, $E\left(f\right)={sup}_{\zeta ,U_{\pi },f}{E}_{\pi \sim \zeta }\left[E\right(\lambda e.U_{\pi }(\pi \cdot e)\left)\right]$

The property for the third-person dynamic view is that ${\psi }_T$ is an infradistribution, and ${\psi }_T\left(f\right)={sup}_{\zeta ,U_{\pi },f}{E}_{\pi \sim \zeta }\left[{\psi }_T\right(\lambda e.U_{\pi }(\pi \cdot e)\left)\right]$ and ${\to }_T\left(e\right)={\top }_A⋉(\lambda a.{\delta }_{e\left(a\right),e_{a,e\left(a\right)}})$

The property for the first-person static view is that $\Theta$ be a belief function, and that it fulfill causality, that $\Theta \left({\pi }^{\prime }\right)\left(U\right)={sup}_{\zeta ,U_{\pi },U({\pi }^{\prime }\cdot \bullet )}{E}_{\pi \sim \zeta }\left[\Theta \right(\pi \left)\right(U_{\pi }\left)\right]$

The property for the first-person dynamic view is that ${\psi }_F$ is an infradistribution, and ${\psi }_F\left(f\right)={sup}_{\zeta ,U_{\pi },f}{E}_{\pi \sim \zeta }\left[{\psi }_F\right(\lambda e.U_{\pi }(\pi \cdot e)\left)\right]$ and ${\to }_F(e,a)={\delta }_{e\left(a\right),e_{a,e\left(a\right)}}$

Before showing that these properties are preserved under morphisms, it will be handy to have an equivalent rephrasing of causality for belief functions.

The causality condition is:

$\Theta \left({\pi }^{\prime }\right)\left(U\right)={sup}_{\zeta ,U_{\pi },U({\pi }^{\prime }\cdot \bullet )}{E}_{\pi \sim \zeta }\left[\Theta \right(\pi \left)\right(U_{\pi }\left)\right]$

We can unconditionally derive the statement

$\Theta \left({\pi }^{\prime }\right)\left(U\right)\le {sup}_{\zeta ,U_{\pi },U({\pi }^{\prime }\cdot \bullet )}{E}_{\pi \sim \zeta }\left[\Theta \right(\pi \left)\right(U_{\pi }\left)\right]$

because, letting $\zeta$ be the dirac-delta distribution on ${\pi }^{\prime }$, and $U_{{\pi }^{\prime }}=U$, we trivially fulfill the necessary condition for the supremum, that $\forall e:E_{\zeta }\left[U_{\pi }\right(\pi \cdot e\left)\right]\le U({\pi }^{\prime }\cdot e)$

So, we get the fact

$\Theta \left({\pi }^{\prime }\right)\left(U\right)=E_{\pi \sim {\delta }_{{\pi }^{\prime }}}\left[\Theta \right(\pi \left)\right(U_{\pi }\left)\right]\le {sup}_{\zeta ,U_{\pi },U({\pi }^{\prime }\cdot \bullet )}{E}_{\pi \sim \zeta }\left[\Theta \right(\pi \left)\right(U_{\pi }\left)\right]$

With this knowledge, the causality condition holds iff

$\Theta \left({\pi }^{\prime }\right)\left(U\right)\ge {sup}_{\zeta ,U_{\pi },U({\pi }^{\prime }\cdot \bullet )}{E}_{\pi \sim \zeta }\left[\Theta \right(\pi \left)\right(U_{\pi }\left)\right]$

and this holds iff

$\forall \zeta \in \Delta \Pi ,U_{\pi }:(\forall e:E_{\pi \sim \zeta }[U_{\pi }(\pi \cdot e)]\le U({\pi }^{\prime }\cdot e\left)\right)\to E_{\pi \sim \zeta }\left[\Theta \right(\pi \left)\right(U_{\pi }\left)\right]\le \Theta \left({\pi }^{\prime }\right)\left(U\right)$

In the first direction, this happens because any particular choice of $\zeta$ and $U_{\pi }$ which fulfills the implication antecendent must have the expectation of $\Theta \left(\pi \right)\left(U_{\pi }\right)$ doing worse than the supremum of such expectation, which still loses to $\Theta \left({\pi }^{\prime }\right)\left(U\right)$.

In the other direction, this happens because the supremum only ranges over distributions on policies and choices of utility function that fulfills the implication antecedent, so the consequent always kicks in. Thus, even the largest possible expectation of $\Theta \left(\pi \right)\left(U_{\pi }\right)$ isn’t above $\Theta \left({\pi }^{\prime }\right)\left(U\right)$.

Thus, we will be taking

$\forall \zeta \in \Delta \Pi ,U_{\pi }:(\forall e:E_{\pi \sim \zeta }[U_{\pi }(\pi \cdot e)]\le U({\pi }^{\prime }\cdot e\left)\right)\to E_{\pi \sim \zeta }\left[\Theta \right(\pi \left)\right(U_{\pi }\left)\right]\le \Theta \left({\pi }^{\prime }\right)\left(U\right)$

as an alternative phrasing of causality for belief functions.

Time to show that these properties are preserved under the morphisms. As usual, the hard part is showing property preservation between first-person static and first-person dynamic.

T5.1.1 3-static to 1-static. Our translation is

$\Theta \left(\pi \right):=(\pi \cdot {)}_{\ast }(E)$

and we must check the five conditions of a belief function, as well as causality. So the proof splits into six parts for those six desired results. The five conditions for a belief function are a bounded Lipschitz constant, lower-semicontinuity, normalization, sensible supports, and agreement on max value. We’ll just be using that $E$ is an infradistribution, and not that it has any additional properties beyond that. The pushforward of an infradistribution is always an infradistribution, so we know that $\Theta \left(\pi \right)$ is always an infradistribution.

T5.1.1.1 For a bounded Lipschitz constant, we have

$|\Theta \left(\pi \right)\left(U\right)-\Theta \left(\pi \right)\left(U^{\prime }\right)|=|(\pi \cdot {)}_{\ast }(E\left)\right(U)-(\pi \cdot {)}_{\ast }\left(E\right)\left(U^{\prime }\right)|$

$=|E(\lambda e.U(\pi \cdot e\left)\right)-E(\lambda e.U^{\prime }(\pi \cdot e\left)\right)|$

and then, since $E$ has some Lipschitz constant ${\lambda }^{\odot }$, we then have

$\le {\lambda }^{\odot }{sup}_e|U(\pi \cdot e)-U^{\prime }(\pi \cdot e)|$

And, for any $\pi ,e$ pair, it induces a history, so this is upper-bounded by

$\le {\lambda }^{\odot }{sup}_h|U\left(h\right)-U^{\prime }\left(h\right)|={\lambda }^{\odot }d(U,U^{\prime })$

So a uniform Lipschitz constant upper bound is shown.

T5.1.1.2 For lower-semicontinuity, it’s actually easy to show for once. We get something even stronger. All causal belief functions aren’t just lower-semicontinuous in their first argument, they’re continuous. The proof is:

${lim}_{n\to \infty }\Theta \left({\pi }_n\right)\left(U\right)={lim}_{n\to \infty }({\pi }_n\cdot {)}_{\ast }(E\left)\right(U)={lim}_{n\to \infty }E(\lambda e.U({\pi }_n\cdot e))$

Now, the thing to realize here is that $\lambda e.U({\pi }_n\cdot e)$ uniformly converges to $\lambda e.U({\pi }_{\infty }\cdot e)$. Why does this happen? Well, once ${\pi }_n$ gets close enough to ${\pi }_{\infty }$, it will perfectly agree with ${\pi }_{\infty }$ about what to do in any situation for the first m steps. So, vs any copolicy at all, the histories ${\pi }_n\cdot e$ (for all sufficiently late n) and ${\pi }_{\infty }\cdot e$ will agree for the first m steps. And, since $U$ is continuous on $(A\times O{)}^{\omega }$ which is a compact space, it must be uniformly continuous. So for any $ϵ$ difference in output, there’s some m where knowing the first m steps of history lets you pin down the value of $U$ to within $ϵ$.

Then, we can just appeal to the finite Lipschitz constant of $E$ to conclude that, since we have uniform convergence of functions, we have

$=E(\lambda e.U({\pi }_{\infty }\cdot e\left)\right)$

which then packs back up in reverse as

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

That was very easy compared to our typical lower-semicontinuity proofs!

T5.1.1.3 For normalization, we have

${inf}_{\pi }\Theta \left(\pi \right)\left(1\right)={inf}_{\pi }(\pi \cdot {)}_{\ast }(E\left)\right(1)={inf}_{\pi }E(1)=1$

And the same goes for 0, because $E$ is an infradistribution.

T5.1.1.4 For sensible supports, assume $U,U^{\prime }$ agree on histories that can be produced by $\pi$. Then,

$|\Theta \left(\pi \right)\left(U\right)-\Theta \left(\pi \right)\left(U^{\prime }\right)|=|(\pi \cdot {)}_{\ast }(E\left)\right(U)-(\pi \cdot {)}_{\ast }\left(E\right)\left(U^{\prime }\right)|$

$=|E(\lambda e.U(\pi \cdot e\left)\right)-E(\lambda e.U^{\prime }(\pi \cdot e\left)\right)|$

But then wait, for any $e$, $\pi \cdot e$ makes a history that can be made by $\pi$, so then $U,U^{\prime }$ must agree on it. Those two inner functions are equal, and so attain equal value, and we have $=0$.

T5.1.1.5 For agreement on max value, you can just go

$\Theta \left(\pi \right)\left(1\right)=(\pi \cdot {)}_{\ast }(E\left)\right(1)=E(1)=({\pi }^{\prime }\cdot {)}_{\ast }\left(E\right)\left(1\right)=\Theta \left({\pi }^{\prime }\right)\left(1\right)$

and

$\Theta \left(\pi \right)\left(\infty \right)=(\pi \cdot {)}_{\ast }(E\left)\right(\infty )=E(\infty )=({\pi }^{\prime }\cdot {)}_{\ast }\left(E\right)\left(\infty \right)=\Theta \left({\pi }^{\prime }\right)\left(\infty \right)$

and you’re done.

T5.1.1.6 That just leaves checking causality. We’ll make a point to not assume any special conditions on $E$ at all in order to show this, because the

$E\left(f\right)={sup}_{\zeta ,U_{\pi },f}{E}_{\pi \sim \zeta }\left[E\right(\lambda e.U_{\pi }(\pi \cdot e)\left)\right]$

condition is actually saying that $E$ is the maximal infradistribution that corresponds to a causal belief function, but it’ll be useful later to know that any infradistribution on copolicies makes a causal belief function.

We’ll be showing our alternate characterization of causality, that

$\forall \zeta \in \Delta \Pi ,U_{\pi },U:(\forall e:E_{\pi \sim \zeta }[U_{\pi }(\pi \cdot e)]\le U({\pi }^{\prime }\cdot e\left)\right)\to E_{\pi \sim \zeta }\left[\Theta \right(\pi \left)\right(U_{\pi }\left)\right]\le \Theta \left({\pi }^{\prime }\right)\left(U\right)$

So, pick an arbitrary $\zeta$, family of $U_{\pi }$, utility function $U$, and policy ${\pi }^{\prime }$, and assume $\forall e:E_{\pi \sim \zeta }\left[U_{\pi }\right(\pi \cdot e\left)\right]\le U({\pi }^{\prime }\cdot e)$ Then, we can go:

$E_{\pi \sim \zeta }\left[\Theta \right(\pi \left)\right(U_{\pi }\left)\right]=E_{\pi \sim \zeta }\left[\right(\pi \cdot {)}_{\ast }\left(E\right)\left(U_{\pi }\right)]=E_{\pi \sim \zeta }[E(\lambda e.U_{\pi }(\pi \cdot e\left)\right)]$

and then, by applying concavity of infradistributions, we can move the expectation inside and the value goes up, and then we apply monotonicity via the precondition we assumed.

$\le E(\lambda e.E_{\pi \sim \zeta }[U_{\pi }(\pi \cdot e)\left]\right)\le E(\lambda e.U({\pi }^{\prime }\cdot e\left)\right)$

and then we just pack this back up.

$=({\pi }^{\prime }\cdot {)}_{\ast }(E\left)\right(U)=\Theta ({\pi }^{\prime }\left)\right(U)$

and we have the causality condition shown.

T5.1.2 1-static to 3-static. Our translation is:

$E:={\bigwedge }_{\pi }(\pi \cdot {)}^{\ast }(\Theta \left(\pi \right))$

The way this proof works is first, we unpack $E$ into a different form in preparation for what follows, that’s phase 1. Then there’s 6 more phases after that, where we show the five infradistribution conditions on $E$ and the causality condition. Some of these are hard to show so we’ll have to split them into more parts.

T5.1.2.1 We’ll unpack this first, in preparation for showing the infradistribution properties and causality property for $E$. We can go

$E\left(f\right)={\bigwedge }_{\pi }(\pi \cdot {)}^{\ast }(\Theta \left(\pi \right)\left)\right(f)$

and then express the intersection as a supremum over $\zeta \in \Delta \Pi$ and $f_{\pi }:E\to [0,1]$ such that $\forall e:E_{\pi \sim \zeta }\left[f_{\pi }\right(e\left)\right]\le f\left(e\right)$ because that’s just how intersections work. This is abbreviated as ${sup}_{\zeta ,f_{\pi },f}$.

$={sup}_{\zeta ,f_{\pi },f}{E}_{\pi \sim \zeta }\left[\right(\pi \cdot {)}^{\ast }\left(\Theta \right(\pi \left)\right)\left(f_{\pi }\right)]$

Then, for the pullback, we take the supremum over $U_{\pi }$ where $U_{\pi }(\pi \cdot e)\le f_{\pi }\left(e\right)$ for all $e$. We’ll write this as ${sup}_{U_{\pi },f_{\pi }}$.

This makes

$={sup}_{\zeta ,f_{\pi },f}{E}_{\pi \sim \zeta }\left[{sup}_{U_{\pi },f_{\pi }}\Theta \right(\pi \left)\right(U_{\pi }\left)\right]$

Now, these $U_{\pi }(\pi \cdot \bullet )$ always make an acceptable substitute for the $f_{\pi }$ functions early on, as they’re always lower than $f_{\pi }$ regardless of copolicy. Further, if you’re attempting to attain the supremum, you’ll never actually use your $f_{\pi }$, it will always be $U_{\pi }$ being plugged in. So, we can just wrap up all the maximization into one supremum, to make

$={sup}_{\zeta ,U_{\pi },f}{E}_{\pi \sim \zeta }\left[\Theta \right(\pi \left)\right(U_{\pi }\left)\right]$

We’ll be using this phrasing as a more explicit unpacking of $E\left(f\right)$.

Now, for the infradistribution conditions on $E$, and the causality condition, there’s a very important technicality going on. Intersection behaves much worse for the $[0,1]$ type signature. In the $R$ type signature, everything works out perfectly. However, in the $[0,1]$ type signature, we’ll be able to show all the needed properties for $E$ except having a finite Lipschitz constant. But, not all is lost, because to compensate for that, we’ll show that you can swap out $E$ (almost an infradistribution) for an actual infradistribution $E^{\prime }$ that induces the same belief function $\Theta$.

Like we said back in the post, it isn’t terribly important that we use the true maximal representative $E$, we just want some infradistribution in the same equivalence class.

T5.1.2.2 First up, monotonicity. Assume $f^{\prime }\ge f$. Then, using our rewrite of $E\left(f^{\prime }\right)$ and $E\left(f\right)$, we have

$E\left(f^{\prime }\right)={sup}_{\zeta ,U_{\pi },f^{\prime }}{E}_{\pi \sim \zeta }\left[\Theta \right(\pi \left)\right(U_{\pi }\left)\right]\ge {sup}_{\zeta ,U_{\pi },f}{E}_{\pi \sim \zeta }\left[\Theta \right(\pi \left)\right(U_{\pi }\left)\right]=E\left(f\right)$

and monotonicity is shown. This occurred because we’re taking the supremum over probability distributions and choices of utility function where the mix underperforms $f^{\prime }$ as an upper bound. Since $f$ is lower, we’re taking the supremum over fewer options.

T5.1.2.3 Now, concavity. We’ll work in reverse for this.

$pE\left(f\right)+(1-p)E\left(f^{\prime }\right)=p{sup}_{\zeta ,U_{{\pi }_1},f}{E}_{\pi \sim \zeta }\left[\Theta \right(\pi \left)\right(U_{{\pi }_1}\left)\right]+(1-p){sup}_{{\zeta }^{\prime },U_{{\pi }_2},f^{\prime }}{E}_{\pi \sim {\zeta }^{\prime }}\left[\Theta \right(\pi \left)\right(U_{{\pi }_2}\left)\right]$

Let’s regard the supremum as being attained (or coming arbitrarily close to being attained) by some particular choice of $\zeta ,{\zeta }^{\prime }$, and families $U_{{\pi }_1}$ and $U_{{\pi }_2}$(which are upper-bounded by $f,f^{\prime }$ respectively) to get

$=p{E}_{\pi \sim \zeta }\left[\Theta \right(\pi \left)\right(U_{{\pi }_1}\left)\right]+(1-p)E_{\pi \sim {\zeta }^{\prime }}\left[\Theta \right(\pi \left)\right(U_{{\pi }_2}\left)\right]$

We can rewrite this as an integral to get

$=p{\int }_{\Pi }(\lambda \pi .\Theta (\pi \left)\right(U_{{\pi }_1}\left)\right)d\zeta +(1-p){\int }_{\Pi }(\lambda \pi .\Theta (\pi \left)\right(U_{{\pi }_2}\left)\right)d{\zeta }^{\prime }$

and then move the $p$ and $(1-p)$ in to get integration w.r.t. a measure.

$={\int }_{\Pi }(\lambda \pi .\Theta (\pi \left)\right(U_{{\pi }_1}\left)\right)d\left(p\zeta \right)+{\int }_{\Pi }(\lambda \pi .\Theta (\pi \left)\right(U_{{\pi }_2}\left)\right)d\left(\right(1-p\left){\zeta }^{\prime }\right)$

And then, since $p\zeta$ and $(1-p){\zeta }^{\prime }$ are both absolutely continuous w.r.t. $p\zeta +(1-p){\zeta }^{\prime }$, we can rewrite both of these integrals w.r.t the Radon-Nikodym derivative, as

$={\int }_{\Pi }(\lambda \pi .\Theta (\pi \left)\right(U_{{\pi }_1})\cdot \frac{d\left(p\zeta \right)}{d(p\zeta +(1-p\left){\zeta }^{\prime }\right)}(\pi \left)\right)d(p\zeta +(1-p\left){\zeta }^{\prime }\right)$
$+{\int }_{\Pi }(\lambda \pi .\Theta (\pi \left)\right(U_{{\pi }_2})\cdot \frac{d\left(\right(1-p\left){\zeta }^{\prime }\right)}{d(p\zeta +(1-p\left){\zeta }^{\prime }\right)}(\pi \left)\right)d(p\zeta +(1-p\left){\zeta }^{\prime }\right)$

and pack these up into one integral as the probability distribution we’re integrating over is the same in both cases,

$={\int }_{\Pi }(\lambda \pi .\frac{d\left(p\zeta \right)}{d(p\zeta +(1-p\left){\zeta }^{\prime }\right)}(\pi )\cdot \Theta (\pi \left)\right(U_{{\pi }_1})+\frac{d\left(\right(1-p\left){\zeta }^{\prime }\right)}{d(p\zeta +(1-p\left){\zeta }^{\prime }\right)}(\pi )\cdot \Theta (\pi \left)\right(U_{{\pi }_2}\left)\right)$
$d(p\zeta +(1-p\left){\zeta }^{\prime }\right)$

And then, because

$\frac{d\left(p\zeta \right)}{d(p\zeta +(1-p\left){\zeta }^{\prime }\right)}\left(\pi \right)+\frac{d\left(\right(1-p\left){\zeta }^{\prime }\right)}{d(p\zeta +(1-p\left){\zeta }^{\prime }\right)}\left(\pi \right)=1$

(well, technically, this may not hold, but only on a set of measure 0 relative to $p\zeta +(1-p){\zeta }^{\prime }$, so we can fiddle with things a bit so this always holds), we can apply concavity of $\Theta \left(\pi \right)$ because it’s an inframeasure, for all $\pi$, and get

$\le {\int }_{\Pi }(\lambda \pi .\Theta (\pi \left)\left(\frac{d\left(p\zeta \right)}{d(p\zeta +(1-p\left){\zeta }^{\prime }\right)}\right(\pi )\cdot U_{{\pi }_1}+\frac{d\left(\right(1-p\left){\zeta }^{\prime }\right)}{d(p\zeta +(1-p\left){\zeta }^{\prime }\right)}(\pi )\cdot U_{{\pi }_2})\right)$
$d(p\zeta +(1-p\left){\zeta }^{\prime }\right)$

and then pack it back up as an expectation, to get

$=E_{\pi \sim p\zeta +(1-p){\zeta }^{\prime }}\left[\Theta \right(\pi \left)\left(\frac{d\left(p\zeta \right)}{d(p\zeta +(1-p\left){\zeta }^{\prime }\right)}\right(\pi )\cdot U_{{\pi }_1}+\frac{d\left(\right(1-p\left){\zeta }^{\prime }\right)}{d(p\zeta +(1-p\left){\zeta }^{\prime }\right)}(\pi )\cdot U_{{\pi }_2})\right]$

We will now attempt to show that, for all copolicies $e$,

$E_{\pi \sim p\zeta +(1-p){\zeta }^{\prime }}\left[\left(\frac{d\left(p\zeta \right)}{d(p\zeta +(1-p\left){\zeta }^{\prime }\right)}\right(\pi )\cdot U_{{\pi }_1}+\frac{d\left(\right(1-p\left){\zeta }^{\prime }\right)}{d(p\zeta +(1-p\left){\zeta }^{\prime }\right)}(\pi )\cdot U_{{\pi }_2})\right(\pi \cdot e\left)\right]$
$\le (pf+(1-p\left)f^{\prime }\right)\left(e\right)$

We can take that big expectation and write it as

$=E_{\pi \sim p\zeta +(1-p){\zeta }^{\prime }}\left[\frac{d\left(p\zeta \right)}{d(p\zeta +(1-p\left){\zeta }^{\prime }\right)}\right(\pi )\cdot U_{{\pi }_1}(\pi \cdot e)+\frac{d\left(\right(1-p\left){\zeta }^{\prime }\right)}{d(p\zeta +(1-p\left){\zeta }^{\prime }\right)}(\pi )\cdot U_{{\pi }_2}(\pi \cdot e\left)\right]$

and then write it as an integral

$={\int }_{\Pi }(\lambda \pi .\frac{d\left(p\zeta \right)}{d(p\zeta +(1-p\left){\zeta }^{\prime }\right)}(\pi )\cdot U_{{\pi }_1}(\pi \cdot e)+\frac{d\left(\right(1-p\left){\zeta }^{\prime }\right)}{d(p\zeta +(1-p\left){\zeta }^{\prime }\right)}(\pi )\cdot U_{{\pi }_2}(\pi \cdot e\left)\right)$
$d(p\zeta +(1-p\left){\zeta }^{\prime }\right)$

Split it up into two integrals

$={\int }_{\Pi }(\lambda \pi .U_{{\pi }_1}(\pi \cdot e)\cdot \frac{d\left(p\zeta \right)}{d(p\zeta +(1-p\left){\zeta }^{\prime }\right)}(\pi \left)\right)d(p\zeta +(1-p\left){\zeta }^{\prime }\right)$
$+{\int }_{\Pi }(\lambda \pi .U_{{\pi }_2}(\pi \cdot e)\cdot \frac{d\left(\right(1-p\left){\zeta }^{\prime }\right)}{d(p\zeta +(1-p\left){\zeta }^{\prime }\right)}(\pi \left)\right)d(p\zeta +(1-p\left){\zeta }^{\prime }\right)$

The Radon-Nikodym derivatives cancel to leave you with

$={\int }_{\Pi }(\lambda \pi .U_{{\pi }_1}(\pi \cdot e\left)\right)d\left(p\zeta \right)+{\int }_{\Pi }(\lambda \pi .U_{{\pi }_2}(\pi \cdot e\left)\right)d\left(\right(1-p\left){\zeta }^{\prime }\right)$

and then pull out the constants to get

$=p{\int }_{\Pi }(\lambda \pi .U_{{\pi }_1}(\pi \cdot e\left)\right)d\zeta +(1-p){\int }_{\Pi }(\lambda \pi .U_{{\pi }_2}(\pi \cdot e\left)\right)d{\zeta }^{\prime }$

pack up as an expectation

$=p{E}_{\pi \sim \zeta }\left[U_{{\pi }_1}\right(\pi \cdot e\left)\right]+(1-p)E_{\pi \sim {\zeta }^{\prime }}\left[U_{{\pi }_2}\right(\pi \cdot e\left)\right]$

And use that

$E_{\pi \sim \zeta }\left[U_{{\pi }_1}\right(\pi \cdot e\left)\right]\le f\left(e\right)$

$E_{\pi \sim {\zeta }^{\prime }}\left[U_{{\pi }_2}\right(\pi \cdot e\left)\right]\le f^{\prime }\left(e\right)$

to get an upper bound of

$\le (pf+(1-p\left)f^{\prime }\right)\left(e\right)$

Ok, we’re done. We now know that $p\zeta +(1-p){\zeta }^{\prime }$ is a probability distribution (mix of two probability distributions). We know that the expectation w.r.t. that distribution of the functions

$\lambda e.\left(\frac{d\left(p\zeta \right)}{d(p\zeta +(1-p\left){\zeta }^{\prime }\right)}\right(\pi )\cdot U_{{\pi }_1}+\frac{d\left(\right(1-p\left){\zeta }^{\prime }\right)}{d(p\zeta +(1-p\left){\zeta }^{\prime }\right)}(\pi )\cdot U_{{\pi }_2})(\pi \cdot e)$

undershoots $pf+(1-p)f^{\prime }$. And since this is a mix of two existing utility functions, it’ll be in $[0,1]$ if the original utility functions were in that range already (or bounded if the originals were). Taking stock of what we’ve done so far, we’ve shown that

$pE\left(f\right)+(1-p)E\left(f^{\prime }\right)\le E_{\pi \sim p\zeta +(1-p){\zeta }^{\prime }}\left[\Theta \right(\pi \left)\left(\frac{d\left(p\zeta \right)}{d(p\zeta +(1-p\left){\zeta }^{\prime }\right)}\right(\pi )\cdot U_{{\pi }_1}+\frac{d\left(\right(1-p\left){\zeta }^{\prime }\right)}{d(p\zeta +(1-p\left){\zeta }^{\prime }\right)}(\pi )\cdot U_{{\pi }_2})\right]$

but the probability distribution, and functions used, ends up mixing to undershoot $pf+(1-p)f^{\prime }$. So we can impose an upper bound of:

$\le {sup}_{{\zeta }^{\prime \prime },U_{{\pi }_3},pf+(1-p)f^{\prime }}{E}_{\pi \sim {\zeta }^{\prime \prime }}\left[\Theta \right(\pi \left)\right(U_{{\pi }_3}\left)\right]$

which then packs up to equal

$=E(pf+(1-p\left)f^{\prime }\right)$

and we’re done, concavity has been shown.

T5.1.2.4 The compact-almost-support property on $E$ is trivial since $E$ is a compact space.

T5.1.2.5 For normalization, we’ll need to do it in two parts, for both 0 and 1.

T5.1.2.5.1 First, we show normalization for 1, which requires showing both directions of the inequality. We start with

$E\left(1\right)={sup}_{\zeta ,U_{\pi },1}{E}_{\pi \sim \zeta }\left[\Theta \right(\pi \left)\right(U_{\pi }\left)\right]$

and a possible choice that the supremum ranges over is the dirac-delta distribution on the ${\pi }^{\prime }$ with the worst value of $\Theta \left(\pi \right)\left(1\right)$ (which is 1, by normalization for belief functions), and all the $U_{\pi }$ are 1. So then we get

$\ge \Theta \left({\pi }^{\prime }\right)\left(1\right)={inf}_{\pi }\Theta \left(\pi \right)\left(1\right)=1$

A lower bound of 1. For getting an upper bound, we have

$E\left(1\right)={sup}_{\zeta ,U_{\pi },1}{E}_{\pi \sim \zeta }\left[\Theta \right(\pi \left)\right(U_{\pi }\left)\right]$

and then, the supremum ranges over $\zeta ,U_{\pi }$ where $\forall e:E_{\pi \sim \zeta }\left[U_{\pi }\right(\pi \cdot e\left)\right]\le 1$

Now, 1 can be written as $U_1({\pi }^{\prime }\cdot e)$ where $U_1$ is the utility function which maps everything to 1, and ${\pi }^{\prime }$ is the policy with the worst value of $\Theta \left(\pi \right)\left(1\right)$, and we can apply our alternate formulation of causality for $\Theta$ to guarantee that

$E_{\pi \sim \zeta }\left[\Theta \right(\pi \left)\right(U_{\pi }\left)\right]\le \Theta \left({\pi }^{\prime }\right)\left(U_1\right)$

regardless of our choice of $\zeta ,U_{\pi }$. And so, we can impose an upper-bound of

$\le \Theta \left({\pi }^{\prime }\right)\left(U_1\right)=\Theta \left({\pi }^{\prime }\right)\left(1\right)={inf}_{\pi }\Theta \left(\pi \right)\left(1\right)=1$

and we’re done, we’ve got inequalities going both way, so $E\left(1\right)=1$.

T5.1.2.5.2 Now for 0. We have

$E\left(0\right)={sup}_{\zeta ,U_{\pi },0}{E}_{\pi \sim \zeta }\left[\Theta \right(\pi \left)\right(U_{\pi }\left)\right]$

and one thing that the supremum ranges over is the dirac-delta on ${\pi }^{\prime }$ which attains the worst value of $\Theta \left(\pi \right)\left(0\right)$, and all the $U_{\pi }$ being 0, so we get

$\ge \Theta \left({\pi }^{\prime }\right)\left(0\right)={inf}_{\pi }\Theta \left(\pi \right)\left(0\right)=0$

and we have a lower-bound of 0. For an upper bound,

$E\left(0\right)={sup}_{\zeta ,U_{\pi },0}{E}_{\pi \sim \zeta }\left[\Theta \right(\pi \left)\right(U_{\pi }\left)\right]$

and then, the supremum ranges over $\zeta ,U_{\pi }$ where $\forall e:E_{\pi \sim \zeta }\left[U_{\pi }\right(\pi \cdot e\left)\right]\le 0$

Now, 1 can be written as $U_0({\pi }^{\prime }\cdot e)$ where $U_0$ is the utility function which maps everything to 1, and ${\pi }^{\prime }$ is the policy with the worst value of $\Theta \left(\pi \right)\left(0\right)$, and we can apply our alternate formulation of causality for $\Theta$ to guarantee that

$E_{\pi \sim \zeta }\left[\Theta \right(\pi \left)\right(U_{\pi }\left)\right]\le \Theta \left({\pi }^{\prime }\right)\left(U_0\right)$

regardless of our choice of $\zeta ,U_{\pi }$. And so, we can impose an upper-bound of

$\le \Theta \left({\pi }^{\prime }\right)\left(U_0\right)=\Theta \left({\pi }^{\prime }\right)\left(0\right)={inf}_{\pi }\Theta \left(\pi \right)\left(0\right)=0$

and we’re done, we’ve got inequalities going both way, so $E\left(0\right)=0$.

T5.1.2.6 Now for Lipschitzness, which we’ll need to split in two for the two type signatures.

T5.1.2.6.1 This will be completely provable for the $R$ type signature on infradistributions. What we’ll do is show that for any two functions $f,f^{\prime }$, when ${\lambda }^{\odot }$is the upper bound on the Lipschitz constant for the belief function $\Theta$, we have

$E\left(f\right)-E(inf(f,f^{\prime }\left)\right)\le {\lambda }^{\odot }d(f,f^{\prime })$

Since both $f,f^{\prime }$ must be above $inf(f,f^{\prime })$, by monotonicity, this result would show that

$|E\left(f\right)-E\left(f^{\prime }\right)|\le {\lambda }^{\odot }d(f,f^{\prime })$

and then we’d be done, that’s Lipschitzness. So let’s get working. We unpack as

$E\left(f\right)-E(inf(f,f^{\prime }\left)\right)={sup}_{\zeta ,U_{{\pi }_1},f}{E}_{\pi \sim \zeta }\left[\Theta \right(\pi \left)\right(U_{{\pi }_1}\left)\right]-{sup}_{{\zeta }^{\prime },U_{{\pi }_2},inf(f,f^{\prime })}{E}_{\pi \sim \zeta }\left[\Theta \right(\pi \left)\right(U_{{\pi }_2}\left)\right]$

Consider the supremum of the first term to be attained by some choice of $\zeta ,U_{{\pi }_1}$ fulfilling the property that $\forall e:E_{\pi \sim \zeta }\left[U_{{\pi }_1}\right(\pi \cdot e\left)\right]\le f\left(e\right)$ and then we can rewrite as

$=E_{\pi \sim \zeta }\left[\Theta \right(\pi \left)\right(U_{{\pi }_1}\left)\right]-{sup}_{{\zeta }^{\prime },U_{{\pi }_2},inf(f,f^{\prime })}{E}_{\pi \sim \zeta }\left[\Theta \right(\pi \left)\right(U_{{\pi }_2}\left)\right]$

Now, let your choice of ${\zeta }^{\prime }$ be $\zeta$, and your choice of the $U_{{\pi }_2}$ family be $U_{{\pi }_1}-d(f,f^{\prime })$. We do need to show that

$\forall e:E_{\pi \sim \zeta }\left[U_{{\pi }_1}\right(\pi \cdot e)-d(f,f^{\prime }\left)\right]\le inf(f,f^{\prime })\left(e\right)$

This is easy, we can fix an arbitrary $e$, and go

$E_{\pi \sim \zeta }\left[U_{{\pi }_1}\right(\pi \cdot e)-d(f,f^{\prime }\left)\right]=E_{\pi \sim \zeta }\left[U_{{\pi }_1}\right(\pi \cdot e\left)\right]-d(f,f^{\prime })\le f\left(e\right)-d(f,f^{\prime })\le inf(f,f^{\prime })\left(e\right)$

So, this choice of ${\zeta }^{\prime }$ and $U_{{\pi }_2}$ works out. Now we can go

$E_{\pi \sim \zeta }\left[\Theta \right(\pi \left)\right(U_{{\pi }_1}\left)\right]-{sup}_{{\zeta }^{\prime },U_{{\pi }_2},inf(f,f^{\prime })}{E}_{\pi \sim \zeta }\left[\Theta \right(\pi \left)\right(U_{{\pi }_2}\left)\right]$

$\le E_{\pi \sim \zeta }\left[\Theta \right(\pi \left)\right(U_{{\pi }_1}\left)\right]-E_{\pi \sim \zeta }\left[\Theta \right(\pi \left)\right(U_{{\pi }_1}-d(f,f^{\prime })\left)\right]$

And then, by monotonicity and a shared Lipschitz constant for the $\Theta \left(\pi \right)$, we have

$\le E_{\pi \sim \zeta }\left[\Theta \right(\pi \left)\right(U_{{\pi }_1}\left)\right]-E_{\pi \sim \zeta }\left[\Theta \right(\pi \left)\right(U_{{\pi }_1})-{\lambda }^{\odot }d(f,f^{\prime }\left)\right]$

$=E_{\pi \sim \zeta }\left[\Theta \right(\pi \left)\right(U_{{\pi }_1}\left)\right]-E_{\pi \sim \zeta }\left[\Theta \right(\pi \left)\right(U_{{\pi }_1}\left)\right]+{\lambda }^{\odot }d(f,f^{\prime })={\lambda }^{\odot }d(f,f^{\prime })$

And we’ve shown what we came here to show,

$E\left(f\right)-E(inf(f,f^{\prime }\left)\right)\le {\lambda }^{\odot }d(f,f^{\prime })$

$f,f^{\prime }$ were arbitrary, so by monotonicity for $E$, we have

$|E\left(f\right)-E\left(f^{\prime }\right)|\le {\lambda }^{\odot }d(f,f^{\prime })$

and $E$ has a finite Lipschitz constant for the $R$ type signature.

T5.1.2.6.2 Now for the fiddly bits with the $[0,1]$ type signature. The reason the above proof doesn’t work for that type signature is that all our functions have to remain in $[0,1]$, and it’s possible that subtracting $d(f,f^{\prime })$ from all the $U_{\pi }$ results in functions that go outside of $[0,1]$, and it’s way way harder than it looks to patch this.

We have all the other properties, though. What unbounded Lipschitz constant for $E$ (as an expectation functional) looks like from the set point of view is that we’ve got minimal points in the set of a-measures over $E$ (our $E$) with unboundedly large measure components. However, all the $\Theta \left(\pi \right)$ infradistribution sets have a bounded Lipschitz constant of ${\lambda }^{\odot }$, all their minimal points can have only ${\lambda }^{\odot }$ measure at most.

If you took your set $E$, and chucked out all the minimal points with measure greater than ${\lambda }^{\odot }$ and built up an infradistribution $E^{\prime }$ from the remaining minimal points, $E^{\prime }$ would produce $\Theta$ again if you went back to a belief function. Why?

Well, the minimal points of an inframeasure/​distribution are the truly critical part of them. As long as two sets of a-measures agree on which a-measures are minimal points, they’re completely 100 percent equivalent in all respects. We travel back to a belief function $\Theta \left(\pi \right)$ via applying the pushforward $(\pi \cdot {)}_{\ast }(E)$. Doing this pushforward, in the set view keeps all the measure components of a-measures the same. So, chucking out all the a-measures in $E$ with too much measure doesn’t throw out any a-measures in $E$ which are necessary to produce a minimal point in some $\Theta \left(\pi \right)$ (all of those have ${\lambda }^{\odot }$ measure or less). When we apply the pushforward to $E^{\prime }$ instead of $E$, we get a smaller set, sure, but the set perfectly agrees with the pushforward of $E$ on the minimal points, so the sets they produce are equivalent. You get the same belief function back.

T5.1.2.7 Now for the last part, showing that we get the causality condition on $E$. Using our rewrite of $E$, we have

$E\left(f\right)={sup}_{\zeta ,U_{\pi },f}{E}_{\pi \sim \zeta }\left[\right(\Theta \left(\pi \right)\left)\right(U_{\pi }\left)\right]$

and then, by causality for $\Theta$, we get

$={sup}_{\zeta ,U_{\pi },f}{E}_{\pi \sim \zeta }\left[{sup}_{{\zeta }_{\pi }^{\prime },U_{{\pi }_{\pi }^{\prime }},U_{\pi }(\pi \cdot \bullet )}{E}_{{\pi }^{\prime }\sim {\zeta }_{\pi }^{\prime }}\right[\left(\Theta \right({\pi }^{\prime }\left)\right)\left(U_{{\pi }_{\pi }^{\prime }}\right)\left]\right]$

Note that there’s a dependence of the second probability distribution and choice of utility functions on the the $\pi$ selected, because we have a separate $sup$ for each $\pi$. Since our rewrite of $E\left(f\right)$ was

$E\left(f\right)={sup}_{\zeta ,U_{\pi },f}{E}_{\pi \sim \zeta }\left[\right(\Theta \left(\pi \right)\left)\right(U_{\pi }\left)\right]$

we can abbreviate the interior of the big equation we have to get

$={sup}_{\zeta ,U_{\pi },f}{E}_{\pi \sim \zeta }\left[E\right(\lambda e.U_{\pi }(\pi \cdot e)\left)\right]$

Which is the causality condition for $E$.

T5.1.3 For 3-static to 3-dynamic, it’s easy, since ${\psi }_T:=E$ so it can just copy over the relevant causality property from $E$, and we specified that the transition dynamics are exactly what we need, ${\to }_T\left(e\right):={\top }_A⋉(\lambda a.{\delta }_{e\left(a\right),e_{a,e\left(a\right)}})$

T5.1.4 For 3-dynamic to 3-static, this will be tricky, so first we set up some preliminaries. The translation process is unrolling the action-observation sequence to get an infradistribution over destinies, and then turning that into a belief function, and then turning that back into a set of copolicies. Ie,

$E:={\bigwedge }_{\pi }(\pi \cdot {)}^{\ast }\left(u_{\sim \pi }^1\left(p{r}_{(A\times O{)}^{\omega }\ast }\right({\psi }_T⋉{\to }_{T:\infty }\left)\right)\right)$

We can save on some work. We recently established that going from a causal belief function to the space of copolicies produces an infradistribution over copolicies with the causality condition. So, actually, all we need to do is show that doing the first two steps (and skipping the third) makes a causal belief function, and we’ll be done.

This is essentially going from third-person dynamic to third-person static (in destiny form), to first-person static, so we should expect it to be a bit hard. So our goal is that

$\Theta \left(\pi \right):=u_{\sim \pi }^1\left(p{r}_{(A\times O{)}^{\omega }\ast }\right({\psi }_T⋉{\to }_{T:\infty }\left)\right)$

ends up making a causal belief function.

Obviously, we need to show the causality property for $\Theta$. However, for all other belief function conditions, we get them for free as long as we have an actual infradistribution over histories (this can be shown by taking the arguments that you get a belief function from translating over an infradistribution back in the Acausal Square Theorem, and adapting them to the pseudocausal case, which is pretty easy). So, actually, all we need to show is that $\Theta$ is causal, and that $p{r}_{(A\times O{)}^{\omega }\ast }({\psi }_T⋉{\to }_{T:\infty })$ is an infradistribution over histories, assuming that ${\psi }_T$ is an infradistribution over copolicies.

So, the proof splits into four parts where we verify the niceness conditions on ${\to }_T$ in order to show that the above line is an infradistribution over histories, and one part where we verify causality for $\Theta$

First up, verifying the niceness conditions for ${\to }_T$ so ${\to }_{T:\infty }$ is well-defined.

T5.1.4.1 We’ll start with lower-semicontinuity, though actually, we’ll be going for something stronger, continuity.

${lim}_{n\to \infty }{\to }_T\left(e^n\right)\left(f\right)={lim}_{n\to \infty }({\top }_A⋉(\lambda a.{\delta }_{e^n\left(a\right),e_{a,e^n\left(a\right)}^n}\left)\right)(\lambda a,o,e.f(a,o,e\left)\right)$

and then unpack the semidirect product and subsitute the dirac-delta values in to get

$={lim}_{n\to \infty }{\top }_A(\lambda a.f(a,e^n\left(a\right),e_{a,e^n\left(a\right)}^n\left)\right)$

and unpack what ${\top }_A$ means to get

$={lim}_{n\to \infty }{inf}_{a}f(a,e^n(a),e_{a,e^n\left(a\right)}^n)$

There are finitely many actions, so we can shift the limit in, to get

$={inf}_a{lim}_{n\to \infty }f(a,e^n(a),e_{a,e^n\left(a\right)}^n)$

Now, as $e^n$ approaches $e^{\infty }$, the observation returned for the first action stabilizes, so we get

$={inf}_a{lim}_{n\to \infty }f(a,e^{\infty }(a),e_{a,e^{\infty }\left(a\right)}^n)$

And then, due to continuity of $f$, and $e_{a,e^{\infty }\left(a\right)}^n$ converging to $e_{a,e^{\infty }\left(a\right)}^{\infty }$ because $e^n$ converges to $e^{\infty }$, we have

$={inf}_{a}f(a,e^{\infty }(a),e_{a,e^{\infty }\left(a\right)}^{\infty })$

Which then packs up in reverse as

$={\top }_A(\lambda a.f(a,e^{\infty }\left(a\right),e_{a,e^{\infty }\left(a\right)}^{\infty }\left)\right)$

$=({\top }_A⋉(\lambda a.{\delta }_{e^{\infty }\left(a\right),e_{a,e^{\infty }\left(a\right)}^{\infty }}\left)\right)(\lambda a,o,e.f(a,o,e\left)\right)={\to }_T\left(e^{\infty }\right)\left(f\right)$

And continuity has been shown. This inducts up to show continuity for ${\to }_{T:\infty }$.

T5.1.4.2 1-Lipschitzness holds because ${\to }_T$ is the semidirect product of a crisp infradistribution (${\top }_A$) (and all crisp infradistributions are 1-Lipschitz) with a crisp infrakernel (also 1-Lipschitz), and the semidirect product of a 1-Lipschitz infrakernel and a 1-Lipschitz infradistribution is 1-Lipschitz.

T5.1.4.3 Compact-shared almost-compact-support is trivial because $A\times O\times E$ is a compact space.

T5.1.4.4 For “constants increase”, actually, crisp infrakernels map constants to the same constant. So we get a stronger result, that ${\to }_T\left(e\right)\left(c\right)=c$, and in particular, ${\to }_{T:\infty }\left(e\right)\left(c\right)=c$ (the property inducts up appropriately). This also has the implication that all the ${\to }_{T:\infty }\left(e\right)$ are infradistributions, as they map 0 to 0 and 1 to 1. This also bags the last condition, 1-normalization. That’s all niceness conditions, so ${\to }_{T:\infty }$is well-defined.

Now that we know it’s well-defined at all, our goal is to show that

$p{r}_{(A\times O{)}^{\omega }\ast }({\psi }_T⋉{\to }_{T:\infty })$

is an infradistribution. This is, again, easy. The semidirect product of an infradistribution and a continuous infrakernel that returns infradistributions is an infradistribution, and the projection of an infradistribution is an infradistribution.

T5.1.4.5 With that, all that remains is showing that $\Theta$, defined as

$\Theta \left({\pi }^{\prime }\right):=u_{\sim {\pi }^{\prime }}^1\left(p{r}_{(A\times O{)}^{\omega }\ast }\right({\psi }_T⋉{\to }_{T:\infty }\left)\right)$

fulfills the causality property. We can rewrite the update and projection to get

$\Theta \left({\pi }^{\prime }\right)\left(U\right)=({\psi }_T⋉{\to }_{T:\infty })(\lambda e_0,ao{e}_{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 }})$

and rewrite the semidirect product

$={\psi }_T(\lambda e_0.{\to }_{T:\infty }(e_0\left)\right(\lambda ao{e}_{1:\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)$

and then write this as a projection,

$={\psi }_T(\lambda e_0.p{r}_{(A\times O{)}^{\omega }\ast }({\to }_{T:\infty }\left(e_0\right)\left)\right(\lambda a{o}_{1:\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)$

and then write this as an update

$={\psi }_T(\lambda e_0.u_{\sim {\pi }^{\prime }}^1(p{r}_{(A\times O{)}^{\omega }\ast }\left({\to }_{T:\infty }\right(e_0\left)\right)\left)\right(\lambda a{o}_{1:\infty }.U\left(a{o}_{1:\infty }\right)\left)\right)$

Now, we should notice something really important here. $p{r}_{(A\times O{)}^{\omega }\ast }\left({\to }_{T:\infty }\right(e_0\left)\right)$, because ${\to }_T$ has complete ignorance over the actions, but has the observations and next copolicies determined by interacting with $e_0$, is the infradistribution generated by all probabilistic mixes of histories capable of being produced by $e_0$. We can think of this as being generated by dirac-delta distributions on all the histories compatible with the copolicy $e_0$.

Updating a dirac-delta on a history on “is the history compatible with ${\pi }^{\prime }$?” will, if it isn’t compatible, make the $(0,1)$ a-measure present in all infradistributions (cannibalize the measure into the b term), (or delete the point entirely for the $R$ type signature) and if it is a dirac-delta distribution on a compatible history, leaves it alone. However, there’s only one history compatible with ${\pi }^{\prime }$ and $e_0$, it’s ${\delta }_{{\pi }^{\prime }\cdot e_0}$, the history made from the two interacting. Thus,

$u_{\sim {\pi }^{\prime }}^1\left(p{r}_{(A\times O{)}^{\omega }\ast }\right({\to }_{T:\infty }\left(e_0\right)\left)\right)={\delta }_{{\pi }^{\prime }\cdot e_0}$

Making this substitution, we get

$={\psi }_T(\lambda e_0.{\delta }_{{\pi }^{\prime }\cdot e_0}(\lambda a{o}_{1:\infty }.U\left(a{o}_{1:\infty }\right)\left)\right)$

And putting the value in the function, we get

$={\psi }_T(\lambda e_0.U({\pi }^{\prime }\cdot e_0\left)\right)$

Now we can apply the causality condition our ${\psi }_T$ has, yielding

$={sup}_{\zeta ,U_{\pi },U({\pi }^{\prime }\cdot \bullet )}{E}_{\pi \sim \zeta }\left[{\psi }_T\right(\lambda e_0.U_{\pi }(\pi \cdot e_0)\left)\right]$

and go in reverse, breaking this out into a dirac-delta to get

$={sup}_{\zeta ,U_{\pi },U({\pi }^{\prime }\cdot \bullet )}{E}_{\pi \sim \zeta }\left[{\psi }_T\right(\lambda e_0.{\delta }_{\pi \cdot e_0}\left(U_{\pi }\right)\left)\right]$

And rewriting this as an update on the projection of the semidirect product initialized on a particular copolicy, yielding

$={sup}_{\zeta ,U_{\pi },U({\pi }^{\prime }\cdot \bullet )}{E}_{\pi \sim \zeta }\left[{\psi }_T\right(\lambda e_0.u_{\sim \pi }^1\left(p{r}_{(A\times O{)}^{\omega }\ast }\right({\to }_{T:\infty }\left(e_0\right)\left)\right)(\lambda a{o}_{1:\infty }.U_{\pi }(a{o}_{1:\infty }\left)\right)\left)\right]$

And expand the update

$={sup}_{\zeta ,U_{\pi },U({\pi }^{\prime }\cdot \bullet )}{E}_{\pi \sim \zeta }\left[{\psi }_T\right(\lambda e_0.p{r}_{(A\times O{)}^{\omega }\ast }\left({\to }_{T:\infty }\right(e_0\left)\right)(\lambda a{o}_{1:\infty }.{\text{1}}_{a{o}_{1:\infty }\sim \pi }{U}_{\pi }(a{o}_{1:\infty })+{\text{1}}_{a{o}_{1:\infty }\nsim \pi })\left)\right]$

And remove the projection

$={sup}_{\zeta ,U_{\pi },U({\pi }^{\prime }\cdot \bullet )}{E}_{\pi \sim \zeta }\left[{\psi }_T\right(\lambda e_0.{\to }_{T:\infty }\left(e_0\right)(\lambda ao{e}_{1:\infty }.{\text{1}}_{a{o}_{1:\infty }\sim \pi }{U}_{\pi }(a{o}_{1:\infty })+{\text{1}}_{a{o}_{1:\infty }\nsim \pi })\left)\right]$

And pack up as a semidirect product and projection

$={sup}_{\zeta ,U_{\pi },U({\pi }^{\prime }\cdot \bullet )}{E}_{\pi \sim \zeta }\left[p{r}_{(A\times O{)}^{\omega }\ast }\right({\psi }_T⋉{\to }_{T:\infty }\left)\right(\lambda a{o}_{1:\infty }.{\text{1}}_{a{o}_{1:\infty }\sim \pi }{U}_{\pi }\left(a{o}_{1:\infty }\right)+{\text{1}}_{a{o}_{1:\infty }\nsim \pi }\left)\right]$

and pack up the update

$={sup}_{\zeta ,U_{\pi },U({\pi }^{\prime }\cdot \bullet )}{E}_{\pi \sim \zeta }\left[u_{\sim \pi }^1\right(p{r}_{(A\times O{)}^{\omega }\ast }({\psi }_T⋉{\to }_{T:\infty })\left)\right(\lambda a{o}_{1:\infty }.U_{\pi }\left(a{o}_{1:\infty }\right)\left)\right]$

and do just one more rewrite to crunch down the function a little bit

$={sup}_{\zeta ,U_{\pi },U({\pi }^{\prime }\cdot \bullet )}{E}_{\pi \sim \zeta }\left[u_{\sim \pi }^1\right(p{r}_{(A\times O{)}^{\omega }\ast }({\psi }_T⋉{\to }_{T:\infty })\left)\right(U_{\pi }\left)\right]$

and pack this up into a belief function like how we defined it, to get

$={sup}_{\zeta ,U_{\pi },U({\pi }^{\prime }\cdot \bullet )}{E}_{\pi \sim \zeta }\left[\Theta \right(\pi \left)\right(U_{\pi }\left)\right]$

and we’re done, we made a causal belief function, and we know that going further from that to the infradistribution on copolicies endows that with the causality condition.

T5.1.5 3-dynamic to 1-dynamic. We don’t have to worry about the starting infradistributions, as they’re identical to each other, so the relevant causality condition is inherited, we just have to check that the infrakernels transform appropriately. We have

${\to }_F(e,a):=p{r}_{O\times E\ast }\left(u_{\left\{a\right\}}^1\right({\to }_T\left(e\right)\left)\right)$

For any action a, applying our definition, we have

${\to }_F(e,a)\left(f\right)=p{r}_{O\times E\ast }\left(u_{\left\{a\right\}}^1\right({\to }_T\left(e\right)\left)\right)\left(f\right)$

Unpacking the projection and update, we have

$={\to }_T\left(e\right)(\lambda a^{\prime },o^{\prime },e^{\prime }.{\text{1}}_{a^{\prime }=a}f(o^{\prime },e^{\prime })+{\text{1}}_{a^{\prime }\ne a})$

And then we consider that ${\to }_T\left(e\right)={\top }_A⋉(\lambda a.{\delta }_{e\left(a\right),e_{a,e\left(a\right)}})$, so we have

$=({\top }_A⋉(\lambda a.{\delta }_{e\left(a\right),e_{a,e\left(a\right)}}\left)\right)(\lambda a^{\prime },o^{\prime },e^{\prime }.{\text{1}}_{a^{\prime }=a}f(o^{\prime },e^{\prime })+{\text{1}}_{a^{\prime }\ne a})$

Unpacking the semidirect product, we have

$={\top }_A(\lambda a^{\prime }.{\delta }_{e\left(a\right),e_{a,e\left(a\right)}}(\lambda o^{\prime },e^{\prime }.{\text{1}}_{a^{\prime }=a}f(o^{\prime },e^{\prime })+{\text{1}}_{a^{\prime }\ne a}\left)\right)$

and substituting the dirac-delta values in, we have

$={\top }_A(\lambda a^{\prime }.{\text{1}}_{a^{\prime }=a}f(e\left(a\right),e_{a,e\left(a\right)})+{\text{1}}_{a^{\prime }\ne a})$

Unpacking what ${\top }_A$ is, we have

$={inf}_{a^{\prime }}{\text{1}}_{a^{\prime }=a}f\left(e\right(a),e_{a,e\left(a\right)})+{\text{1}}_{a^{\prime }\ne a})$

This is 1 or infinity when $a^{\prime }\ne a$, so $a^{\prime }=a$.

$=f\left(e\right(a),e_{a,e\left(a\right)})$

And then we just pull out a dirac-delta

$={\delta }_{e\left(a\right),e_{a,e\left(a\right)}}\left(f\right)$

and we’re done! The infrakernel has the right form.

T5.1.6 3-dynamic to 1-dynamic. We know ${\to }_T\left(e\right):={\top }_A⋉(\lambda a.{\to }_F(e,a\left)\right)$

and we know ${\to }_F(e,a)={\delta }_{e\left(a\right),e_{a,e\left(a\right)}}$ and we want

${\to }_T\left(e\right)={\top }_A⋉(\lambda a.{\delta }_{e\left(a\right),e_{a,e\left(a\right)}})$

This is tautological, no problems here.

T5.1.7 1-static to 1-dynamic. Well, we’re going 1-static to 1-dynamic via

${\psi }_F:={\bigwedge }_{\pi }(\pi \cdot {)}^{\ast }(\Theta \left(\pi \right))$

So we can just copy the proof of 1-static to 3-static, the translation functions are the same in both cases. The infrakernel also works out appropriately.

T5.1.8 1-dynamic to 1-static. We define our belief function via

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

This proof will be very similar to third-person dynamic to third-person static, but easier. To cut down on a truly aggravating amount of overhead, we invoke our Theorem 4 on pseudocausal IPOMDP’s. Our state space is $E$. We only need to show that ${\to }_F$ fulfills the niceness conditions, and we then know that $\Theta$ fulfills all belief function conditions except for maybe normalization.

Our game plan is to show that ${\to }_F$ fulfills the niceness conditions on an infrakernel (four parts, since we can sort of lump 1-normalization in with moving constants up), show that $\Theta$ fulfills the normalization property (last thing needed to show it’s a belief function that Theorem 4 doesn’t get), and then show that $\Theta$ is causal, for 6 parts in total.

T5.1.8.1 First niceness condition, lower-semicontinuity. We’ll go for continuity instead, it’s as easy to show.

${lim}_{n\to \infty }{\to }_F(e^n,a^n)\left(f\right)={lim}_{n\to \infty }{\delta }_{e^n\left(a^n\right),e_{a^n,e^n\left(a^n\right)}^n}(\lambda o,e.f(o,e\left)\right)$

$={lim}_{n\to \infty }f\left(e^n\right(a^n),e_{a^n,e^n\left(a^n\right)}^n)$

We know that $a^n$ settles down to $a^{\infty }$ after finite time because the action space is finite, and $e^n\left(a\right)$ settles down to $e^{\infty }\left(a\right)$ for any action because eventually the copolicy settles down on what it does for the initial action, so we get

$={lim}_{n\to \infty }f\left(e^{\infty }\right(a^{\infty }),e_{a^{\infty },e^{\infty }\left(a^{\infty }\right)}^n)$

and, in the limit, because $f$ is continuous, and $e^n$ limits to $e^{\infty }$, we have

$=f\left(e^{\infty }\right(a^{\infty }),e_{a^{\infty },e^{\infty }\left(a^{\infty }\right)}^{\infty })={\delta }_{e^{\infty }\left(a^{\infty }\right),e_{a^{\infty },e^{\infty }\left(a^{\infty }\right)}^{\infty }}(\lambda o,e.f(o,e\left)\right)$

$={\to }_F(e^{\infty },a^{\infty })\left(f\right)$

and we’re done, continuity is shown.

T5.1.8.2 Compact-shared compact-almost-support is trivial because $O\times E$ is a compact space.

T5.1.8.3,4 1-Lipschitzness, and mapping constants to constants (ie, ${\to }_F(e,a)\left(c\right)=c$) are trivial because it’s a single probability distribution, and those are always 1-Lipschitz and map constants to constants. In particular, 1 gets mapped to 1 so that’s the fifth niceness condition taken care of. The infinite infrakernel is well-defined, and our theorem can be invoked.

T5.1.8.5 To get normalization for $\Theta$, we first observe that since all the ${\to }_F$ map constants to the same constant, the same applies to all the ${\to }_{F,n}^{\pi }$, and then to the infinite infrakernel ${\to }_{F:\infty }^{\pi }$. So we have

${inf}_{\pi }\Theta \left(\pi \right)\left(1\right)={inf}_{\pi }p{r}_{(A\times O{)}^{\omega }\ast }({\psi }_F⋉{\to }_{F:\infty }^{\pi })\left(1\right)$

$={inf}_{\pi }({\psi }_F⋉{\to }_{F:\infty }^{\pi })\left(1\right)={inf}_{\pi }{\psi }_F(\lambda e.{\to }_{F:\infty }^{\pi }(e\left)\right(1\left)\right)$

and then, since constants are mapped to the same constant, we have

$={inf}_{\pi }{\psi }_F\left(1\right)=1$

Where that last step was done by normalization for ${\psi }_F$ since it’s an infradistribution and thus normalized. The exact same argument works for 0, showing that the resulting $\Theta$ is normalized and thus a belief function.

T5.1.8.6 All that remains is to show causality for $\Theta$. We want to show that

$\Theta \left({\pi }^{\prime }\right)\left(U\right)={sup}_{\zeta ,U_{\pi },U({\pi }^{\prime }\cdot \bullet )}{E}_{\pi \sim \zeta }\left[\Theta \right(\pi \left)\right(U_{\pi }\left)\right]$

To do this, just go

$\Theta \left({\pi }^{\prime }\right)\left(U\right)=p{r}_{(A\times O{)}^{\omega }\ast }({\psi }_F⋉{\to }_{F:\infty }^{{\pi }^{\prime }})(\lambda a{o}_{1:\infty }.U(a{o}_{1:\infty }\left)\right)$

and reexpress the projection and semidirect product to get

$={\psi }_F(\lambda e_0.{\to }_{F:\infty }^{{\pi }^{\prime }}(e_0\left)\right(\lambda ao{e}_{1:\infty }.U\left(a{o}_{1:\infty }\right)\left)\right)$

and wrap this back up as a projection to get

$={\psi }_F(\lambda e_0.p{r}_{(A\times O{)}^{\omega }\ast }({\to }_{F:\infty }^{{\pi }^{\prime }}\left(e_0\right)\left)\right(\lambda a{o}_{1:\infty }.U\left(a{o}_{1:\infty }\right)\left)\right)$

And then we observe that $p{r}_{(A\times O{)}^{\omega }\ast }\left({\to }_{F:\infty }^{{\pi }^{\prime }}\right(e_0\left)\right)$is just ${\delta }_{{\pi }^{\prime }\cdot e_0}$, because the infradistribution is “repeatedly play ${\pi }^{\prime }$ against $e_0$ and record the actions and observations you get”, so making that substitution we get

$={\psi }_F(\lambda e_0.{\delta }_{{\pi }^{\prime }\cdot e_0}(\lambda a{o}_{1:\infty }.U\left(a{o}_{1:\infty }\right)\left)\right)$

And then we can substite the dirac-delta in and get

$={\psi }_F(\lambda e_0.U({\pi }^{\prime }\cdot e_0\left)\right)$

and apply the causality condition for ${\psi }_F$ to get

$={sup}_{\zeta ,U_{\pi },U({\pi }^{\prime }\cdot \bullet )}{E}_{\pi \sim \zeta }\left[{\psi }_F\right(\lambda e_0.U_{\pi }(\pi \cdot e_0)\left)\right]$

And then we go in reverse, substituting the dirac-delta for $p{r}_{(A\times O{)}^{\omega }\ast }\left({\to }_{F:\infty }^{\pi }\right(e_0\left)\right)$ and then pulling out projections and expressing as a semidirect product and reexpressing it as a projection to get

$={sup}_{\zeta ,U_{\pi },U({\pi }^{\prime }\cdot \bullet )}{E}_{\pi \sim \zeta }\left[p{r}_{(A\times O{)}^{\omega }\ast }\right({\psi }_F⋉{\to }_{F:\infty }^{\pi }\left)\right(U_{\pi }\left)\right]$

and then pack it back up to get

$={sup}_{\zeta ,U_{\pi },U({\pi }^{\prime }\cdot \bullet )}{E}_{\pi \sim \zeta }\left[\Theta \right(\pi \left)\right(U_{\pi }\left)\right]$

and we’re done, that’s the last of it! Time for isomorphism directions.

T5.2.1 First, 1-static to 3-static to 1-static. We want to show

$E={\bigwedge }_{\pi }(\pi \cdot {)}^{\ast }((\pi \cdot {)}_{\ast }(E\left)\right)$

Breaking down the big intersection, we get

${\bigwedge }_{\pi }(\pi \cdot {)}^{\ast }((\pi \cdot {)}_{\ast }(E\left)\right)\left(f\right)={sup}_{\zeta ,f_{\pi },f}{E}_{\pi \sim \zeta }\left[\right(\pi \cdot {)}^{\ast }\left(\right(\pi \cdot {)}_{\ast }\left(E\right)\left)\right(\lambda e.f_{\pi }\left(e\right)\left)\right]$

and breaking down the pullbacks, we get

$={sup}_{\zeta ,f_{\pi },f}{E}_{\pi \sim \zeta }\left[{sup}_{U_{\pi },f_{\pi }}\right((\pi \cdot {)}_{\ast }(E\left)\right)(\lambda h.U_{\pi }(h\left)\right)]$

and reexpressing the pushforward, we get

$={sup}_{\zeta ,f_{\pi },f}{E}_{\pi \sim \zeta }\left[{sup}_{U_{\pi },f_{\pi }}E\right(\lambda e.U_{\pi }(\pi \cdot e)\left)\right]$

Folding the sups into one, we get

$={sup}_{\zeta ,U_{\pi },f}{E}_{\pi \sim \zeta }\left[E\right(\lambda e.U_{\pi }(\pi \cdot e)\left)\right]$

Which, by the causality condition for $E$, is $E\left(f\right)$ and we’re done! In fact, the causality condition for $E$ is basically just saying that going 1-static to 3-static to 1-static is identity.

T5.2.2 For 3-static to 1-static to 3-static, we want to show that

$\Theta \left({\pi }^{\prime }\right)=({\pi }^{\prime }\cdot {)}_{\ast }\left({\bigwedge }_{\pi }\right(\pi \cdot {)}^{\ast }\left(\Theta \right(\pi \left)\right))$

Taking the latter thing

$({\pi }^{\prime }\cdot {)}_{\ast }\left({\bigwedge }_{\pi }\right(\pi \cdot {)}^{\ast }\left(\Theta \right(\pi \left)\right))(U)$

and undoing the pushforward, we get

$={\bigwedge }_{\pi }(\pi \cdot {)}^{\ast }(\Theta \left(\pi \right)\left)\right(\lambda e.U({\pi }^{\prime }\cdot e))$

And reexpressing the intersection, we get

$={sup}_{\zeta ,f_{\pi },U({\pi }^{\prime }\cdot \bullet )}{E}_{\pi \sim \zeta }\left[\right(\pi \cdot {)}^{\ast }\left(\Theta \right(\pi \left)\right)(\lambda e.f_{\pi }(e\left)\right)]$

and reexpressing the pullback, we get

$={sup}_{\zeta ,f_{\pi },U({\pi }^{\prime }\cdot \bullet )}{E}_{\pi \sim \zeta }\left[{sup}_{U_{\pi },f_{\pi }}\Theta \right(\pi \left)\right(\lambda h.U_{\pi }\left(h\right)\left)\right]$

folding the sups into one, we get

$={sup}_{\zeta ,U_{\pi },U({\pi }^{\prime }\cdot \bullet )}{E}_{\pi \sim \zeta }\left[\Theta \right(\pi \left)\right(U_{\pi }\left)\right]$

And, by causality for $\Theta$, this is just

$=\Theta \left({\pi }^{\prime }\right)\left(U\right)$

and we’re done there.

T5.2.3 For 3-static to 3-dynamic to 3-static, this will be tricky, because third-person dynamic to third-person static is a complicated operation. We want to show that

$E={\bigwedge }_{\pi }(\pi \cdot {)}^{\ast }\left(u_{\sim \pi }^1\left(p{r}_{(A\times O{)}^{\omega }\ast }\right(E⋉{\to }_{T:\infty }\left)\right)\right)$

So, let’s take the big thing and start unpacking it.

${\bigwedge }_{\pi }(\pi \cdot {)}^{\ast }\left(u_{\sim \pi }^1\left(p{r}_{(A\times O{)}^{\omega }\ast }\right(E⋉{\to }_{T:\infty }\left)\right)\right)(f)$

we undo the big and, to get

$={sup}_{\zeta ,f_{\pi },f}{E}_{\pi \sim \zeta }\left[\right(\pi \cdot {)}^{\ast }\left(u_{\sim \pi }^1\left(p{r}_{(A\times O{)}^{\omega }\ast }\right(E⋉{\to }_{T:\infty }\left)\right)\right)(\lambda e.f_{\pi }(e\left)\right)]$

and then reexpress the pullbacks to get

$={sup}_{\zeta ,f_{\pi },f}{E}_{\pi \sim \zeta }\left[{sup}_{U_{\pi },f_{\pi }}\left(u_{\sim \pi }^1\left(p{r}_{(A\times O{)}^{\omega }\ast }\right(E⋉{\to }_{T:\infty }\left)\right)\right)\right(\lambda a{o}_{1:\infty }.U_{\pi }\left(a{o}_{1:\infty }\right)\left)\right]$

and then fold the two sups into one to get

$={sup}_{\zeta ,U_{\pi },f}{E}_{\pi \sim \zeta }\left[u_{\sim \pi }^1\left(p{r}_{(A\times O{)}^{\omega }\ast }\right(E⋉{\to }_{T:\infty }\left)\right)\right(\lambda a{o}_{1:\infty }.U_{\pi }\left(a{o}_{1:\infty }\right)\left)\right]$

and then reexpress the update to get

$={sup}_{\zeta ,U_{\pi },f}{E}_{\pi \sim \zeta }\left[p{r}_{(A\times O{)}^{\omega }\ast }\right(E⋉{\to }_{T:\infty }\left)\right(\lambda a{o}_{1:\infty }.{\text{1}}_{a{o}_{1:\infty }\sim \pi }{U}_{\pi }\left(a{o}_{1:\infty }\right)+{\text{1}}_{a{o}_{1:\infty }\nsim \pi }\left)\right]$

And then reexpress the projection and semidirect product to get

$={sup}_{\zeta ,U_{\pi },f}{E}_{\pi \sim \zeta }\left[E\right(\lambda e_0.{\to }_{T:\infty }\left(e_0\right)(\lambda ao{e}_{1:\infty }.{\text{1}}_{a{o}_{1:\infty }\sim \pi }{U}_{\pi }(a{o}_{1:\infty })+{\text{1}}_{a{o}_{1:\infty }\nsim \pi })\left)\right]$

And then wrap it back up in a projection to get

$={sup}_{\zeta ,U_{\pi },f}{E}_{\pi \sim \zeta }\left[E\right(\lambda e_0.p{r}_{(A\times O{)}^{\omega }\ast }\left({\to }_{T:\infty }\right(e_0\left)\right)(\lambda a{o}_{1:\infty }.{\text{1}}_{a{o}_{1:\infty }\sim \pi }{U}_{\pi }(a{o}_{1:\infty })+{\text{1}}_{a{o}_{1:\infty }\nsim \pi })\left)\right]$

And then rewrite this as an update, to get

$={sup}_{\zeta ,U_{\pi },f}{E}_{\pi \sim \zeta }\left[E\right(\lambda e_0.u_{\sim \pi }^1\left(p{r}_{(A\times O{)}^{\omega }\ast }\right({\to }_{T:\infty }\left(e_0\right)\left)\right)(\lambda a{o}_{1:\infty }.U_{\pi }(a{o}_{1:\infty }\left)\right)\left)\right]$

And then, by our earlier arguments when we were doing third-person dynamic to third-person static, we showed

$u_{\sim \pi }^1\left(p{r}_{(A\times O{)}^{\omega }\ast }\right({\to }_{T:\infty }\left(e_0\right)\left)\right)={\delta }_{\pi \cdot e_0}$

So, making that substitution, we have

$={sup}_{\zeta ,U_{\pi },f}{E}_{\pi \sim \zeta }\left[E\right(\lambda e_0.{\delta }_{\pi \cdot e_0}(\lambda a{o}_{:\infty }.U_{\pi }(a{o}_{:\infty }\left)\right)\left)\right]$

Substituting the dirac-delta in, we get

$={sup}_{\zeta ,U_{\pi },f}{E}_{\pi \sim \zeta }\left[E\right(\lambda e_0.U_{\pi }(\pi \cdot e_0)\left)\right]$

Renaming our variables a little bit, we have

$={sup}_{\zeta ,U_{\pi },f}{E}_{\pi \sim \zeta }\left[E\right(\lambda e.U_{\pi }(\pi \cdot e)\left)\right]$

and then, by the causality condition for $E$, this is just $=E\left(f\right)$ and we’re done.

T5.2.4 For 3-dynamic to 3-static to 3-dynamic, our desired result is

${\psi }_T={\bigwedge }_{\pi }(\pi \cdot {)}^{\ast }\left(u_{\sim \pi }^1\left(p{r}_{(A\times O{)}^{\omega }\ast }\right({\psi }_T⋉{\to }_{T:\infty }\left)\right)\right)$

And the proof of this is the exact same as going third-person static to third-person dynamic and back, just use ${\psi }_T$ instead of $E$. Also, ${\to }_F\left(e\right)$ works out as it should.

T5.2.5,6 For translating back and forth between 3-dynamic and 1-dynamic, we observe that both translations keep the initial infradistribution over destinies the same, and our 3-dynamic to 1-dynamic, and 1-dynamic to 3-dynamic proofs verified that the ${\to }_F$ and ${\to }_T$ behave as they should when they go back and forth, so we don’t need to worry about this.

T5.2.7 We’re on the last two! For 1-dynamic to 1-static to 1-dynamic, we want to show that

${\psi }_F={\bigwedge }_{\pi }(\pi \cdot {)}^{\ast }(p{r}_{(A\times O{)}^{\omega }\ast }({\psi }_F⋉{\to }_{F:\infty }^{\pi }))$

Taking the big part, we have

${\bigwedge }_{\pi }(\pi \cdot {)}^{\ast }(p{r}_{(A\times O{)}^{\omega }\ast }({\psi }_F⋉{\to }_{F:\infty }^{\pi })\left)\right(f)$

and undoing the big and, and the pullback via interaction with $\pi$, and merging the sups together as usual, (skipping a few steps we’ve seen several times before) we have

$={sup}_{\zeta ,U_{\pi },f}{E}_{\pi \sim \zeta }\left[p{r}_{(A\times O{)}^{\omega }\ast }\right({\psi }_F⋉{\to }_{F:\infty }^{\pi }\left)\right(\lambda a{o}_{1:\infty }.U_{\pi }\left(a{o}_{1:\infty }\right)\left)\right]$

Undoing the projection, and the semidirect product, we have

$={sup}_{\zeta ,U_{\pi },f}{E}_{\pi \sim \zeta }\left[{\psi }_F\right(\lambda e_0.{\to }_{F:\infty }^{\pi }\left(e_0\right)(\lambda ao{e}_{1:\infty }.U_{\pi }(a{o}_{1:\infty }\left)\right)\left)\right]$

and wrap it up in a projection,

$={sup}_{\zeta ,U_{\pi },f}{E}_{\pi \sim \zeta }\left[{\psi }_F\right(\lambda e_0.p{r}_{(A\times O{)}^{\omega }\ast }\left({\to }_{F:\infty }^{\pi }\right(e_0\left)\right)(\lambda a{o}_{1:\infty }.U_{\pi }(a{o}_{1:\infty }\left)\right)\left)\right]$

and then, because $p{r}_{(A\times O{)}^{\omega }\ast }\left({\to }_{F:\infty }^{\pi }\right(e_0\left)\right)={\delta }_{\pi \cdot e_0}$ because unrolling a policy against a copolicy and recording the actions and observations does that, we have

$={sup}_{\zeta ,U_{\pi },f}{E}_{\pi \sim \zeta }\left[{\psi }_F\right(\lambda e_0.{\delta }_{\pi \cdot e_0}(\lambda a{o}_{1:\infty }.U_{\pi }(a{o}_{1:\infty }\left)\right)\left)\right]$

Then, substituting the value of the dirac-delta in, we get

$={sup}_{\zeta ,U_{\pi },f}{E}_{\pi \sim \zeta }\left[{\psi }_F\right(\lambda e_0.U_{\pi }(\pi \cdot e_0)\left)\right]$

And then, by causality for ${\psi }_F$, this is just

$={\psi }_F\left(f\right)$

and we’re done there.

T5.2.8 Last one, 1-static to 1-dynamic to 1-static. We want to show that

$\Theta \left({\pi }^{\prime }\right)=p{r}_{(A\times O{)}^{\omega }\ast }(\left({\bigwedge }_{\pi }\right(\pi \cdot {)}^{\ast }\left(\Theta \right(\pi \left)\right))⋉{\to }_{F:\infty }^{{\pi }^{\prime }})$

Starting at the complicated side, we have

$p{r}_{(A\times O{)}^{\omega }\ast }(\left({\bigwedge }_{\pi }\right(\pi \cdot {)}^{\ast }\left(\Theta \right(\pi \left)\right))⋉{\to }_{F:\infty }^{{\pi }^{\prime }})\left(U\right)$

and then, undoing the projection,

$=(\left({\bigwedge }_{\pi }\right(\pi \cdot {)}^{\ast }\left(\Theta \right(\pi \left)\right))⋉{\to }_{F:\infty }^{{\pi }^{\prime }})(\lambda e_0,ao{e}_{1:\infty }.U(a{o}_{1:\infty }\left)\right)$

Now, rewriting the semidirect product, we have

$=\left({\bigwedge }_{\pi }\right(\pi \cdot {)}^{\ast }\left(\Theta \right(\pi \left)\right))(\lambda e_0.{\to }_{F:\infty }^{{\pi }^{\prime }}(e_0\left)\right(\lambda ao{e}_{1:\infty }.U\left(a{o}_{1:\infty }\right)\left)\right)$

Rewriting this as a projection, we have

$=\left({\bigwedge }_{\pi }\right(\pi \cdot {)}^{\ast }\left(\Theta \right(\pi \left)\right))(\lambda e_0.p{r}_{(A\times O{)}^{\omega }\ast }({\to }_{F:\infty }^{{\pi }^{\prime }}\left(e_0\right)\left)\right(\lambda a{o}_{1:\infty }.U\left(a{o}_{1:\infty }\right)\left)\right)$

We use the usual trick of this projection of a semidirect product just being the dirac-delta on the copolicy interacting with the policy, and substituting that in to get

$=\left({\bigwedge }_{\pi }\right(\pi \cdot {)}^{\ast }\left(\Theta \right(\pi \left)\right))(\lambda e_0.U({\pi }^{\prime }\cdot e_0\left)\right)$

And then we do the usual unpacking of the intersection and the pullbacks to get:

$={sup}_{\zeta ,U_{\pi },U({\pi }^{\prime }\cdot \bullet )}{E}_{\pi \sim \zeta }\left[\Theta \right(\pi \left)\right(U_{\pi }\left)\right]$

Which, by causality for $\Theta$, is just

$=\Theta \left({\pi }^{\prime }\right)\left(U\right)$

and we’re done with the isomorphisms.

T5.3 The 2 paths from first-person static to third-person dynamic being equivalent is pretty easy since we’ve got identity for two of the legs, and the other two legs are just “intersection of preimages of the $\Theta \left(\pi \right)$”, ie identical, and we’re done!