Proofs Theorem 4

Diffractor

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

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

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

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

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

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

5: $Θ$ is pseudocausal.

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

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

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

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

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

Obviously it produces inframeasures, since $K$ does.

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

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

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

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

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

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

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

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

and then we pack this back up as

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

and lower-semicontinuity has been shown.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Then our proof goal becomes

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

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

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

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

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

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

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

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

and

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

and then unpack to get

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Pull out the constant and combine, to get

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

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

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

and then expands as

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

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

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

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

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

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

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

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

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

Which unpacks as

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

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

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

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

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

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

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

And then we unpack this as an integral.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

as just

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

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

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

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

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

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

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

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

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

First, observe that the functions

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

and

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

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

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

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

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

$= - 2 | | f | |$

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

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

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

and apply our lower-bound to get

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

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

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

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

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

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

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

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

Doing a little bit of regrouping, we have

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

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

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

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

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

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

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

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

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

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

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

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

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

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

converge pointwise in n to the function

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

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

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

And since we have pointwise limiting, this is

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

and then, packing it up,

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

And then, pack it up as

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

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

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

which reexpresses as

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

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

Our net result is

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

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

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

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

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

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

and then this unpacks as

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

Reexpressing the projection, we have:

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

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

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

Which then packs up as

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

and then

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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