This post is an appendix to "Infra-Bayesian physicalism: a formal theory of naturalized induction".

Lemma 1: ${\text{pr}}_{\Gamma \times \Phi }\left({\chi }_{y\in \alpha }\right(s_{\ast }\left(\theta \right)\left)\right)\in \Theta$ occurs for all $s:\Gamma \to \Gamma$ iff, for all $g:\Gamma \times \Phi \to [0,1]$ and $s:\Gamma \to \Gamma$, $\theta (\lambda y\alpha x.{\chi }_{s\left(y\right)\in \alpha }g(s\left(y\right),x\left)\right)\le \Theta (\lambda yx.g(y,x\left)\right)$

This lemma will be implicitly used all over the place, in order to deal with the "presence in the bridge transform" condition algebraically, in terms of function expectations. The bulk of the conditions for a contribution to lie in the bridge transform is this endofunction condition (the support condition is trivial most of the time), so it's advantageous to reformulate it. First-off, we have that $${\text{pr}}_{\Gamma \times \Phi }\left({\chi }_{y\in \alpha }\right(s_{\ast }\left(\theta \right)\left)\right)\in \Theta$$ iff, for all $g:\Gamma \times \Phi \to [0,1]$, we have $${\text{pr}}_{\Gamma \times \Phi }\left({\chi }_{y\in \alpha }\right(s_{\ast }\left(\theta \right)\left)\right)(\lambda yx.g(y,x\left)\right)\le \Theta (\lambda yx.g(y,x\left)\right)$$ By LF-duality for ultradistributions, proved in Less Basic Inframeasure theory. A contribution lies in an ultracontribution set iff its expectations, w.r.t. all functions, are less than or equal to the ultracontribution expectations.

Now, we just need to unpack the left-hand-side into our desired form. Start off with $${\text{pr}}_{\Gamma \times \Phi }\left({\chi }_{y\in \alpha }\right(s_{\ast }\left(\theta \right)\left)\right)(\lambda yx.g(y,x\left)\right)$$ Apply how projections work $$={\chi }_{y\in \alpha }\left(s_{\ast }\right(\theta \left)\right)(\lambda y\alpha x.g(y,x\left)\right)$$ Now, we can move the indicator function into the function we're taking the expectation again, because there's no difference between deleting all measure outside of an event, or taking the expectation of a function that's 0 outside of that event. So, we get $$=s_{\ast }\left(\theta \right)(\lambda y\alpha x.{\chi }_{y\in \alpha }g(y,x\left)\right)$$ Then we use how pushforwards are defined in probability theory. $$=\theta (\lambda y\alpha x.{\chi }_{s\left(y\right)\in \alpha }g(s\left(y\right),x\left)\right)$$ And that's our desired form. So, we've shown that for any particular $s:\Gamma \to \Gamma$, we have ${\text{pr}}_{\Gamma \times \Phi }\left({\chi }_{y\in \alpha }\right(s_{\ast }\left(\theta \right)\left)\right)\in \Theta$ iff, for all $g:\Gamma \times \Phi \to [0,1]$, $$\theta (\lambda y\alpha x.{\chi }_{s\left(y\right)\in \alpha }g(s\left(y\right),x\left)\right)\le \Theta (\lambda yx.g(y,x\left)\right)$$ And so, we get our desired iff statement by going from the iff for one $s$ to the iff for all $s$. $■$

Proposition 2.1: For any $\Gamma$, $\Phi$ and $\Theta \in {\square }^c(\Gamma \times \Phi )$, $\text{Br}\left(\Theta \right)$ exists and satisfies ${\text{pr}}_{\Gamma \times \Phi }\text{Br}\left(\Theta \right)=\Theta$. In particular, if $\Theta \in \square (\Gamma \times \Phi )$ then $\text{Br}\left(\Theta \right)\in \square ({\text{el}}^{\Gamma }\times \Phi )$.

Proof sketch: We'll show that for any particular contribution in $\theta \in \Theta$, there's a contribution ${\theta }^{\ast }$ which lies within $\text{Br}\left(\Theta \right)$ that projects down to equal $\theta$. And then, show the other direction, that any contribution in $\text{Br}\left(\Theta \right)$ lands within $\Theta$ when you project it down. Thus, the projection of $\text{Br}\left(\Theta \right)$ must be $\Theta$ exactly.

For the first direction, given some $\theta \in \Theta$, let ${\theta }^{\ast }:=\theta ⋉(\lambda y.\{y\left\}\right)$. Note that since $\theta \in {\Delta }^c(\Gamma \times \Phi )$, this means that ${\theta }^{\ast }\in {\Delta }^c(\Gamma \times 2^{\Gamma }\times \Phi )$, so the type signatures line up. Clearly, projecting ${\theta }^{\ast }$ down to $\Gamma \times \Phi$ makes $\theta$ again. So that leaves showing that ${\theta }^{\ast }\in \text{Br}\left(\Theta \right)$. Applying Lemma 1, an equivalent way of stating the bridge transform is that it consists precisely of all the ${\theta }^{\prime }\in {\Delta }^c(\Gamma \times 2^{\Gamma }\times \Phi )$ s.t. for all $s:\Gamma \to \Gamma$ and $g:\Gamma \times \Phi \to [0,1]$, $${\theta }^{\prime }(\lambda y\alpha x.{\chi }_{s\left(y\right)\in \alpha }g(s\left(y\right),x\left)\right)\le \Theta (\lambda yx.g(y,x\left)\right)$$ and also, $\text{supp}{\theta }^{\prime }\subseteq {\text{el}}^{\Gamma }\times \Phi$.

Clearly, for our given ${\theta }^{\ast }$, everything works out with the support condition, so that leaves the endofunction condition. Let $s,g$ be arbitrary. $${\theta }^{\ast }(\lambda y\alpha x.{\chi }_{s\left(y\right)\in \alpha }g(s\left(y\right),x\left)\right)=(\theta ⋉(\lambda y.\left\{y\right\}\left)\right)(\lambda y\alpha x.{\chi }_{s\left(y\right)\in \alpha }g(s\left(y\right),x\left)\right)$$ $$=\theta (\lambda yx.{\delta }_{\left\{y\right\}}(\lambda \alpha .{\chi }_{s\left(y\right)\in \alpha }g\left(s\right(y),x)\left)\right)=\theta (\lambda yx.{\chi }_{s\left(y\right)\in \left\{y\right\}}g(s\left(y\right),x\left)\right)$$ $$=\theta (\lambda yx.{\chi }_{s\left(y\right)=y}g(s\left(y\right),x\left)\right)=\theta (\lambda yx.{\chi }_{s\left(y\right)=y}g(y,x\left)\right)\le \theta (\lambda yx.g(y,x\left)\right)$$ $$\le \underset{\theta \in \Theta }{max}\theta (\lambda yx.g(y,x\left)\right)=\Theta (\lambda yx.g(y,x\left)\right)$$ In order, the equalities were unpacking the semidirect product, substituting the dirac-delta in, reexpressing the condition for the indicator function, using that $s\left(y\right)=y$ inside the indicator function, applying monotonicity of $\theta$, using that $\theta \in \Theta$, and then packing up the definition of $\Theta$. And that inequality has been fulfilled, so, yes, ${\theta }^{\ast }$ lies within $\text{Br}\left(\Theta \right)$. Since $\theta$ was arbitrary within $\Theta$, this shows that the projection set is as-big-or-bigger than $\Theta$.

Now to show the reverse direction, that anything in the projection set lies within $\Theta$. For any particular ${\theta }^{\prime }\in \Theta$, remember, it must fulfill, for all $g,s$, that $${\theta }^{\prime }(\lambda y\alpha x.{\chi }_{s\left(y\right)\in \alpha }g(s\left(y\right),x\left)\right)\le \Theta (\lambda yx.g(y,x\left)\right)$$ So, in particular, we can let $s:\Gamma \to \Gamma$ be the identity function, and $g$ be anything, and we'd get $${\theta }^{\prime }(\lambda y\alpha x.{\chi }_{y\in \alpha }g(y,x\left)\right)\le \Theta (\lambda yx.g(y,x\left)\right)$$ And, since ${\theta }^{\prime }$ is in $\text{Br}\left(\Theta \right)$, it's supported on the $(y,\alpha )$ pairs s.t. $y\in \alpha$, so that indicator function drops out of existence, and we get $${\theta }^{\prime }(\lambda y\alpha x.g(y,x\left)\right)\le \Theta (\lambda yx.g(y,x\left)\right)$$ And then this can be written as a projection $${\text{pr}}_{\Gamma \times \Phi }\left({\theta }^{\prime }\right)(\lambda yx.g(y,x\left)\right)\le \Theta (\lambda yx.g(y,x\left)\right)$$ And since this holds for all the various $g$, this means that $${\text{pr}}_{\Gamma \times \Phi }\left({\theta }^{\prime }\right)\in \Theta$$ And we're done with the other direction of things, the projection must be exactly equal to $\Theta$ since projections of contributions in $\text{Br}\left(\Theta \right)$ always land in $\Theta$, and we can surject onto $\Theta$. $■$

Proposition 2.2: Let $X$ be a poset, $\theta ,\eta \in {\Delta }^{c}X$. Then, $\theta ⪯\eta$ if and only if there exists $\kappa :X\to \Delta X$ s.t.: For all $x\in X$, $y\in \text{supp}\kappa \left(x\right)$: $x\le y$. ${\kappa }_{\ast }\theta \le \eta$

Vanessa proved this one, with a very nice proof involving the max-flow min-cut theorem.

Make the following directed graph: The nodes are the elements of $\left\{s\right\}\cup \left\{t\right\}\cup X\times \{0,1\}$. Basically, two copies of the finite poset $X$, a source node $s$, and a sink node $t$. $x$ will be used to denote a variable from $X$, while a subscript of 0 or 1 denotes that the 0 or 1 version of that $x$, respectively.

As for the edges, there is an edge from $s$ to every point in $X_0$. And an edge from every point in $X_1$ to $t$. And, for some $x_0\in X_0$ and $y_1\in X_1$, there's an edge iff $x\le y$. The capacities of the edges are, for all $x\in X$, $c_{s,x_0}:=\theta \left(x\right)$, and for all $x\in X$, $c_{x_1,t}:=\eta \left(x\right)$, and for $x,y\in X$ s.t. $x\le y$, $c_{x_0,y_1}:=\infty$.

To work up to applying min-cut max-flow, we must show that the cut of all the edges between $s$ and $X_0$ is a min-cut of the network.

Remember, all cuts are induced by partitions of the nodes into two sets, $S$ and $T$, where $S$ includes the source $s$ and $T$ includes the sink $t$. And the value of a cut is $$c(S,T)=\sum _{a\in S,b\in T}{c}_{a,b}=\sum _{x_0\in T}{c}_{s,x_0}+\sum _{x_0\in S,y_1\in T:x\le y}{c}_{x_0,y_1}+\sum _{y_1\in S}{c}_{y_1,t}$$ Implicitly converting both of the following sets to be subsets of $X$, we have $(S\cap X_1)\supseteq (S\cap X_0{)}^{\uparrow }$ for any non-infinite cut. Why? Well, if it was false, then there'd be some $y\ge x$ where $x_0\in S$, and yet $y_1\notin S$. So $y_1\in T$. Then, the cost of the cut would include $c_{x_0,y_1}=\infty$, contradiction. So, now, we have that for any non-infinite cut, $$c(S,T)=\sum _{a\in S,b\in T}{c}_{a,b}=\sum _{x_0\in T}{c}_{s,x_0}+\sum _{y_1\in S}{c}_{y_1,t}$$ and $(S\cap X_1)\supseteq (S\cap X_0{)}^{\uparrow }$ holds.

Now, we'll change our cut. Given some cut $(S,T)$, let our new cut $(S^{\prime },T^{\prime })$ be defined as $S^{\prime }:=\left\{s\right\}\cup \left(\right(S\cap X_0{)}^{\uparrow }\times \{0,1\})$ (which still respects that superset property listed above since both sets would be the same), and $T^{\prime }$ be the complement. Letting some stuff cancel out, we get $$c(S,T)-c(S^{\prime },T^{\prime })=\sum _{x_0\in T}{c}_{s,x_0}+\sum _{y_1\in S}{c}_{y_1,t}-\sum _{x_0\in T^{\prime }}{c}_{s,x_0}-\sum _{y_1\in S^{\prime }}{c}_{y_1,t}$$ $$=\sum _{x_0\in T/T^{\prime }}{c}_{s,x_0}+\sum _{y_1\in S/S^{\prime }}{c}_{y_1,t}-\sum _{x_0\in T^{\prime }/T}{c}_{s,x_0}-\sum _{y_1\in S^{\prime }/S}{c}_{y_1,t}$$ Now, because $S^{\prime }\cap X_1=(S\cap X_0{)}^{\uparrow }\times \{1\}\subseteq S\cap X_1$ by that subset property, it means that there's no $y_1\in S^{\prime }/S$, so we get $$=\sum _{x_0\in T/T^{\prime }}{c}_{s,x_0}+\sum _{y_1\in S/S^{\prime }}{c}_{y_1,t}-\sum _{x_0\in T^{\prime }/T}{c}_{s,x_0}$$ As for that other minus term, we have that $S^{\prime }\cap X_0=(S\cap X_0{)}^{\uparrow }\times \{0\}\supseteq S\cap X_0$ by how it was defined, so $T^{\prime }\cap X_0\subseteq T\cap X_0$, so that other minus term is 0, and we get $$=\sum _{x_0\in T/T^{\prime }}{c}_{s,x_0}+\sum _{y_1\in S/S^{\prime }}{c}_{y_1,t}\ge 0$$ Rearranging this a bit, we have $c(S,T)\ge c(S^{\prime },T^{\prime })$.

And now we'll show that $c(S^{\prime },T^{\prime })$ is underscored by $c\left(\right\{s\},(X\times \{0,1\})\cup \{t\left\}\right)$. Let's go. We have $$c(S^{\prime },T^{\prime })-c\left(\right\{s\},(X\times \{0,1\})\cup \{t\left\}\right)$$ $$=\sum _{x_0\in T^{\prime }}{c}_{s,x_0}+\sum _{y_1\in S^{\prime }}{c}_{y_1,t}-\sum _{x_0\in (X\times \{0,1\left\}\right)\cup \left\{t\right\}}{c}_{s,x_0}-\sum _{y_1\in \left\{s\right\}}{c}_{y_1,t}$$ This simplifies a bit as $$=\sum _{x_0\in T^{\prime }}{c}_{s,x_0}+\sum _{y_1\in S^{\prime }}{c}_{y_1,t}-\sum _{x_0\in X_0}{c}_{s,x_0}$$ This can be rewritten a bit as $$=(\sum _{x_0\in X_0}{c}_{s,x_0}-\sum _{x_0\in S^{\prime }}{c}_{s,x_0})+\sum _{y_1\in S^{\prime }}{c}_{y_1,t}-\sum _{x_0\in X_0}{c}_{s,x_0}$$ $$=\sum _{y_1\in S^{\prime }}{c}_{y_1,t}-\sum _{x_0\in S^{\prime }}{c}_{s,x_0}$$ And then, using what $S^{\prime }$ is defined as, we can get $$=\sum _{y\in (S\cap X_0{)}^{\uparrow }}{c}_{y_1,t}-\sum _{x\in (S\cap X_0{)}^{\uparrow }}{c}_{s,x_0}$$ and using what the costs are, it's $$=\sum _{y\in (S\cap X_0{)}^{\uparrow }}\eta \left(y\right)-\sum _{x\in (S\cap X_0{)}^{\uparrow }}\theta \left(y\right)$$ $$=\eta \left(\right(S\cap X_0{)}^{\uparrow })-\theta ((S\cap X_0{)}^{\uparrow })\ge 0$$ This holds because $\theta ⪯\eta$ and the indicator function for $(S\cap X_0{)}^{\uparrow }$ is monotone. And so, we get $c(S^{\prime },T^{\prime })\ge c\left(\right\{s\},(X\times \{0,1\})\cup \{t\left\}\right)$. And we previously showed that $c(S,T)\ge c(S^{\prime },T^{\prime })$. So, this means that the cut around $s$ is a minimal cut, it underscores all other cuts.

By the max-flow min-cut theorem, there's a way of having stuff flow from $s$ to $t$ that saturates the capacities of all the edges that are cut. $f_{x_0,y_1}$ will be used to denote the flow from $x_0$ to $y_1$ according to this max-flow way. Let's finish things up.

Define $\kappa :X\to \Delta X$ as follows. For some $x$, if $f_{s,x_0}>0$, then $$\kappa \left(x\right)\left(y\right):=\frac{f_{x_0,y_1}}{f_{s,x_0}}$$ If $f_{s,x_0}=0$, let $\kappa \left(x\right)$ be any probability distribution on $x^{\uparrow }$. Note that $\kappa \left(x\right)$ is always a probability distribution supported on $x^{\uparrow }$, by fiat if $f_{s,x_0}=0$, and otherwise, $$\sum _{y\in X}\kappa \left(x\right)\left(y\right)=\sum _{y\in X}\frac{f_{x_0,y_1}}{f_{s,x_0}}=\frac{f_{s,x_0}}{f_{s,x_0}}=1$$ This is because, the flow out of $x_0$ must equal the flow into $x_0$ from the source. And $\kappa \left(x\right)$ is supported on $x^{\uparrow }$ because the only edges out of $x_0$ go to $y_1$ where $y\ge x$. Now that we've got this demonstrated, we'll show our desired inequality. Fix an arbitrary $y$. We have $${\kappa }_{\ast }\left(\theta \right)\left(y\right)=\sum _{x\in X}\theta \left(x\right)\cdot \kappa \left(x\right)\left(y\right)=\sum _{x\in X}{c}_{s,x_0}\cdot \frac{f_{x_0,y_1}}{f_{s,x_0}}$$ And then we use that all the capacities of the edges cut in the min-cut are saturated according to the max-flow plan, so $c_{s,x_0}=f_{s,x_0}$, and we have $$=\sum _{x\in X}{f}_{s,x_0}\cdot \frac{f_{x_0,y_1}}{f_{s,x_0}}$$ Now, if $f_{s,x_0}=0$, then because the flow in equals the flow out, that means that $f_{x_0,y_1}=0$, and otherwise we can cancel out, so we can rewrite as $$=\sum _{x\in X}{f}_{x_0,y_1}=f_{y_1,t}\le c_{y_1,t}=\eta \left(y\right)$$ Where the first equality came from flow in equals flow out, the inequality came from the flow plan respecting the capacity of the paths, and the equality came from how the capacities were defined. So, for all $y\in X$, we have ${\kappa }_{\ast }\left(\theta \right)\left(y\right)\le \eta \left(y\right)$ so we have ${\kappa }_{\ast }\left(\theta \right)\le \eta$.

For the reverse direction, if there's some $\kappa :X\to \Delta X$ s.t $\kappa \left(x\right)$ is supported on $x^{\uparrow }$ s.t. ${\kappa }_{\ast }\left(\theta \right)\le \eta$, then for any monotone function $f$, we have $$\eta \left(f\right)\ge {\kappa }_{\ast }\left(\theta \right)\left(f\right)=\theta (\lambda x.\kappa (x\left)\right(f\left)\right)$$ And then we use that, since $\kappa \left(x\right)$ is supported on $x^{\uparrow }$, and $f$ is monotone, $f\left(x\right)$ is less than or equal to the expectation of $f$ w.r.t $\kappa \left(x\right)$ (remember, for $\kappa \left(x\right)$ you have a 100 percent chance of drawing something at-or-above $x$, which guarantees that f of whatever you picked is above $f\left(x\right)$). And so, we get $$\ge \theta \left(f\right)$$ And since this holds for every monotone $f$, we have $\theta ⪯\eta$.$■$

Proposition 2.3: Let $X$ be a poset, $\theta ,\eta \in {\Delta }^{c}X$. Then, $\theta ⪯\eta$ if and only if there exists $\kappa :X\to \Delta X$ s.t. For all $x\in X$, $y\in \text{supp}\kappa \left(x\right)$: $x\ge y$. $\theta \le {\kappa }_{\ast }\eta$

Proof: Because $\theta ⪯\eta$, we can get a maximum flow in exactly the same way as Proposition 2.2. Then, just flip the direction of all flows, which will be denoted by swapping the order of the subscripts. Now, define $$\kappa \left(y\right)\left(x\right):=\frac{f_{y_1,x_0}}{f_{t,y_1}}$$ And, again, if it's 0, it should be an arbitrary probability distribution supported on $y\downarrow$. Note that $\kappa \left(y\right)$ is always a probability distribution supported on $y\downarrow$, by fiat if $f_{t,y_1}^{\prime }=0$, and otherwise, $$\sum _{x\in X}\kappa \left(y\right)\left(x\right)=\sum _{x\in X}\frac{f_{y_1,x_0}}{f_{t,y_1}}=\frac{f_{t,y_1}}{f_{t,y_1}}=1$$ This is because, the flow out of $y_1$ must equal the flow into $y_1$ from the source $t$ (the old sink). And $\kappa \left(y\right)$ is supported on $y\downarrow$ because the only edges out of $y_1$ go to $x_0$ where $y\ge x$. Now that we've got this demonstrated, we'll show our desired inequality. Fix an arbitrary $x$. We have $${\kappa }_{\ast }\left(\eta \right)\left(x\right)=\sum _{y\in X}\eta \left(y\right)\cdot \kappa \left(y\right)\left(x\right)=\sum _{y\in X}{c}_{y_1,t}\cdot \frac{f_{y_1,x_0}}{f_{t,y_1}}$$ Then use that $c_{y_1,t}\ge f_{t,y_1}$ (because even with the flow reversed, the flow through a path must be less than or the same as the capacity. Accordingly, we get $$\ge \sum _{y\in X}{f}_{y_1,x_0}=f_{x_0,s}=c_{s,x_0}=\theta \left(x\right)$$ And we're done, inequality established, using definitions and the flow saturating all the paths out of $s$.

So, for all $x\in X$, we have ${\kappa }_{\ast }\left(\eta \right)\left(x\right)\ge \theta \left(x\right)$ so we have ${\kappa }_{\ast }\left(\eta \right)\ge \theta$.

For the reverse direction, if there's some $\kappa :X\to \Delta X$ s.t $\kappa \left(y\right)$ is supported on $y\downarrow$ s.t. ${\kappa }_{\ast }\left(\eta \right)\ge \theta$, then for any monotone function $f$, we have $$\theta \left(f\right)\le {\kappa }_{\ast }\left(\eta \right)\left(f\right)=\eta (\lambda x.\kappa (x\left)\right(f\left)\right)$$ And then we use that, since $\kappa \left(x\right)$ is supported on $x\downarrow$, and $f$ is monotone, $f\left(x\right)$ is greater than or equal to the expectation of $f$ w.r.t $\kappa \left(x\right)$ (remember, for $\kappa \left(x\right)$ you have a 100 percent chance of drawing something at-or-below $x$, which guarantees that f of whatever you picked is below $f\left(x\right)$). And so, we get $$\le \eta \left(f\right)$$ And since this holds for every monotone $f$, we have $\theta ⪯\eta$. $■$

Proposition 2.4: For any $\Gamma$, $\Phi$ and $\Theta \in {\square }^c(\Gamma \times \Phi )$,$\text{Br}\left(\Theta \right)$ is downwards closed w.r.t. the induced order on ${\Delta }^c({\text{el}}^{\Gamma }\times \Phi )$. That is, if $\theta \in \text{Br}\left(\Theta \right)$ and $\eta ⪯\theta$ then $\eta \in \text{Br}\left(\Theta \right)$.

Remember, the condition for some $\theta$ to lie in $\text{Br}\left(\Theta \right)$ is that it be supported on ${\text{el}}^{\Gamma }$, and that, for all $s:\Gamma \to \Gamma$, and $g:\Gamma \times \Phi \to [0,1]$, $$\theta (\lambda y\alpha x.{\chi }_{s\left(y\right)\in \alpha }g(s\left(y\right),x\left)\right)\le \Theta (\lambda yx.g(y,x\left)\right)$$ So, given that $\eta ⪯\theta$ (lower score for all monotone functions) we'll show that $\eta$ fulfills both conditions. The support thing is taken care of by $\eta \in {\Delta }^c({\text{el}}^{\Gamma }\times \Phi )$. As for the other one, we have $$\eta (\lambda y\alpha x.{\chi }_{s\left(y\right)\in \alpha }g(s\left(y\right),x\left)\right)\le \theta (\lambda y\alpha x.{\chi }_{s\left(y\right)\in \alpha }g(s\left(y\right),x\left)\right)$$ $$\le \Theta (\lambda yx.g(y,x\left)\right)$$ That inequality occurs because as you make $\alpha$ larger, ie, go up in the partial ordering, the value assigned to the relevant point increases since $s\left(y\right)\in \alpha$ is more likely now, so the function value increases from 0 to something that may be greater than 0. So, it's a monotone function, and we then use that $\eta ⪯{\theta }^{\prime }$. $■$

Proposition 2.5: Consider a finite set $X$, ${\varphi }_{?}\in \Delta X$, ${\varphi }_{!}:\{0,1\}\to \Delta X$, $p\in [0,1]$ and $\varphi :=(1-p){\varphi }_{?}+p{\varphi }_{!}$. Then, $p\ge {\text{d}}_{\text{TV}}\left(\varphi \right(0),\varphi (1\left)\right)$. Conversly, consider any $\varphi :\{0,1\}\to \Delta X$. Then, there exist ${\varphi }_{?}\in \Delta X$ and ${\varphi }_{!}:\{0,1\}\to \Delta X$ s.t. $\varphi =(1-p){\varphi }_{?}+p{\varphi }_{!}$ for $p:={\text{d}}_{\text{TV}}\left(\varphi \right(0),\varphi (1\left)\right)$.

Ok, so let $f$ be some arbitrary function $X\to [0,1]$. We have an alternate characterization of the total variation distance as $${\text{d}}_{\text{TV}}\left(\varphi \right(0),\varphi (1\left)\right):=\underset{f\in X\to [0,1]}{sup}|\varphi \left(0\right)\left(f\right)-\varphi \left(1\right)\left(f\right)|$$ And then from there we can go $$=\underset{f\in X\to [0,1]}{sup}|\left(\right(1-p\left){\varphi }_{?}\right(f)+p{\varphi }_{!}(0\left)\right(f\left)\right)-\left(\right(1-p\left){\varphi }_{?}\right(f)+p{\varphi }_{!}(1\left)\right(f\left)\right)|$$ $$=\underset{f\in X\to [0,1]}{sup}|p{\varphi }_{!}\left(0\right)\left(f\right)-p{\varphi }_{!}\left(1\right)\left(f\right)|$$ $$=p\underset{f\in X\to [0,1]}{sup}|{\varphi }_{!}\left(0\right)\left(f\right)-{\varphi }_{!}\left(1\right)\left(f\right)|$$ $$=p{\text{d}}_{\text{TV}}\left({\varphi }_{!}\right(0),{\varphi }_{!}(1\left)\right)$$ And since $p\ge p{\text{d}}_{\text{TV}}\left({\varphi }_{!}\right(0),{\varphi }_{!}(1\left)\right)$, we have $p\ge {\text{d}}_{\text{TV}}\left(\varphi \right(0),\varphi (1\left)\right)$ and are done.

Conversely, let the value of $p$ be $1-\left(\varphi \right(0)\wedge \varphi (1\left)\right)\left(1\right)$, and ${\varphi }_{?}$ be $\frac{1}{(1-p)}\left(\varphi \right(0)\wedge \varphi (1\left)\right)$. It is clear that this is a probability distribution because of how $p$ was defined. The $\wedge$ is the minimum/common overlap of the two probability distributions. Then, let ${\varphi }_{!}\left(0\right)=\frac{1}{p}\left(\varphi \right(0)-(\varphi \left(0\right)\wedge \varphi \left(1\right)\left)\right)$, and similar for the 1. Well, as long as $p>0$. If $p=0$, it can be any probability distribution you want. It's a probability distribution because $${\varphi }_{!}\left(0\right)\left(1\right)=\frac{1}{p}\left(\varphi \right(0\left)\right(1)-(\varphi \left(0\right)\wedge \varphi \left(1\right)\left)\right(1\left)\right)=\frac{1}{p}(1-(\varphi \left(0\right)\wedge \varphi \left(1\right)\left)\right(1\left)\right)$$ $$=\frac{1-\left(\varphi \right(0)\wedge \varphi (1\left)\right)\left(1\right)}{1-\left(\varphi \right(0)\wedge \varphi (1\left)\right)\left(1\right)}=1$$ And since $p>0$, everything works out. Now we just need to show that these add up to make $\varphi$ and that $p$ is the same as the total variation distance. $$\varphi \left(0\right)=\left(\varphi \right(0)\wedge \varphi (1\left)\right)+\varphi \left(0\right)-\left(\varphi \right(0)\wedge \varphi (1\left)\right)$$ $$=(1-p)\frac{1}{(1-p)}\left(\varphi \right(0)\wedge \varphi (1\left)\right)+p\frac{1}{p}\left(\varphi \right(0)-(\varphi \left(0\right)\wedge \varphi \left(1\right)\left)\right)=(1-p){\varphi }_{?}+p{\varphi }_{!}\left(0\right)$$ And this works symmetrically for $\varphi \left(1\right)$, showing that we indeed have equality. As for showing that $p$ is the total variation distance, referring back to what we've already proved, we have $${\text{d}}_{\text{TV}}\left(\varphi \right(0),\varphi (1\left)\right)=p{\text{d}}_{\text{TV}}\left({\varphi }_{!}\right(0),{\varphi }_{!}(1\left)\right)$$ And now, since ${\varphi }_{!}\left(0\right)=\varphi \left(0\right)-\left(\varphi \right(0)\wedge \varphi (1\left)\right)$ and ${\varphi }_{!}\left(1\right)=\varphi \left(1\right)-\left(\varphi \right(0)\wedge \varphi (1\left)\right)$, the supports of these two probability distributions are disjoint, which implies that the total variation distance is 1, so we have ${\text{d}}_{\text{TV}}\left(\varphi \right(0),\varphi (1\left)\right)=p$.

Proposition 2.6: Consider any $\Phi$ and $\varphi :\{0,1\}\to \Delta \Phi$. Denote $U:=\{0,1\}\times \left\{\right\{0,1\left\}\right\}\times \Phi$ (the event ``program is unrealized''). Let $\Lambda :=\text{Br}({\top }_{\{0,1\}}⋉\varphi )$. Then, $$\Lambda \left({\chi }_U\right)=1-{\text{d}}_{\text{TV}}\left(\varphi \right(0),\varphi (1\left)\right)$$

This will take some work to establish. One direction, showing that the bridge transform value exceeds the total variation distance value, is fairly easy. As for the other direction, it'll take some work. Let's begin. $$\Lambda \left({\chi }_U\right)=\text{Br}({\top }_{\{0,1\}}⋉\varphi )\left({\chi }_U\right)=\text{Br}({\top }_{\{0,1\}}⋉\varphi )(\lambda y\alpha x.{\chi }_{\alpha =\{0,1\}})$$ $$=\underset{\theta \in \text{Br}({\top }_{\{0,1\}}⋉\varphi )}{max}{\theta }^{\prime }(\lambda y\alpha x.{\chi }_{\alpha =\{0,1\}})$$ We'll make a particular contribution ${\theta }^{\ast }$. It is defined as $${\delta }_0\times \left(\varphi \right(0)-\varphi (0)\wedge \varphi (1\left)\right)\times {\delta }_{\left\{0\right\}}+{\delta }_0\times \left(\varphi \right(0)\wedge \varphi (1\left)\right)\times {\delta }_{\{0,1\}}$$ Or, put another way, restricting to $0,\left\{0\right\}$, it's $\varphi \left(0\right)-\varphi \left(0\right)\wedge \varphi \left(1\right)$, and conditioning on $0,\{0,1\}$, it's $\varphi \left(0\right)\wedge \varphi \left(1\right)$. So, for a given $s:\{0,1\}\to \{0,1\}$, we have $${\theta }^{\ast }(\lambda y\alpha x.{\chi }_{s\left(y\right)\in \alpha }g(s\left(y\right),x\left)\right)$$ $$=({\delta }_0\times (\varphi \left(0\right)-\varphi \left(0\right)\wedge \varphi \left(1\right))\times {\delta }_{\left\{0\right\}}+{\delta }_0\times (\varphi \left(0\right)\wedge \varphi \left(1\right))\times {\delta }_{\{0,1\}})(\lambda y\alpha x.{\chi }_{s\left(y\right)\in \alpha }g(s\left(y\right),x\left)\right)$$ $$=({\delta }_0\times (\varphi \left(0\right)-\varphi \left(0\right)\wedge \varphi \left(1\right))\times {\delta }_{\left\{0\right\}})(\lambda y\alpha x.{\chi }_{s\left(y\right)\in \alpha }g(s\left(y\right),x\left)\right)$$ $$+({\delta }_0\times (\varphi \left(0\right)\wedge \varphi \left(1\right))\times {\delta }_{\{0,1\}})(\lambda y\alpha x.{\chi }_{s\left(y\right)\in \alpha }g(s\left(y\right),x\left)\right)$$ $$=\left(\varphi \right(0)-\varphi (0)\wedge \varphi (1\left)\right)(\lambda x.{\chi }_{s\left(0\right)\in \left\{0\right\}}g(s\left(0\right),x\left)\right)+\left(\varphi \right(0)\wedge \varphi (1\left)\right)(\lambda x.{\chi }_{s\left(0\right)\in \{0,1\}}g(s\left(0\right),x\left)\right)$$ Now, we'll go through two exhaustive possibilities for what $s$ could be. If it maps 0 to 0, then it's $$=\left(\varphi \right(0)-\varphi (0)\wedge \varphi (1\left)\right)(\lambda x.{\chi }_{0\in \left\{0\right\}}g(0,x\left)\right)+\left(\varphi \right(0)\wedge \varphi (1\left)\right)(\lambda x.{\chi }_{0\in \{0,1\}}g(0,x\left)\right)$$ $$=\left(\varphi \right(0)-\varphi (0)\wedge \varphi (1\left)\right)(\lambda x.g(0,x\left)\right)+\left(\varphi \right(0)\wedge \varphi (1\left)\right)(\lambda x.g(0,x\left)\right)$$ $$=\varphi \left(0\right)(\lambda x.g(0,x\left)\right)\le \underset{y\in \{0,1\}}{max}\varphi \left(y\right)(\lambda x.g(y,x\left)\right)$$ $$={\top }_{\{0,1\}}(\lambda y.\varphi (y\left)\right(\lambda x.g(y,x))=({\top }_{\{0,1\}}⋉\varphi \left)\right(\lambda yx.g(y,x))$$ And our desired inequality is established. If $s$ maps 0 to 1, then it's $$=\left(\varphi \right(0)-\varphi (0)\wedge \varphi (1\left)\right)(\lambda x.{\chi }_{1\in \left\{0\right\}}g(1,x\left)\right)+\left(\varphi \right(0)\wedge \varphi (1\left)\right)(\lambda x.{\chi }_{1\in \{0,1\}}g(1,x\left)\right)$$ $$=\left(\varphi \right(0)\wedge \varphi (1\left)\right)(\lambda x.g(1,x\left)\right)\le \varphi \left(1\right)(\lambda x.g(1,x\left)\right)$$ $$\le \underset{y\in \{0,1\}}{max}\varphi \left(y\right)(\lambda x.g(y,x\left)\right)=({\top }_{\{0,1\}}⋉\varphi )(\lambda yx.g(y,x\left)\right)$$ And that is taken care of. So, our ${\theta }^{\ast }$ lies in $\text{Br}({\top }_{\{0,1\}}⋉\varphi )$.

Now, where were we? Ah right, we were at $$\Lambda \left({\chi }_U\right)=\underset{\theta \in \text{Br}({\top }_{\{0,1\}}⋉\varphi )}{max}\theta (\lambda y\alpha x.{\chi }_{\alpha =\{0,1\}})$$ But now we can continue with $$\ge {\theta }^{\ast }(\lambda y\alpha x.{\chi }_{\alpha =\{0,1\}})$$ Which unpacks as $$=({\delta }_0\times (\varphi \left(0\right)-\varphi \left(0\right)\wedge \varphi \left(1\right))\times {\delta }_{\left\{0\right\}}+{\delta }_0\times (\varphi \left(0\right)\wedge \varphi \left(1\right))\times {\delta }_{\{0,1\}})(\lambda y\alpha x.{\chi }_{\alpha =\{0,1\}})$$ $$=({\delta }_0\times (\varphi \left(0\right)-\varphi \left(0\right)\wedge \varphi \left(1\right))\times {\delta }_{\left\{0\right\}})(\lambda y\alpha x.{\chi }_{\alpha =\{0,1\}})$$ $$+({\delta }_0\times (\varphi \left(0\right)\wedge \varphi \left(1\right))\times {\delta }_{\{0,1\}})(\lambda y\alpha x.{\chi }_{\alpha =\{0,1\}})$$ $$=\left(\varphi \right(0)-\varphi (0)\wedge \varphi (1\left)\right)(\lambda x.{\chi }_{\left\{0\right\}=\{0,1\}})+\left(\varphi \right(0)\wedge \varphi (1\left)\right)(\lambda x.{\chi }_{\{0,1\}=\{0,1\}})$$ $$=\left(\varphi \right(0)\wedge \varphi (1\left)\right)\left(1\right)$$ And then, the value of the overlap between two distributions is $1-{\text{d}}_{\text{TV}}\left(\varphi \right(0),\varphi (1\left)\right)$. So, we've shown one direction, we have $$\Lambda \left({\chi }_U\right)\ge 1-{\text{d}}_{\text{TV}}\left(\varphi \right(0),\varphi (1\left)\right)$$ In the other direction of the equality we're trying to prove, we need to constrain what $\theta$ might be. Starting off with what we definitely know, we have $$\Lambda \left({\chi }_U\right)=\underset{\theta \in \text{Br}({\top }_{\{0,1\}}⋉\varphi )}{max}\theta (\lambda y\alpha x.{\chi }_{\alpha =\{0,1\}})$$ Now it's time to show that for any $\theta \in \text{Br}({\top }_{\{0,1\}}⋉\varphi )$, that the measure on $\alpha =\{0,1\}$ can't be too high. Specifically, to proceed further, we'll need to show that $$\forall x^{\prime }\in \Phi :\theta (\lambda y\alpha x.{\chi }_{x=x^{\prime }\wedge \alpha =\{0,1\}})\le \left(\varphi \right(0)\wedge \varphi (1\left)\right)(\lambda x.{\chi }_{x=x^{\prime }})$$ Time to establish it. On $x^{\prime }$, either $\varphi \left(0\right)\left(x^{\prime }\right)\ge \varphi \left(1\right)\left(x^{\prime }\right)$, or vice-versa. Without loss of generality, assume that it's $\varphi \left(0\right)\left(x^{\prime }\right)$ that's lower.

Then, let $s$ be the constant-0 function, and $g(0,x^{\prime })$ be 1, and 0 everywhere else. Then, we have $$\theta (\lambda y\alpha x.{\chi }_{x=x^{\prime }\wedge \alpha =\{0,1\}})\le \theta (\lambda y\alpha x.{\chi }_{s\left(y\right)\in \alpha }g(s\left(y\right),x\left)\right)$$ $$\le ({\top }_{\{0,1\}}⋉\varphi )(\lambda yx.g(y,x\left)\right)=({\top }_{\{0,1\}}⋉\varphi )(\lambda yx.{\chi }_{y=0\wedge x=x^{\prime }})$$ $$=\underset{y\in \{0,1\}}{max}\varphi \left(y\right)(\lambda x.{\chi }_{y=0\wedge x=x^{\prime }})=\varphi \left(0\right)(\lambda x.{\chi }_{x=x^{\prime }})=\varphi \left(0\right)\left(x^{\prime }\right)$$ $$=\left(\varphi \right(0)\wedge \varphi (1\left)\right)\left(x^{\prime }\right)$$ Just abbreviating, using that $\theta$ lies in the bridge transform, deabbreviating with what $g$ is, unpacking things a little bit and canceling out. At the end we used that $\varphi \left(0\right)\left(x^{\prime }\right)\le \varphi \left(1\right)\left(x^{\prime }\right)$.

Ok, so, now that we've established the key fact that $$\forall x^{\prime }\in \Phi :\theta (\lambda y\alpha x.{\chi }_{x=x^{\prime }\wedge \alpha =\{0,1\}})\le \left(\varphi \right(0)\wedge \varphi (1\left)\right)(\lambda x.{\chi }_{x=x^{\prime }})$$ We can resume our work. We were previously at $$=\underset{\theta \in \text{Br}({\top }_{\{0,1\}}⋉\varphi )}{max}\theta (\lambda y\alpha x.{\chi }_{\alpha =\{0,1\}})$$ and we can proceed to $$=\underset{\theta \in \text{Br}({\top }_{\{0,1\}}⋉\varphi )}{max}\sum _{x^{\prime }\in \Phi }\theta (\lambda y\alpha x.{\chi }_{x=x^{\prime }\wedge \alpha =\{0,1\}})$$ and from there, using the inequality we proved, proceed to $$\le \sum _{x^{\prime }\in \Phi }\left(\varphi \right(0)\wedge \varphi (1\left)\right)(\lambda x.{\chi }_{x=x^{\prime }})=\left(\varphi \right(0)\wedge \varphi (1\left)\right)\left(1\right)=1-{\text{d}}_{\text{TV}}\left(\varphi \right(0),\varphi (1\left)\right)$$ And we're done, we established that it's an upper bound as well a lower bound, so we have equality. $■$

Lemma 2: If there's a function $h:\Phi \to 2^{\Gamma }$ and $\Theta (\lambda yx.{\chi }_{y\notin h\left(x\right)})=0$, then for all $\theta \in \text{Br}\left(\Theta \right)$, $\theta$ is supported on the set $\{\alpha ,x|\alpha \subseteq h(x\left)\right\}$.

Assume that the conclusion is false, that there is some nonzero probability of drawing a $x^{\ast },{\alpha }^{\ast }$ pair where ${\alpha }^{\ast }⊈h\left(x^{\ast }\right)$. In particular, there must be some special $y^{\ast }\in \Gamma$ value that witnesses that ${\alpha }^{\ast }$ isn't a subset, by $y^{\ast }\in {\alpha }^{\ast }$ and $y^{\ast }\notin h\left(x^{\ast }\right)$. Remember that for all $s:\Gamma \to \Gamma$ and $g:\Gamma \times \Phi \to [0,1]$, that since $\theta \in \text{Br}\left(\Theta \right)$, we have $$\theta (\lambda y\alpha x.{\chi }_{s\left(y\right)\in \alpha }g(s\left(y\right),x\left)\right)\le \Theta (\lambda yx.g(y,x\left)\right)$$ Now, in particular, let $g:={\chi }_{y\notin h\left(x\right)}$, and $s$ be the constant function that maps everything to $y^{\ast }$. Then, this turns into $$0<\theta (\lambda y\alpha x.{\chi }_{y^{\ast }\in \alpha }{\chi }_{y^{\ast }\notin h\left(x\right)})\le \Theta (\lambda yx.{\chi }_{y\notin h\left(x\right)})=0$$ which is impossible. The equality as the end was our starting assumption. The middle inequality was just specializing our inequality to a particular pair of functions. And it's greater than 0 because there's a nonzero probability of drawing $x^{\ast },{\alpha }^{\ast }$. And $y^{\ast }$ was selected to lie in ${\alpha }^{\ast }$ and outside of $h\left(x^{\ast }\right)$, so there's a nonzero probability of getting a nonzero value. Therefore, the result follows. $■$

Lemma 3: For any $s:\Gamma \to \Gamma$, and $\Theta :{\square }^c(\Gamma \times \Phi )$, if $\theta \in \text{Br}\left(\Theta \right)$, then ${\chi }_{{\text{el}}^{\Gamma }}\left(s_{\ast }\right({\theta }^{\prime }\left)\right)\in \text{Br}\left(\Theta \right)$.

So, the support condition is trivially fulfilled, because we're restricting to the event $y\in \alpha$. That just leaves the endofunction condition. Let $s^{\prime }:\Gamma \to \Gamma$ be arbitrary, and $g:\Gamma \times \Phi \to [0,1]$ be arbitrary. Then we have $${\chi }_{{\text{el}}^{\Gamma }}\left(s_{\ast }\right(\theta \left)\right)(\lambda y\alpha x.{\chi }_{s^{\prime }\left(y\right)\in \alpha }g(s^{\prime }\left(y\right),x\left)\right)=s_{\ast }\left(\theta \right)(\lambda y\alpha x.{\chi }_{y\in \alpha \wedge s^{\prime }\left(y\right)\in \alpha }g(s^{\prime }\left(y\right),x\left)\right)$$ $$\le s_{\ast }\left(\theta \right)(\lambda y\alpha x.{\chi }_{s^{\prime }\left(y\right)\in \alpha }g(s^{\prime }\left(y\right),x\left)\right)=\theta (\lambda y\alpha x.{\chi }_{s^{\prime }\left(s\right(y\left)\right)\in \alpha }g(s^{\prime }\left(s\right(y\left)\right),x\left)\right)$$ And, since $s^{\prime }\circ s:\Gamma \to \Gamma$, we can use that $\theta \in \text{Br}\left(\Theta \right)$ to get $$\le \Theta (\lambda yx.g(y,x\left)\right)$$ And we're done, we've established that our modified version of $\theta$ remains in $\text{Br}\left(\Theta \right)$. $■$

Proposition 2.7: If $X$ is a poset and $\Theta \in {\square }^{c}X$, then ${\Theta }^{\downarrow }$ will denote downward closure of $\Theta$. For any $\Gamma$, $\Phi$ and $\Theta \in {\square }^c(\Gamma \times \Phi )$ if $(y,\alpha ,x)\in \text{supp}\text{Br}\left(\Theta \right)$ and $y^{\prime }\in \alpha$, then $(y^{\prime },x)\in \text{supp}\Theta$. Moreover, define ${\text{sus}}^{\Theta }:\Phi \to 2^{\Gamma }$ by ${\text{sus}}^{\Theta }\left(x\right):=\{y\in \Gamma \mid (y,x)\in \text{supp}\Theta \}$. Then, $\text{Br}\left(\Theta \right)\subseteq (\Theta ⋉{\text{sus}}^{\Theta }{)}^{\downarrow }$ (we slightly abuse notation by treating ${\text{sus}}^{\Theta }$ as a mapping $\Gamma \times \Phi \to 2^{\Gamma }$ that doesn't depend on the first argument, and also playing loose with the order of factors in the set on which our HUCs live).

This proof splits into two parts. Part 1 will be proving the support statement. Part 2 will be proving the thing with ${\text{sus}}^{\Theta }$.

Part 1: Here's the basics of how this part will work. There's some $(y^{\ast },{\alpha }^{\ast },x^{\ast })$ tuple in the support of $\text{Br}\left(\Theta \right)$. Since the support of $\text{Br}\left(\Theta \right)$ is the union of the supports for the $\theta \in \text{Br}\left(\Theta \right)$, there's some $\theta$ that assigns nonzero probability to that event. Also, $y^{\prime }\in {\alpha }^{\ast }$. The key part of the proof is showing there's some ${\theta }^{\ast }\in \text{Br}\left(\Theta \right)$ that assigns nonzero measure to the event $(y^{\prime },x^{\ast },{\alpha }^{\ast })$. Once we've got that, since we know by Proposition 2.1 that $\text{Br}\left(\Theta \right)$ projects down to equal $\Theta$, that means that the projection of ${\theta }^{\ast }$ will land in $\Theta$, and it will assign nonzero measure to the event $(y^{\prime },x^{\ast })$, so the event $(y^{\prime },x^{\ast })$ lies in the support of $\Theta$.

So, that just leaves appropriately defining our ${\theta }^{\ast }$ and showing that it lies in $\text{Br}\left(\Theta \right)$ and assigns nonzero probability to our event of interest. Our particular choice of ${\theta }^{\ast }$ will be as follows. Let $c_{y^{\prime }}:\Gamma \to \Gamma$ be the constant function mapping everything to $y^{\prime }$. $${\theta }^{\ast }:={\chi }_{{\text{el}}^{\Gamma }}\left(\right(c_{y^{\prime }}{)}_{\ast }\left(\theta \right))$$ Applying Lemma 3, this is in $\text{Br}\left(\Theta \right)$, so that just leaves showing that it assigns nonzero probability to the event $y^{\prime },x^{\ast },{\alpha }^{\ast }$. We have $${\chi }_{{\text{el}}^{\Gamma }}\left(\right(c_{y^{\prime }}{)}_{\ast }\left(\theta \right)\left)\right(\lambda y\alpha x.{\chi }_{y=y^{\prime }\wedge x=x^{\ast }\wedge \alpha ={\alpha }^{\ast }})$$ $$=\left(c_{y^{\prime }}{)}_{\ast }\right(\theta \left)\right(\lambda y\alpha x.{\chi }_{y=y^{\prime }\wedge x=x^{\ast }\wedge \alpha ={\alpha }^{\ast }\wedge y\in \alpha })$$ We can simplify this a bit, because if the first three properties hold, that tells you something about what $\alpha$ is. $$=\left(c_{y^{\prime }}{)}_{\ast }\right(\theta \left)\right(\lambda y\alpha x.{\chi }_{y=y^{\prime }\wedge x=x^{\ast }\wedge \alpha ={\alpha }^{\ast }\wedge y\in {\alpha }^{\ast }})$$ unpack the pushforward $$=\theta (\lambda y\alpha x.{\chi }_{c_{y^{\prime }}\left(y\right)=y^{\prime }\wedge x=x^{\ast }\wedge \alpha ={\alpha }^{\ast }\wedge c_{y^{\prime }}\left(y\right)\in {\alpha }^{\ast }})$$ Then we use that it's a constant function $$=\theta (\lambda y\alpha x.{\chi }_{y^{\prime }=y^{\prime }\wedge x=x^{\ast }\wedge \alpha ={\alpha }^{\ast }\wedge y^{\prime }\in {\alpha }^{\ast }})$$ Now, since $y^{\prime }\in {\alpha }^{\ast }$ by the problem setup, and $y^{\prime }=y^{\prime }$ is a tautology, we can remove those two events. $$=\theta (\lambda y\alpha x.{\chi }_{x=x^{\ast }\wedge \alpha ={\alpha }^{\ast }})$$ and use an inequality $$\ge \theta (\lambda y\alpha x.{\chi }_{y=y^{\ast }\wedge x=x^{\ast }\wedge \alpha ={\alpha }^{\ast }})>0$$ Because $\theta$ assigned nonzero probability to that event. So, we know that our ${\theta }^{\ast }$ assigns nonzero measure to the event of interest. And that's it! It fulfills the appropriate properties to carry the proof through.

Proof part 2: First off, we can reexpress $$\text{Br}\left(\Theta \right)\subseteq (\Theta ⋉{\text{sus}}^{\Theta }{)}^{\downarrow }$$ as the equivalent statement that, for all $f:{\text{el}}^{\Gamma }\times \Phi \to [0,1]$, we have $$\text{Br}\left(\Theta \right)(\lambda y\alpha x.f(y,x,\alpha \left)\right)\le (\Theta ⋉{\text{sus}}^{\Theta }{)}^{\downarrow }(\lambda y\alpha x.f(y,x,\alpha ))$$ Although, since $\text{Br}\left(\Theta \right)$ and $(\Theta ⋉{\text{sus}}^{\Theta }{)}^{\downarrow }$ are downwards-closed, we actually only need to demonstrate this inequality for monotone functions $f$.

The reason we only need to demonstrate this inequality for monotone $f$ is because of $$\text{Br}\left(\Theta \right)\left(f\right)=\text{Br}\left(\Theta \right)\left(f^{max}\right)\le (\Theta ⋉{\text{sus}}^{\Theta }{)}^{\downarrow }(f^{max})=(\Theta ⋉{\text{sus}}^{\Theta }{)}^{\downarrow }\left(f\right)$$ Where the equalities follow from Proposition 3.1 and the downward closure of the two ultracontributions, and the inequality is what we're trying to prove (since $f^{max}$ in the sense of Proposition 3.1 is always a monotone function.

So, let $f$ be monotone, and we're trying to prove the desired inequality. We'll unpack it bit by bit. $$\text{Br}\left(\Theta \right)(\lambda y\alpha x.f(y,x,\alpha \left)\right)=\underset{\theta \in \text{Br}\left(\Theta \right)}{max}\theta (\lambda y\alpha x.f(y,x,\alpha \left)\right)$$ And now we remember that the set $\{x,y|y\in {\text{sus}}^{\Theta }(x\left)\right\}$ is a support for $\Theta$, because it's the same as $\{x,y|(y,x)\in \text{supp}\Theta \}$, ie, the support of $\Theta$. So, by Lemma 2, we can conclude that any $\theta \in \text{Br}\left(\Theta \right)$ is supported on $\alpha ,x$ pairs s.t. $\alpha \subseteq {\text{sus}}^{\Theta }\left(x\right)$. In particular, this means that $\alpha \le {\text{sus}}^{\Theta }\left(x\right)$, and since $f$ is monotone, swapping out $\alpha$ for ${\text{sus}}^{\Theta }\left(x\right)$ always produces an increase in expected value, so we get $$\le \underset{\theta \in \text{Br}\left(\Theta \right)}{max}\theta (\lambda y\alpha x.f(y,x,{\text{sus}}^{\Theta }\left(x\right)\left)\right)$$ and then, since all $\theta \in \text{Br}\left(\Theta \right)$ are supported on $y,\alpha$ s.t. $y\in \alpha$, we can go $$=\underset{\theta \in \text{Br}\left(\Theta \right)}{max}\theta (\lambda y\alpha x.{\chi }_{y\in \alpha }f(y,x,{\text{sus}}^{\Theta }\left(x\right)\left)\right)$$ And then, since all the $\theta \in \text{Br}\left(\Theta \right)$ fulfill the endofunction property, we can let $s$ be identity and $g$ be $f$, and go $$\le \Theta (\lambda yx.f(y,x,{\text{sus}}^{\Theta }\left(x\right)\left)\right)$$ And rewrite that as $$=\Theta (\lambda yx.{\delta }_{{\text{sus}}^{\Theta }\left(x\right)}(\lambda \alpha .f(y,x,\alpha )\left)\right)$$ $$=(\Theta ⋉{\text{sus}}^{\Theta })(\lambda y\alpha x.f(y,x,\alpha \left)\right)$$ and then since $f$ is monotone $$=(\Theta ⋉{\text{sus}}^{\Theta }{)}^{\downarrow }(\lambda y\alpha x.f(y,x,\alpha ))$$ This holds because all contributions added when you take the downward closure can only produce lower expectation values than the existing contributions due to monotonicity of $f$, and so they're ignored.

And now we're done! We got the inequality going appropriately to hit our proof target. $■$

Proposition 2.8: For any $\Gamma$, $\Phi$ and $\Theta \in {\square }^c(\Gamma \times \Phi )$ $$\text{Br}\left({\text{pr}}_{\Gamma \times 2^{\Gamma }}\text{Br}\right(\Theta \left)\right)=\left[\right({\text{id}}_{\Gamma }\times {\text{diag}}_{2^{\Gamma }}{)}_{\ast }{\text{pr}}_{\Gamma \times 2^{\Gamma }}\text{Br}\left(\Theta \right){]}^{\downarrow }$$

For notation, we'll use $\beta$ for the set which is being treated as part of the background environment, and $\alpha$ as the usual set.

The way to establish this is to show equal expectation values for all functions monotone in the last argument (the relevant set-based one), which is all we need to do as both sets are downwards-closed. We'll do this by establishing the two inequalities separately. Our first order of business is showing that for all $f:{\text{el}}^{\Gamma }\times 2^{\Gamma }$ monotone in the last coordinate, we have $$\text{Br}\left({\text{pr}}_{\Gamma \times 2^{\Gamma }}\text{Br}\right(\Theta \left)\right)(\lambda y\alpha \beta .f(y,\beta ,\alpha \left)\right)\ge \left[\right({\text{id}}_{\Gamma }\times {\text{diag}}_{2^{\Gamma }}{)}_{\ast }{\text{pr}}_{\Gamma \times 2^{\Gamma }}\text{Br}\left(\Theta \right){]}^{\downarrow }(\lambda y\alpha \beta .f(y,\beta ,\alpha \left)\right)$$ Let's begin. Pick an $f$ that's monotone in the last argument. $$\left[\right({\text{id}}_{\Gamma }\times {\text{diag}}_{2^{\Gamma }}{)}_{\ast }{\text{pr}}_{\Gamma \times 2^{\Gamma }}\text{Br}\left(\Theta \right){]}^{\downarrow }(\lambda y\alpha \beta .f(y,\beta ,\alpha \left)\right)$$ $$=\left[\right({\text{id}}_{\Gamma }\times {\text{diag}}_{2^{\Gamma }}{)}_{\ast }{\text{pr}}_{\Gamma \times 2^{\Gamma }}\text{Br}\left(\Theta \right)\left]\right(\lambda y\alpha \beta .f(y,\beta ,\alpha ))$$ $$={\text{pr}}_{\Gamma \times 2^{\Gamma }}\text{Br}\left(\Theta \right)(\lambda y\beta .f(y,\beta ,\beta \left)\right)=\text{Br}\left(\Theta \right)(\lambda y\beta x.f(y,\beta ,\beta \left)\right)$$ $$=\underset{{\theta }^{\prime }\in \text{Br}\left(\Theta \right)}{max}{\theta }^{\prime }(\lambda y\beta x.f(y,\beta ,\beta \left)\right)=\underset{{\theta }^{\prime }\in \text{Br}\left(\Theta \right)}{max}{\theta }^{\prime }(\lambda y\beta x.{\delta }_{\beta }(\lambda \alpha .f(y,\beta ,\alpha )\left)\right)$$ $$=\underset{{\theta }^{\prime }\in \text{Br}\left(\Theta \right)}{max}{\text{pr}}_{\Gamma \times 2^{\Gamma }}\left({\theta }^{\prime }\right)(\lambda y\beta .{\delta }_{\beta }(\lambda \alpha .f(y,\beta ,\alpha )\left)\right)$$ $$=\underset{{\theta }^{\prime }\in \text{Br}\left(\Theta \right)}{max}\left({\text{pr}}_{\Gamma \times 2^{\Gamma }}\right({\theta }^{\prime })⋉{\text{id}}_{2^{\Gamma }})(\lambda y\beta \alpha .f(y,\beta ,\alpha \left)\right)$$ We'll set this to the side for a moment to show that if ${\theta }^{\prime }\in \text{Br}\left(\Theta \right)$, then ${\text{pr}}_{\Gamma \times 2^{\Gamma }}\left({\theta }^{\prime }\right)⋉{\text{id}}_{2^{\Gamma }}\in \text{Br}\left({\text{pr}}_{\Gamma \times 2^{\Gamma }}\text{Br}\right(\Theta \left)\right)$.

The support part is easy. Since ${\theta }^{\prime }\in \text{Br}\left(\Theta \right)$, it's supported on $(y,\beta )$ pairs where $y\in \beta$. Taking semidirect product with identity means that $y\in \alpha$ always happens, because $\beta =\alpha$ always happens. So, that leaves showing the endofunction condition. We have $$\left({\text{pr}}_{\Gamma \times 2^{\Gamma }}\right({\theta }^{\prime })⋉{\text{id}}_{2^{\Gamma }})(\lambda y\alpha \beta .{\chi }_{s\left(y\right)\in \alpha }g(s\left(y\right),\beta \left)\right)$$ $$={\text{pr}}_{\Gamma \times 2^{\Gamma }}\left({\theta }^{\prime }\right)(\lambda y\beta .{\delta }_{\beta }(\lambda \alpha .{\chi }_{s\left(y\right)\in \alpha }g\left(s\right(y),\beta ))$$ $$={\text{pr}}_{\Gamma \times 2^{\Gamma }}\left({\theta }^{\prime }\right)(\lambda y\beta .{\chi }_{s\left(y\right)\in \beta }g(s\left(y\right),\beta \left)\right)={\theta }^{\prime }(\lambda y\beta x.{\chi }_{s\left(y\right)\in \beta }g(s\left(y\right),\beta \left)\right)$$ And start packing things up a bit $$=s_{\ast }\left({\theta }^{\prime }\right)(\lambda y\beta x.{\chi }_{y\in \beta }g(y,\beta \left)\right)$$ $$={\chi }_{{\text{el}}^{\Gamma }}\left(s_{\ast }\right({\theta }^{\prime }\left)\right)(\lambda y\beta x.g(y,\beta \left)\right)$$ And, since ${\theta }^{\prime }\in \text{Br}\left(\Theta \right)$, this update of the pushforward of ${\theta }^{\prime }$ lands in $\text{Br}\left(\Theta \right)$ by Lemma 3, so we get $$\le \underset{{\theta }^{\prime \prime }\in \text{Br}\left(\Theta \right)}{max}{\theta }^{\prime \prime }(\lambda y\beta x.g(y,\beta \left)\right)$$ $$=\text{Br}\left(\Theta \right)(\lambda y\beta x.g(y,\beta \left)\right)$$ $$={\text{pr}}_{\Gamma \times 2^{\Gamma }}\text{Br}\left(\Theta \right)(\lambda y\beta .g(y,\beta \left)\right)$$ Now, since we've established that inequality for all choices of $s,g$, we have that $${\text{pr}}_{\Gamma \times 2^{\Gamma }}\left({\theta }^{\prime }\right)⋉{\text{id}}_{2^{\Gamma }}\in \text{Br}\left({\text{pr}}_{\Gamma \times 2^{\Gamma }}\text{Br}\right(\Theta \left)\right)$$ Resuming where we last left off, the last place we were at in our chain of inequalities was $$=\underset{{\theta }^{\prime }\in \text{Br}\left(\Theta \right)}{max}\left({\text{pr}}_{\Gamma \times 2^{\Gamma }}\right({\theta }^{\prime })⋉{\text{id}}_{2^{\Gamma }})(\lambda y\alpha \beta .f(y,\beta ,\alpha \left)\right)$$ Since these things are always in $\text{Br}\left({\text{pr}}_{\Gamma \times 2^{\Gamma }}\text{Br}\right(\Theta \left)\right)$, we can go $$\le \underset{{\theta }^{\prime \prime }\in \text{Br}\left({\text{pr}}_{\Gamma \times 2^{\Gamma }}\text{Br}\right(\Theta \left)\right)}{max}{\theta }^{\prime \prime }(\lambda y\alpha \beta .f(y,\beta ,\alpha \left)\right)$$ $$=\text{Br}\left({\text{pr}}_{\Gamma \times 2^{\Gamma }}\text{Br}\right(\Theta \left)\right)(\lambda y\alpha \beta .f(y,\beta ,\alpha \left)\right)$$ And we're done with that inequality direction.

Now to show the reverse direction, which actually will use that $f$ is monotone in the last argument. We start with $$\text{Br}\left({\text{pr}}_{\Gamma \times 2^{\Gamma }}\text{Br}\right(\Theta \left)\right)(\lambda y\alpha \beta .f(y,\beta ,\alpha \left)\right)$$ $$=\underset{{\theta }^{\prime \prime }\in \text{Br}\left({\text{pr}}_{\Gamma \times 2^{\Gamma }}\text{Br}\right(\Theta \left)\right)}{max}{\theta }^{\prime \prime }(\lambda y\alpha \beta .f(y,\beta ,\alpha \left)\right)$$ And now, we can use that ${\text{pr}}_{\Gamma \times 2^{\Gamma }}\text{Br}\left(\Theta \right)$ is supported on $(y,\beta )$ pairs where $y\in \text{id}\left(\beta \right)$, along with Lemma 2 applied to id, to conclude that all the ${\theta }^{\prime \prime }$ must be supported on the event $\alpha \subseteq \text{id}\left(\beta \right)=\beta$. Since big sets go more towards the top and get a higher loss, and $f$ is monotone in the last argument, we get $$\le \underset{{\theta }^{\prime \prime }\in \text{Br}\left({\text{pr}}_{\Gamma \times 2^{\Gamma }}\text{Br}\right(\Theta \left)\right)}{max}{\theta }^{\prime \prime }(\lambda y\alpha \beta .f(y,\beta ,\beta \left)\right)$$ Now, we can use the endofunction property of all the ${\theta }^{\prime \prime }$ w.r.t. ${\text{pr}}_{\Gamma \times 2^{\Gamma }}\text{Br}\left(\Theta \right)$ to get a uniform upper bound of $$\le {\text{pr}}_{\Gamma \times 2^{\Gamma }}\text{Br}\left(\Theta \right)(\lambda y\beta .f(y,\beta ,\beta \left)\right)$$ and then go $$=\left[\right({\text{id}}_{\Gamma }\times {\text{diag}}_{2^{\Gamma }}{)}_{\ast }{\text{pr}}_{\Gamma \times 2^{\Gamma }}\text{Br}\left(\Theta \right)\left]\right(\lambda y\alpha \beta .f(y,\beta ,\alpha ))$$ $$=\left[\right({\text{id}}_{\Gamma }\times {\text{diag}}_{2^{\Gamma }}{)}_{\ast }{\text{pr}}_{\Gamma \times 2^{\Gamma }}\text{Br}\left(\Theta \right){]}^{\downarrow }(\lambda y\alpha \beta .f(y,\beta ,\alpha \left)\right)$$ and we're done, we got the inequality going in the other direction, so we have equality for arbitrary monotone functions, and thus equality. $■$

Proposition 2.9: For any $\Gamma$, $\Phi$ and ${\Theta }_1,{\Theta }_2\in {\square }^c(\Gamma \times \Phi )$, if ${\Theta }_1\subseteq {\Theta }_2$ then $\text{Br}\left({\Theta }_1\right)\subseteq \text{Br}\left({\Theta }_2\right)$.

Proof: This is really easy to show, we just need to take some contribution ${\theta }^{\prime }\in \text{Br}\left({\Theta }_1\right)$ and show that it lies in $\text{Br}\left({\Theta }_2\right)$. The support condition is easily fulfilled, so that leaaves showing the endofunction condition. Let's begin. $${\theta }^{\prime }(\lambda y\alpha x.{\chi }_{s\left(y\right)\in \alpha }g(s\left(y\right),x\left)\right)\le {\Theta }_1(\lambda yx.g(y,x\left)\right)=\underset{\theta \in {\Theta }_1}{max}\theta (\lambda yx.g(y,x\left)\right)$$ And now, since ${\Theta }_1\subseteq {\Theta }_2$, we have $$\le \underset{\theta \in {\Theta }_2}{max}\theta (\lambda yx.g(y,x\left)\right)={\Theta }_2(\lambda yx.g(y,x\left)\right)$$ Done. $■$

Proposition 2.10: For any $\Gamma$, ${\Phi }_1$, ${\Phi }_2$, $t:{\Phi }_2\to {\Phi }_1$ and $\Theta \in {\square }^c(\Gamma \times {\Phi }_2)$ $$({\text{id}}_{{\text{el}}^{\Gamma }}\times t{)}_{\ast }\text{Br}(\Theta )\subseteq \text{Br}(({\text{id}}_{\Gamma }\times t{)}_{\ast }\Theta )$$

As usual, we just need to establish that for all $f:{\text{el}}^{\Gamma }\times \Phi$, the expectation value is lower in the first function than the second function, so our proof goal will be $$({\text{id}}_{{\text{el}}^{\Gamma }}\times t{)}_{\ast }\text{Br}(\Theta \left)\right(\lambda y\alpha x_1.f(y,\alpha ,x_1))\le \text{Br}(({\text{id}}_{\Gamma }\times t{)}_{\ast }\Theta )(\lambda y\alpha x_1.f(y,\alpha ,x_1\left)\right)$$ Let's begin trying to show this. $$({\text{id}}_{{\text{el}}^{\Gamma }}\times t{)}_{\ast }\text{Br}(\Theta \left)\right(\lambda y\alpha x_1.f(y,x_1,\alpha ))$$ $$=\text{Br}\left(\Theta \right)(\lambda y\alpha x_2.f(y,t\left(x_2\right),\alpha \left)\right)$$ $$=\underset{{\theta }^{\prime }\in \text{Br}\left(\Theta \right)}{max}{\theta }^{\prime }(\lambda y\alpha x_2,.f(y,t\left(x_2\right),\alpha \left)\right)$$ $$=\underset{{\theta }^{\prime }\in \text{Br}\left(\Theta \right)}{max}({\text{id}}_{{\text{el}}^{\Gamma }}\times t{)}_{\ast }({\theta }^{\prime }\left)\right(\lambda y\alpha x_1.f(y,x_1,\alpha ))$$ Now we will show that all the contributions of this form lie in $\text{Br}\left(\right({\text{id}}_{\Gamma }\times t{)}_{\ast }\Theta )$. Clearly the $y\in \alpha$ condition is always fulfilled for these pushforwards, so that just leaves the endofunction condition. Let's begin. $$({\text{id}}_{{\text{el}}^{\Gamma }}\times t{)}_{\ast }({\theta }^{\prime }\left)\right(\lambda y\alpha x_1.{\chi }_{s\left(y\right)\in \alpha }g\left(s\right(y),x_1))={\theta }^{\prime }(\lambda y\alpha x_2.{\chi }_{s\left(y\right)\in \alpha }g\left(s\right(y),t(x_2\left)\right))$$ $$\le \Theta (\lambda y{x}_2.g(y,t\left(x_2\right)\left)\right)=({\text{id}}_{\Gamma }\times t{)}_{\ast }(\Theta \left)\right(\lambda y{x}_1.g(y,x_1))$$ And we're done, we established our desired result that the pushforward lands in the appropriate set. So, we can proceed by going $$\le \underset{{\theta }^{\prime \prime }\in \text{Br}\left(\right({\text{id}}_{\Gamma }\times t{)}_{\ast }\left(\Theta \right))}{max}{\theta }^{\prime \prime }(\lambda y\alpha x_1.f(y,x_1,\alpha \left)\right)$$ $$=\text{Br}\left(\right({\text{id}}_{\Gamma }\times t{)}_{\ast }\left(\Theta \right)\left)\right(\lambda y\alpha x_1.f(y,x_1,\alpha ))$$ And we're done! $■$

Proposition 2.11: Consider any $\Gamma$, ${\Phi }_1$, ${\Phi }_2$, $t:{\Phi }_2\to {\Phi }_1$, $\Xi :{\Phi }_1\to \square {\Phi }_2$ and $\Theta \in {\square }^c(\Gamma \times {\Phi }_1)$ s.t. $t\circ \Xi ={\text{id}}_{{\Phi }_1}$. Then, $$({\text{id}}_{{\text{el}}^{\Gamma }}\times \Xi {)}_{\ast }\text{Br}(\Theta )\subseteq \text{Br}(({\text{id}}_{\Gamma }\times \Xi {)}_{\ast }\Theta )\subseteq ({\text{id}}_{{\text{el}}^{\Gamma }}\times t{)}^{\ast }\text{Br}(\Theta )$$ In particular, $${\text{pr}}_{{\text{el}}^{\Gamma }}\text{Br}\left(\Theta \right)={\text{pr}}_{{\text{el}}^{\Gamma }}\text{Br}\left(\right({\text{id}}_{\Gamma }\times \Xi {)}_{\ast }\Theta )$$

Well, let's get started on proving these various things. To begin with, to prove $$({\text{id}}_{{\text{el}}^{\Gamma }}\times \Xi {)}_{\ast }\text{Br}(\Theta )\subseteq \text{Br}(({\text{id}}_{\Gamma }\times \Xi {)}_{\ast }\Theta )$$ We need to prove that, for all $f:{\text{el}}^{\Gamma }\times {\Phi }_2\to [0,1]$, $$({\text{id}}_{{\text{el}}^{\Gamma }}\times \Xi {)}_{\ast }\text{Br}(\Theta \left)\right(\lambda y\alpha x_2.f(y,x_2,\alpha ))\le \text{Br}(({\text{id}}_{\Gamma }\times \Xi {)}_{\ast }\Theta )(\lambda y\alpha x_2.f(y,x_2,\alpha \left)\right)$$ Let's establish this. Unpacking the left-hand side, we have $$({\text{id}}_{{\text{el}}^{\Gamma }}\times \Xi {)}_{\ast }\text{Br}(\Theta \left)\right(\lambda y\alpha x_2.f(y,x_2,\alpha ))$$ $$=\text{Br}\left(\Theta \right)(\lambda y\alpha x_1.\Xi (x_1\left)\right(\lambda x_2.f(y,x_2,\alpha )\left)\right)$$ $$=\underset{{\theta }^{\prime }\in \text{Br}\left(\Theta \right)}{max}{\theta }^{\prime }(\lambda y\alpha x_1.\Xi (x_1\left)\right(\lambda x_2.f(y,x_2,\alpha )\left)\right)$$ $$=\underset{{\theta }^{\prime }\in \text{Br}\left(\Theta \right)}{max}({\text{id}}_{{\text{el}}^{\Gamma }}\times \Xi {)}_{\ast }({\theta }^{\prime }\left)\right(\lambda y\alpha x_2.f(y,x_2,\alpha ))$$ $$=\underset{{\theta }^{\prime }\in \text{Br}\left(\Theta \right)}{max}\underset{{\theta }^{\prime \prime }\in ({\text{id}}_{{\text{el}}^{\Gamma }}\times \Xi {)}_{\ast }({\theta }^{\prime })}{max}{\theta }^{\prime \prime }(\lambda y\alpha x_2.f(y,x_2,\alpha \left)\right)$$ Now we'll show that this ${\theta }^{\prime \prime }$ lies in $\text{Br}\left(\right({\text{id}}_{\Gamma }\times \Xi {)}_{\ast }\Theta )$. The support condition is trivial, so that leaves the endofunction condition. $${\theta }^{\prime \prime }(\lambda y\alpha x_2.{\chi }_{y\in \alpha }g(s\left(y\right),x_2\left)\right)\le ({\text{id}}_{{\text{el}}^{\Gamma }}\times \Xi {)}_{\ast }({\theta }^{\prime }\left)\right(\lambda y\alpha x_2.{\chi }_{s\left(y\right)\in \alpha }g\left(s\right(y),x_2))$$ $$={\theta }^{\prime }(\lambda y\alpha x_1.\Xi (x_1\left)\right(\lambda x_2.{\chi }_{s\left(y\right)\in \alpha }g\left(s\right(y),x_2)\left)\right)$$ Then, by homogenity of $\Xi$, we can pull a constant out, the indicator function, to get $$={\theta }^{\prime }(\lambda y\alpha x_1.{\chi }_{s\left(y\right)\in \alpha }\Xi (x_1\left)\right(\lambda x_2.g\left(s\right(y),x_2)\left)\right)$$ Then, by the endofunction condition, we get $$\le \Theta (\lambda y{x}_1.\Xi (x_1\left)\right(\lambda x_2.g(y,x_2)\left)\right)$$ $$=({\text{id}}_{\Gamma }\times \Xi {)}_{\ast }(\Theta \left)\right(\lambda y{x}_2.g(y,x_2))$$ And bam, we've showed that ${\theta }^{\prime \prime }$ lies in the appropriate set. We were last at $$=\underset{{\theta }^{\prime }\in \text{Br}\left(\Theta \right)}{max}\underset{{\theta }^{\prime \prime }\in ({\text{id}}_{{\text{el}}^{\Gamma }}\times \Xi {)}_{\ast }({\theta }^{\prime })}{max}{\theta }^{\prime \prime }(\lambda y\alpha x_2.f(y,x_2,\alpha \left)\right)$$ So we can impose an upper bound of $$\le \underset{{\theta }^{\prime \prime }\in \text{Br}\left(\right({\text{id}}_{\Gamma }\times \Xi {)}_{\ast }\Theta )}{max}{\theta }^{\prime \prime }(\lambda y\alpha x_2.f(y,x_2,\alpha \left)\right)$$ $$\le \text{Br}\left(\right({\text{id}}_{\Gamma }\times \Xi {)}_{\ast }\left(\Theta \right)\left)\right(\lambda y\alpha x_2.f(y,x_2,\alpha ))$$ And we're done, we've established our desired inequality. Now for proving another inequality. $$\text{Br}\left(\right({\text{id}}_{\Gamma }\times \Xi {)}_{\ast }\Theta )\subseteq ({\text{id}}_{{\text{el}}^{\Gamma }}\times t{)}^{\ast }\text{Br}\left(\Theta \right)$$ This can be proved by applying Proposition 2.10. Start out with Proposition 2.10. $$({\text{id}}_{{\text{el}}^{\Gamma }}\times t{)}_{\ast }\text{Br}({\Theta }^{\prime })\subseteq \text{Br}(({\text{id}}_{\Gamma }\times t{)}_{\ast }{\Theta }^{\prime })$$ Specialize ${\Theta }^{\prime }$ to $({\text{id}}_{\Gamma }\times \Xi {)}_{\ast }(\Theta )$, yielding $$({\text{id}}_{{\text{el}}^{\Gamma }}\times t{)}_{\ast }\text{Br}(({\text{id}}_{\Gamma }\times \Xi {)}_{\ast }\Theta )\subseteq \text{Br}\left(\right({\text{id}}_{\Gamma }\times t{)}_{\ast }({\text{id}}_{\Gamma }\times \Xi {)}_{\ast }\Theta )$$ The two pushforwards can be folded into one. $$({\text{id}}_{{\text{el}}^{\Gamma }}\times t{)}_{\ast }\text{Br}(({\text{id}}_{\Gamma }\times \Xi {)}_{\ast }\Theta )\subseteq \text{Br}\left(\right({\text{id}}_{\Gamma }\times t\circ \Xi {)}_{\ast }\Theta )$$ Now use that $t\circ \Xi$ is identity $$({\text{id}}_{{\text{el}}^{\Gamma }}\times t{)}_{\ast }\text{Br}(({\text{id}}_{\Gamma }\times \Xi {)}_{\ast }\Theta )\subseteq \text{Br}\left(\Theta \right)$$ Apply pullback along $t$ to both sides $$({\text{id}}_{{\text{el}}^{\Gamma }}\times t{)}^{\ast }({\text{id}}_{{\text{el}}^{\Gamma }}\times t{)}_{\ast }\text{Br}\left(\right({\text{id}}_{\Gamma }\times \Xi {)}_{\ast }\Theta )\subseteq ({\text{id}}_{{\text{el}}^{\Gamma }}\times t{)}^{\ast }\text{Br}\left(\Theta \right)$$

On the other hand, we also have

$$\text{Br}\left(\right({\text{id}}_{\Gamma }\times \Xi {)}_{\ast }\Theta )\subseteq ({\text{id}}_{{\text{el}}^{\Gamma }}\times t{)}^{\ast }({\text{id}}_{{\text{el}}^{\Gamma }}\times t{)}_{\ast }\text{Br}(({\text{id}}_{\Gamma }\times \Xi {)}_{\ast }\Theta )$$

Combining the last two lines, we get the desired result:

$$\text{Br}\left(\right({\text{id}}_{\Gamma }\times \Xi {)}_{\ast }\Theta )\subseteq ({\text{id}}_{{\text{el}}^{\Gamma }}\times t{)}^{\ast }\text{Br}\left(\Theta \right)$$ That just leaves showing the equality result, now that we've got both subset inclusions.

We start out with $$({\text{id}}_{{\text{el}}^{\Gamma }}\times \Xi {)}_{\ast }\text{Br}(\Theta )\subseteq \text{Br}(({\text{id}}_{\Gamma }\times \Xi {)}_{\ast }\Theta )\subseteq ({\text{id}}_{{\text{el}}^{\Gamma }}\times t{)}^{\ast }\text{Br}(\Theta )$$ Applying projection yields $${\text{pr}}_{{\text{el}}^{\Gamma }}\left(\right({\text{id}}_{{\text{el}}^{\Gamma }}\times \Xi {)}_{\ast }\text{Br}\left(\Theta \right))\subseteq {\text{pr}}_{{\text{el}}^{\Gamma }}(\text{Br}\left(\right({\text{id}}_{\Gamma }\times \Xi {)}_{\ast }\Theta \left)\right)\subseteq {\text{pr}}_{{\text{el}}^{\Gamma }}\left(\right({\text{id}}_{{\text{el}}^{\Gamma }}\times t{)}^{\ast }\text{Br}\left(\Theta \right))$$ For any given $f$, we have $${\text{pr}}_{{\text{el}}^{\Gamma }}\left(\right({\text{id}}_{{\text{el}}^{\Gamma }}\times \Xi {)}_{\ast }\text{Br}\left(\Theta \right)\left)\right(\lambda y\alpha .f(y,\alpha ))$$ $$\le {\text{pr}}_{{\text{el}}^{\Gamma }}\left(\text{Br}\right(({\text{id}}_{\Gamma }\times \Xi {)}_{\ast }\Theta )\left)\right(\lambda y\alpha .f(y,\alpha ))$$ $$\le {\text{pr}}_{{\text{el}}^{\Gamma }}\left(\right({\text{id}}_{{\text{el}}^{\Gamma }}\times t{)}^{\ast }\text{Br}\left(\Theta \right)\left)\right(\lambda y\alpha .f(y,\alpha ))$$ Unpacking the projection on the two ends, we get $$({\text{id}}_{{\text{el}}^{\Gamma }}\times \Xi {)}_{\ast }\text{Br}(\Theta \left)\right(\lambda y\alpha x_2.f(y,\alpha ))$$ $$\le {\text{pr}}_{{\text{el}}^{\Gamma }}\left(\text{Br}\right(({\text{id}}_{\Gamma }\times \Xi {)}_{\ast }\Theta )\left)\right(\lambda y\alpha .f(y,\alpha ))$$ $$\le ({\text{id}}_{{\text{el}}^{\Gamma }}\times t{)}^{\ast }\text{Br}(\Theta \left)\right(\lambda y\alpha x_2.f(y,\alpha ))$$ And then, for the smallest and largest quantities, the pullback or pushforward only affects the $x_1$ or $x_2$ coordinates, everything else remains the same. In particular, $f$ doesn't depend on such coordinates. So, we get $$\text{Br}\left(\Theta \right)(\lambda y\alpha x_1.f(y,\alpha \left)\right)$$ $$\le {\text{pr}}_{{\text{el}}^{\Gamma }}\left(\text{Br}\right(({\text{id}}_{\Gamma }\times \Xi {)}_{\ast }\Theta )\left)\right(\lambda y\alpha .f(y,\alpha ))$$ $$\le \text{Br}\left(\Theta \right)(\lambda y\alpha x_1.f(y,\alpha \left)\right)$$ The left and right hand sides are equal, so we have $${\text{pr}}_{{\text{el}}^{\Gamma }}\left(\text{Br}\right(({\text{id}}_{\Gamma }\times \Xi {)}_{\ast }\Theta )\left)\right(\lambda y\alpha .f(y,\alpha ))=\text{Br}(\Theta \left)\right(\lambda y\alpha x_1.f(y,\alpha ))$$ Then, packing the projection back up, we have $${\text{pr}}_{{\text{el}}^{\Gamma }}\left(\text{Br}\right(({\text{id}}_{\Gamma }\times \Xi {)}_{\ast }\Theta )\left)\right(\lambda y\alpha .f(y,\alpha ))={\text{pr}}_{{\text{el}}^{\Gamma }}\text{Br}(\Theta \left)\right(\lambda y\alpha .f(y,\alpha ))$$ And since there's equality for all functions, the two ultradistributions are equal, so we have $${\text{pr}}_{{\text{el}}^{\Gamma }}\left(\text{Br}\right(({\text{id}}_{\Gamma }\times \Xi {)}_{\ast }\Theta ))={\text{pr}}_{{\text{el}}^{\Gamma }}\text{Br}(\Theta )$$ And we're done. $■$

Proposition 2.12: For any $\Gamma$, $\Phi$, ${\Theta }_1,{\Theta }_2\in {\square }^c(\Gamma \times \Phi )$ and $p\in [0,1]$ $$p\text{Br}\left({\Theta }_1\right)+(1-p)\text{Br}\left({\Theta }_2\right)\subseteq \text{Br}(p{\Theta }_1+(1-p\left){\Theta }_2\right)$$

We'll do this by showing that all contributions of the form $p\theta +(1-p){\theta }^{\prime }$ with $\theta \in \text{Br}\left({\Theta }_1\right)$ and ${\theta }^{\prime }\in \text{Br}\left({\Theta }_2\right)$ lie within $\text{Br}(p{\Theta }_1+(1-p\left){\Theta }_2\right)$. The support property is trivial, so that leaves the endofunction property. $$(p\theta +(1-p\left){\theta }^{\prime }\right)(\lambda y\alpha x.{\chi }_{s\left(y\right)\in \alpha }g(s\left(y\right),x\left)\right)$$ $$=p\theta (\lambda y\alpha x.{\chi }_{s\left(y\right)\in \alpha }g(s\left(y\right),x\left)\right)+(1-p){\theta }^{\prime }(\lambda y\alpha x.{\chi }_{s\left(y\right)\in \alpha }g(s\left(y\right),x\left)\right)$$ $$\le p{\Theta }_1(\lambda yx.g(y,x\left)\right)+(1-p){\Theta }_2(\lambda yx.g(y,x\left)\right)$$ $$=(p{\Theta }_1+(1-p\left){\Theta }_2\right)(\lambda yx.g(y,x\left)\right)$$ Done, the mix lies in $\text{Br}(p{\Theta }_1+(1-p\left){\Theta }_2\right)$. $■$

Proposition 2.13: Consider some $\Gamma$, ${\Phi }_1$, ${\Phi }_2$, ${\Theta }_1\in {\square }^c(\Gamma \times {\Phi }_1)$, ${\Theta }_1\in {\square }^c(\Gamma \times {\Phi }_2)$ and $p\in [0,1]$. Regard ${\Phi }_{1,2}$ as subsets of ${\Phi }_1\bigsqcup {\Phi }_2$, so that $p{\Theta }_1+(1-p){\Theta }_2\in {\square }^c(\Gamma \times ({\Phi }_1\bigsqcup {\Phi }_2\left)\right)$. Then, $$p\text{Br}\left({\Theta }_1\right)+(1-p)\text{Br}\left({\Theta }_2\right)=\text{Br}(p{\Theta }_1+(1-p\left){\Theta }_2\right)$$

We already established one subset direction in Proposition 2.12. We just need the other direction, to take any ${\theta }^{\prime \prime }\in \text{Br}(p{\Theta }_1+(1-p\left){\Theta }_2\right)$, and write it as $p\theta +(1-p){\theta }^{\prime }$ where $\theta \in \text{Br}\left({\Theta }_1\right)$ and ${\theta }^{\prime }\in \text{Br}\left({\Theta }_2\right)$.

We trivially have equality when $p=0$ or 1, so that leaves the cases where $p\in (0,1)$. With that, our attempted $\theta$ will be $\frac{{\chi }_{{\Phi }_1}{\theta }^{\prime \prime }}{p}$, and our attempted ${\theta }^{\prime }$ will be $\frac{{\chi }_{{\Phi }_2}{\theta }^{\prime \prime }}{1-p}$.

Now, clearly, these mix to make ${\theta }^{\prime \prime }$, because $$p\theta +(1-p){\theta }^{\prime }=p\frac{{\chi }_{{\Phi }_1}{\theta }^{\prime \prime }}{p}+(1-p)\frac{{\chi }_{{\Phi }_2}{\theta }^{\prime \prime }}{1-p}={\chi }_{{\Phi }_1}{\theta }^{\prime \prime }+{\chi }_{{\Phi }_2}{\theta }^{\prime \prime }={\theta }^{\prime \prime }$$ Remember, ${\Phi }_1$ and ${\Phi }_2$ are the two components of a space made by disjoint union.

They clearly both fulfill the support condition, because they're made from ${\theta }^{\prime \prime }$ which fulfills the support condition. This leaves the endofunction condition, which is somewhat nontrivial to show, and will require some setup. Clearly, without loss of generality, we just need to show it for $\theta$, and ${\theta }^{\prime }$ follows by identical arguments. For some $g:\Gamma \times ({\Phi }_1\bigsqcup {\Phi }_2)\to [0,1]$, $g^{\prime }$ will denote the function that mimics $g$ on $\Gamma \times {\Phi }_1$, and is 0 on $\Gamma \times {\Phi }_2$.

Also, note that $\theta$, as defined, is supported entirely on $\Gamma \times {\Phi }_1$, and ${\theta }^{\prime }$, as defined, is supported entirely on $\Gamma \times {\Phi }_2$. Let's get started on showing our endofunction condition. Let $g$ and $s$ be arbitrary. $$\theta (\lambda y\alpha x.{\chi }_{s\left(y\right)\in \alpha }g(s\left(y\right),x\left)\right)$$ $$=\theta (\lambda y\alpha x.{\chi }_{s\left(y\right)\in \alpha }g(s\left(y\right),x\left)\right)+\frac{1-p}{p}{\theta }^{\prime }\left(\lambda y\alpha x.0\right)$$ This is because the expectation of an all-0 function is 0. Then, $$=\theta (\lambda y\alpha x.{\chi }_{s\left(y\right)\in \alpha }{g}^{\prime }(s\left(y\right),x\left)\right)+\frac{1-p}{p}{\theta }^{\prime }(\lambda y\alpha x.{\chi }_{s\left(y\right)\in \alpha }{g}^{\prime }(s\left(y\right),x\left)\right)$$ Why does this happen? Well, $\theta$ is supported entirely on ${\Phi }_1$, and $g^{\prime }$ mimics $g$ perfectly on ${\Phi }_1$. And ${\theta }^{\prime }$ is supported entirely on ${\Phi }_2$, and $g^{\prime }$ mimics $0$ perfectly on ${\Phi }_2$. So it doesn't matter that we changed the functions outside of the contribution support. $$=(\theta +\frac{1-p}{p}{\theta }^{\prime })(\lambda y\alpha x.{\chi }_{s\left(y\right)\in \alpha }{g}^{\prime }(s\left(y\right),x\left)\right)$$ $$=\frac{1}{p}(p\theta +(1-p\left){\theta }^{\prime }\right)(\lambda y\alpha x.{\chi }_{s\left(y\right)\in \alpha }{g}^{\prime }(s\left(y\right),x\left)\right)$$ $$=\frac{1}{p}{\theta }^{\prime \prime }(\lambda y\alpha x.{\chi }_{s\left(y\right)\in \alpha }{g}^{\prime }(s\left(y\right),x\left)\right)$$ Now we use the endofunction condition on ${\theta }^{\prime \prime }$ to get $$\le \frac{1}{p}(p{\Theta }_1+(1-p\left){\Theta }_2\right)(\lambda yx.g^{\prime }(y,x\left)\right)$$ $$=({\Theta }_1+\frac{1-p}{p}{\Theta }_2)(\lambda yx.g^{\prime }(y,x\left)\right)$$ $$={\Theta }_1(\lambda yx.g^{\prime }(y,x\left)\right)+\frac{1-p}{p}{\Theta }_2(\lambda yx.g^{\prime }(y,x\left)\right)$$ And then we use that ${\Theta }_1$ is supported on ${\Psi }_1$ and ${\Theta }_2$ is supported on ${\Psi }_2$, and on ${\Psi }_1$, $g^{\prime }=g$, and on ${\Psi }_2$, $g^{\prime }=0$, to get $$={\Theta }_1(\lambda yx.g(y,x\left)\right)+\frac{1-p}{p}{\Theta }_2\left(\lambda yx.0\right)$$ $$={\Theta }_1(\lambda yx.g(y,x\left)\right)$$ And we're done! The endofunction condition goes through, which is the last piece of the proof we needed. $■$

Proposition 2.14: Consider some $\Gamma$, $\Phi$, $\Theta \in {\square }^c(\Gamma \times \Phi )$ and $F\subseteq \Gamma$. Let ${\cap }_F:2^{\Gamma }\to 2^{\Gamma }$ be defined by ${\cap }_F\left(\alpha \right):=F\cap \alpha$. Then, $${\text{Br}}_{\Gamma }(\Theta \cap {\top }_{F\times \Phi })=({\text{id}}_{\Gamma }\times {\cap }_F\times {\text{id}}_{\Phi }{)}_{\ast }({\text{Br}}_{\Gamma }\left(\Theta \right)\cap {\top }_{F\times 2^{\Gamma }\times \Phi })$$ Moreover, let $\iota :{\Gamma }^{\prime }\to \Gamma$ be an injection and ${\text{el}}^{\iota }:{\text{el}}^{{\Gamma }^{\prime }}\to {\text{el}}^{\Gamma }$ be the injection induced by $\iota$. Then, $${\text{Br}}_{{\Gamma }^{\prime }}\left(\right(\iota \times {\text{id}}_{\Phi }{)}^{\ast }(\Theta \cap {\top }_{im\left(\iota \right)\times \Phi }))=({\text{el}}^{\iota }\times {\text{id}}_{\Phi }{)}^{\ast }{\text{Br}}_{\Gamma }(\Theta \cap {\top }_{im\left(\iota \right)\times \Phi })$$

We'll have to prove both directions separately. Notice that for our proofs so far, they involve transforming one side of the equation to a certain form, then there's a critical step in the middle that's tricky to show, then we just transform back down. So our first step will be unpacking the two sides of the equation up to the critical inequality.

Also, intersecting with the top distribution corresponding to a particular set is the same as the raw-update on that set, we'll use that. We'll suppress identity functions and unused coordinates for $\top$ in the notation, so if some coordinate isn't mentioned, assume it's either the identity function for pushforwards, or that the set for $\top$ is the specified set times the entire space for unmentioned coordinates. With that notational note, we have $${\text{Br}}_{\Gamma }(\Theta \cap {\top }_{F\times \Phi })(\lambda y\alpha x.f(y,x,\alpha \left)\right)$$ Suppressing notation $$=\text{Br}(\Theta \cap {\top }_F)(\lambda y\alpha x.f(y,x,\alpha \left)\right)$$ And rewriting the bridge transform, $$=\underset{\theta \in \text{Br}(\Theta \cap {\top }_F)}{max}\theta (\lambda y\alpha x.f(y,x,\alpha \left)\right)$$ This is our unpacking in one direction.

In the other direction, we have $$({\text{id}}_{\Gamma }\times {\cap }_F\times {\text{id}}_{\Phi }{)}_{\ast }({\text{Br}}_{\Gamma }\left(\Theta \right)\cap {\top }_{F\times 2^{\Gamma }\times \Phi }\left)\right(\lambda y\alpha x.f(y,x,\alpha ))$$ Suppress some notation, $$=\left({\cap }_F{)}_{\ast }\right(\text{Br}\left(\Theta \right)\cap {\top }_F\left)\right(\lambda y\alpha x.f(y,x,\alpha ))$$ Unpack the pushforward and intersection $$=\left(\text{Br}\right(\Theta )\cap {\top }_F)(\lambda y\alpha x.f(y,x,\alpha \cap F\left)\right)$$ $$=\text{Br}\left(\Theta \right)(\lambda y\alpha x.{\chi }_{y\in F}f(y,x,\alpha \cap F\left)\right)$$ And unpack the bridge transform $$=\underset{{\theta }^{\prime }\in \text{Br}\left(\Theta \right)}{max}{\theta }^{\prime }(\lambda y\alpha x.{\chi }_{y\in F}f(y,x,\alpha \cap F\left)\right)$$ Pack back up $$=\underset{{\theta }^{\prime }\in \text{Br}\left(\Theta \right)}{max}({\theta }^{\prime }\cap {\top }_F)(\lambda y\alpha x.f(y,x,\alpha \cap F\left)\right)$$ $$=\underset{{\theta }^{\prime }\in {\text{Br}}_{\Gamma }\left(\Theta \right)}{max}\left({\cap }_F{)}_{\ast }\right({\theta }^{\prime }\cap {\top }_F\left)\right(\lambda y\alpha x.f(y,x,\alpha ))$$ So, our goal to show equality overall is to establish the equality $$\underset{\theta \in \text{Br}(\Theta \cap {\top }_F)}{max}\theta (\lambda y\alpha x.f(y,x,\alpha \left)\right)$$ $$=\underset{{\theta }^{\prime }\in \text{Br}\left(\Theta \right)}{max}\left({\cap }_F{)}_{\ast }\right({\theta }^{\prime }\cap {\top }_F\left)\right(\lambda y\alpha x.f(y,x,\alpha ))$$ This can be done by establishing the following two things. First, is, if ${\theta }^{\prime }\in \text{Br}\left(\Theta \right)$, then $\left({\cap }_F{)}_{\ast }\right({\theta }^{\prime }\cap {\top }_F)\in \text{Br}(\Theta \cap {\top }_F)$. That establishes the $\ge$ inequality direction.

For the reverse direction, we'll need to show that for any $\theta \in \text{Br}(\Theta \cap {\top }_F)$, $\theta$ also lies in $\text{Br}\left(\Theta \right)$, and that $\left({\cap }_F{)}_{\ast }\right(\theta \cap {\top }_F)=\theta$. This establishes the $\le$ inequality direction, since any choice of $\theta$ for the left hand side can be duplicated on the right hand side.

Let's switch our proof target to showing these two things. First off, assume ${\theta }^{\prime }\in \text{Br}\left(\Theta \right)$. The goal is to show that $\left({\cap }_F{)}_{\ast }\right({\theta }^{\prime }\cap {\top }_F)\in \text{Br}(\Theta \cap {\top }_F)$

For once, the support condition is not entirely trivial. However, notice that ${\theta }^{\prime }\cap {\top }_F$ always has $y\in F$ holding (because we updated) and $y\in \alpha$ always holds (because ${\theta }^{\prime }$ fulfills the support condition due to being in $\text{Br}\left(\Theta \right)$). So, it's guaranteed that $y\in \alpha \cap F$. Then, applying the pushforward that turns $\alpha$ into $\alpha \cap F$ doesn't change that there's a guarantee that $y$ lies in the set it's paired with.

Now for the endofunction condition. $$\left({\cap }_F{)}_{\ast }\right({\theta }^{\prime }\cap {\top }_F\left)\right(\lambda y\alpha x.{\chi }_{s\left(y\right)\in \alpha }g\left(s\right(y),x))$$ $$=({\theta }^{\prime }\cap {\top }_F)(\lambda y\alpha x.{\chi }_{s\left(y\right)\in \alpha \cap F}g(s\left(y\right),x\left)\right)$$ $$={\theta }^{\prime }(\lambda y\alpha x.{\chi }_{y\in F}{\chi }_{s\left(y\right)\in \alpha \cap F}g(s\left(y\right),x\left)\right)$$ $$\le {\theta }^{\prime }(\lambda y\alpha x.{\chi }_{s\left(y\right)\in \alpha \cap F}g(s\left(y\right),x\left)\right)={\theta }^{\prime }(\lambda y\alpha x.{\chi }_{s\left(y\right)\in \alpha }{\chi }_{s\left(y\right)\in F}g(s\left(y\right),x\left)\right)$$ $$\le \Theta \left(\lambda yx{\chi }_{y\in F}g\right(y,x\left)\right)=(\Theta \cap {\top }_F)(\lambda yx.g(y,x\left)\right)$$ And we're done, that half of the proof works out.

Now for the reverse direction, establishing that for any $\theta \in \text{Br}(\Theta \cap {\top }_F)$, $\theta$ also lies in $\text{Br}\left(\Theta \right)$, and that $\left({\cap }_F{)}_{\ast }\right(\theta \cap {\top }_F)=\theta$.

The first part of this is easy. $$\theta (\lambda y\alpha x.{\chi }_{s\left(y\right)\in \alpha }g(s\left(y\right),x\left)\right)\le (\Theta \cap {\top }_F)(\lambda yx.g(y,x\left)\right)$$ $$=\Theta (\lambda yx.{\chi }_{y\in F}g(y,x\left)\right)\le \Theta (\lambda yx.g(y,x\left)\right)$$ And we're done. For the second part, it's a bit trickier. In short, what happens is that a piece of measure from $\theta$ is deleted if $y\notin F$, and then $\alpha$ gets mapped to $\alpha \cap F$. So, if we knew that $\theta$ was supported on $F\times 2^F$, we'd know that neither of the two transformations do anything whatsoever, and so you just get $\theta$ out again.

So, let's show that $\theta \in \text{Br}(\Theta \cap {\top }_F)$ is supported on $F\times 2^F$. For this, the way we do it is use Proposition 2.7 to get an upper bound on the bridge transformation, and show that said upper bound is also supported on $F\times 2^F$. By proposition 2.7, $$\text{Br}(\Theta \cap {\top }_F)\subseteq \left(\right(\Theta \cap {\top }_F)⋉{\text{sus}}^{\Theta \cap {\top }_F}{)}^{\downarrow }$$ The downwards arrow means that we're passing from larger subsets to smaller subsets, so it doesn't matter if we remove that, it won't affect whether the support is a subset of $F\times 2^F$. Clearly, $\Theta \cap {\top }_F$ is supported on $F$. And, for sus, we have $${\text{sus}}^{\Theta \cap {\top }_F}\left(x\right)=\left\{y|\right(y,x)\in \text{supp}(\Theta \cap {\top }_F\left)\right\}$$ So clearly it can only produce sets of $y$ which are subsets of $F$ since that's an upper bound on the support of $\Theta \cap {\top }_F$. So we have support on $F\times 2^F$, and we're done with this half of the theorem.

So now we move onto the second half of the theorem with the injections. Without loss of generality, we can reduce this problem to a slightly simpler form, where we assume that $\Theta$ is supported over $im\left(\iota \right)$. This is because any $\Theta$ supported over $im\left(\iota \right)$ has $\Theta \cap {\top }_{im\left(\iota \right)}=\Theta$, and also for any ${\Theta }^{\prime }$, ${\Theta }^{\prime }\cap {\top }_{im\left(\iota \right)}$ is always supported over $im\left(\iota \right)$.

Accordingly, assume that $\Theta$ is supported over $im\left(\iota \right)$. Suppressing identity functions, our goal is to prove that $${\text{Br}}_F\left(\right(\iota {)}^{\ast }\Theta )=({\text{el}}^{\iota }{)}^{\ast }{\text{Br}}_{\Gamma }\left(\Theta \right)$$ This is suprisingly aggravating to prove. Again, we'll try to rewrite things until we get to a point where there's just one equality to show, and then put in the work of showing the endofunction condition in both directions. Time to start rewriting. Subscripts $F$ will be used to denote when a particular $y$ is part of $F$, or of $\Gamma$. Similar with $2^F$ and $2^{\Gamma }$. $${\text{Br}}_F\left(\right(\iota {)}^{\ast }\Theta \left)\right(\lambda y_F{\alpha }_{F}x.f(y_F,x,{\alpha }_F))$$ $$=\underset{{\theta }_F\in {\text{Br}}_F\left(\right(\iota {)}^{\ast }\Theta )}{max}{\theta }_F(\lambda y_F{\alpha }_{F}x.f(y_F,x,{\alpha }_F\left)\right)$$ Rewriting the other direction, we have $$\left({\text{el}}^{\iota }{)}^{\ast }{\text{Br}}_{\Gamma }\right(\Theta \left)\right(\lambda y_F{\alpha }_{F}x.f(y_F,x,{\alpha }_F))$$ Now, for pullback, it's defined like this. Maximum over the empty set is 0. $$={\text{Br}}_{\Gamma }\left(\Theta \right)(\lambda y\alpha x.\underset{y_F,{\alpha }_F\in \left({\text{el}}^{\iota }{)}^{-1}\right(y,\alpha )}{max}f(y_F,x,{\alpha }_F\left)\right)$$ $$=\underset{\theta \in {\text{Br}}_{\Gamma }\left(\Theta \right)}{max}\theta (\lambda y\alpha x.\underset{y_F,{\alpha }_F\in \left({\text{el}}^{\iota }{)}^{-1}\right(y,\alpha )}{max}f(y_F,x,{\alpha }_F\left)\right)$$ $$=\underset{\theta \in {\text{Br}}_{\Gamma }\left(\Theta \right)}{max}\left({\text{el}}^{\iota }{)}^{\ast }\right(\theta \left)\right(\lambda y_F{\alpha }_{F}x.f(y_F,x,{\alpha }_F))$$ And so we now must embark on showing these two things are equal, by showing that every value that one of the maxes is capable of producing, the other is capable of producing too. Our proof goal is $$\underset{{\theta }_F\in {\text{Br}}_F\left(\right(\iota {)}^{\ast }\Theta )}{max}{\theta }_F(\lambda y_F{\alpha }_{F}x.f(y_F,x,{\alpha }_F\left)\right)=\underset{\theta \in {\text{Br}}_{\Gamma }\left(\Theta \right)}{max}\left({\text{el}}^{\iota }{)}^{\ast }\right(\theta \left)\right(\lambda y_F{\alpha }_{F}x.f(y_F,x,{\alpha }_F))$$ Now, for one direction of this, we need to show that if $\theta \in {\text{Br}}_{\Gamma }\left(\Theta \right)$, then $\left({\text{el}}^{\iota }{)}^{\ast }\right(\theta )\in {\text{Br}}_F(\left(\iota {)}^{\ast }\Theta \right)$.

The support condition is easily fulfilled, because the only time the pullback works is when $y,\alpha \in im\left({\text{el}}^{\iota }\right)$, and $\iota$ is an injection, so there's a unique preimage point $y_F,{\alpha }_F$, and since $y\in F$ occurs always,then $y_F\in {\alpha }_F$ occurs always. That leaves the endofunction condition. Let $s_F:F\to F$, $g_F:F\times \Phi \to [0,1]$. Let $s^{\prime }$ be defined as follows. For points in $im\left(\iota \right)$, it maps $y$ to $\iota \left(s_F\right({\iota }^{-1}\left(y\right)\left)\right)$. Everywhere else, it's the identity. Also, $g^{\prime }$, for points in $im\left(\iota \right)$, maps $y,x$ to $g\left({\iota }^{-1}\right(y),x)$, and is 0 everywhere else. Both of these are uniquely defined because $\iota$ is an injection. We have $$\left({\text{el}}^{\iota }{)}^{\ast }\right(\theta \left)\right(\lambda y_F{\alpha }_{F}x:{\chi }_{s_F\left(y_F\right)\in {\alpha }_F}{g}_F\left(s_F\right(y_F),x))$$ $$=\theta (\lambda y\alpha x:\underset{y_F,{\alpha }_F\in \left({\text{el}}^{\iota }{)}^{-1}\right(y,\alpha )}{max}{\chi }_{s_F\left(y_F\right)\in {\alpha }_F}{g}_F(s_F\left(y_F\right),x\left)\right)$$ We can partially write the maximum as an indicator function for checking whether $y\in im\left(\iota \right)$ and $\alpha \subseteq im\left(\iota \right)$ (because in such a case the maximum is taken over an empty set and 0 is returned in those cases). And also, since there's only one point in that inverse, since $\iota$ is an injection, there's a canonical inverse and we can swap everything out for that, yielding $$=\theta (\lambda y\alpha x:{\chi }_{y\in im\left(\iota \right)\wedge \alpha \subseteq im\left(\iota \right)}{\chi }_{s_F\left({\iota }^{-1}\right(y\left)\right)\in {\iota }^{-1}\left(\alpha \right)}{g}_F(s_F\left({\iota }^{-1}\right(y\left)\right),x\left)\right)$$ Now, since $\iota$ is an injection, applying it to the point and the set in the indicator function don't affect whether the point is in the relevant set, so we can go $$=\theta (\lambda y\alpha x:{\chi }_{y\in im\left(\iota \right)\wedge \alpha \subseteq im\left(\iota \right)}{\chi }_{\iota \left(s_F\right({\iota }^{-1}\left(y\right)\left)\right)\in \iota \left({\iota }^{-1}\right(\alpha \left)\right)}{g}_F(s_F\left({\iota }^{-1}\right(y\left)\right),x\left)\right)$$ And we can also apply $\iota$ and ${\iota }^{-1}$ to the point in the $g_F$ function, as that's just identity. $$=\theta (\lambda y\alpha x:{\chi }_{y\in im\left(\iota \right)\wedge \alpha \subseteq im\left(\iota \right)}{\chi }_{\iota \left(s_F\right({\iota }^{-1}\left(y\right)\left)\right)\in \iota \left({\iota }^{-1}\right(\alpha \left)\right)}{g}_F({\iota }^{-1}\left(\iota \right(s_F\left({\iota }^{-1}\right(y\left)\right)\left)\right),x\left)\right)$$ Use our $s^{\prime }$ and $g^{\prime }$ abbreviations since we know that the relevant point is in $im\left(\iota \right)$ if it made it past the indicator function. Also do some canceling out of identity functions around the $\alpha$. $$=\theta (\lambda y\alpha x:{\chi }_{y\in im\left(\iota \right)\wedge \alpha \subseteq im\left(\iota \right)}{\chi }_{s^{\prime }\left(y\right)\in \alpha }{g}_F({\iota }^{-1}\left(s^{\prime }\right(y\left)\right),x\left)\right)$$ And use our abbreviation of $g^{\prime }$ $$=\theta (\lambda y\alpha x:{\chi }_{y\in im\left(\iota \right)\wedge \alpha \subseteq im\left(\iota \right)}{\chi }_{s^{\prime }\left(y\right)\in \alpha }{g}^{\prime }(s^{\prime }\left(y\right),x\left)\right)$$ Remove the indicator function $$\le \theta (\lambda y\alpha x:{\chi }_{s^{\prime }\left(y\right)\in \alpha }{g}^{\prime }(s^{\prime }\left(y\right),x\left)\right)$$ Apply endofunction property $$\le \Theta (\lambda yx.g^{\prime }(y,x\left)\right)$$ Now, $g^{\prime }$ is 0 when $y\notin im\left(\iota \right)$, and is $g_F\left({\iota }^{-1}\right(y),x)$ otherwise, so we have $$=\Theta (\lambda yx.{\chi }_{y\in im\left(\iota \right)}{g}_F({\iota }^{-1}\left(y\right),x\left)\right)$$ $$=\Theta (\lambda yx.\underset{y_F\in {\iota }^{-1}\left(y\right)}{max}{g}_F(y_F,x\left)\right)=\left(\iota {)}^{\ast }\Theta \right(\lambda y_{F}x.g_F(y_F,x))$$ And we're done here, the endofunction condition has been shown, establishing one direction of the inequality.

For the reverse direction, we'll be working on showing that if ${\theta }_F\in {\text{Br}}_F\left(\right(\iota {)}^{\ast }\Theta )$, then $({\text{el}}^{\iota }{)}_{\ast }{\theta }_F\in \text{Br}(\Theta )$, though it will take a little bit of extra work at the end to show how this implies our desired equality. The support property obviously holds, we're just applying $\iota$ to our point and set, so that leaves the endofunction property. $s$ and $g$ are as usual. $$\left({\text{el}}^{\iota }{)}_{\ast }{\theta }_F\right(\lambda y\alpha x.{\chi }_{s\left(y\right)\in \alpha }g\left(s\right(y),x))$$ $$={\theta }_F(\lambda y_F{\alpha }_{F}x.{\chi }_{s\left(\iota \right(y_F\left)\right)\in \iota \left({\alpha }_F\right)}g(s\left(\iota \right(y_F\left)\right),x\left)\right)$$ Now, if $s\left(\iota \right(y_F\left)\right)\in im\left(\iota \right)$, it might pass the indicator function, but if $s\left(\iota \right(y_F\left)\right)\notin im\left(\iota \right)$, it definitely won't. So let's place that indicator function. $$={\theta }_F(\lambda y_F{\alpha }_{F}x.{\chi }_{s\left(\iota \right(y_F\left)\right)\in im\left(\iota \right)}{\chi }_{s\left(\iota \right(y_F\left)\right)\in \iota \left({\alpha }_F\right)}g(s\left(\iota \right(y_F\left)\right),x\left)\right)$$ Now, since we know this stuff is in the image of $\iota$ (and $\iota \left({\alpha }_F\right)$ definitely is), and $\iota$ is an injection, we can safely take the inverse of everything, yielding $$={\theta }_F(\lambda y_F{\alpha }_{F}x.{\chi }_{s\left(\iota \right(y_F\left)\right)\in im\left(\iota \right)}{\chi }_{{\iota }^{-1}\left(s\right(\iota \left(y_F\right)\left)\right)\in {\iota }^{-1}\left(\iota \right({\alpha }_F\left)\right)}g(\iota \left({\iota }^{-1}\right(s\left(\iota \right(y_F\left)\right)\left)\right),x\left)\right)$$ In order, this was because we could reverse the injection as long as we're past that indicator function, reversing the injection doesn't affect whether the point is an element of the set, and $\iota \circ {\iota }^{-1}$ is identity. Cancel out some of the identity.. $$={\theta }_F(\lambda y_F{\alpha }_{F}x.{\chi }_{s\left(\iota \right(y_F\left)\right)\in im\left(\iota \right)}{\chi }_{{\iota }^{-1}\left(s\right(\iota \left(y_F\right)\left)\right)\in {\alpha }_F}g(\iota \left({\iota }^{-1}\right(s\left(\iota \right(y_F\left)\right)\left)\right),x\left)\right)$$ Now, at this point, let $s_F:F\to F$ be defined as $s_F\left(y_F\right)={\iota }^{-1}\left(s\right(\iota \left(y_F\right)\left)\right)$ when $s\left(\iota \right(y_F\left)\right)\in im\left(\iota \right)$, and arbitrary otherwise. And let $g_F$ be defined as $g_F(y_F,x)=g\left(\iota \right(y_F),x)$ Now, using these abbreviations, we can go $$={\theta }_F(\lambda y_F{\alpha }_{F}x.{\chi }_{s\left(\iota \right(y_F\left)\right)\in im\left(\iota \right)}{\chi }_{s_F\left(y_F\right)\in {\alpha }_F}g(\iota \left(s_F\right(y_F\left)\right),x\left)\right)$$ $$={\theta }_F(\lambda y_F{\alpha }_{F}x.{\chi }_{s\left(\iota \right(y_F\left)\right)\in im\left(\iota \right)}{\chi }_{s_F\left(y_F\right)\in {\alpha }_F}{g}_F(s_F\left(y_F\right),x\left)\right)$$ Now we can safely strip away the indicator function. $$\le {\theta }_F(\lambda y_F{\alpha }_{F}x.{\chi }_{s_F\left(y_F\right)\in {\alpha }_F}{g}_F(s_F\left(y_F\right),x\left)\right)$$ And apply the endofunction condition $$\le \left(\iota {)}^{\ast }\right(\Theta \left)\right(\lambda y_{F}x.g_F(y_F,x))$$ Unpacking the pullback, we get $$=\Theta (\lambda yx.\underset{y_F\in {\iota }^{-1}\left(y\right)}{max}{g}_F(y_F,x\left)\right)$$ Now unpack the definition of $g_F$ $$=\Theta (\lambda yx.\underset{y_F\in {\iota }^{-1}\left(y\right)}{max}g(\iota \left(y_F\right),x\left)\right)$$ Use that $\Theta$ is supported on the image of $\iota$, so that max is always nonempty. Then, things cancel out to yield $$=\Theta (\lambda yx.g(y,x\left)\right)$$ And we're done there.

Ok, so... we've shown one inequality direction already, all that remained to be shown was $$\underset{{\theta }_F\in {\text{Br}}_F\left(\right(\iota {)}^{\ast }\Theta )}{max}{\theta }_F(\lambda y_F{\alpha }_{F}x.f(y_F,x,{\alpha }_F\left)\right)\le \underset{\theta \in {\text{Br}}_{\Gamma }\left(\Theta \right)}{max}\left({\text{el}}^{\iota }{)}^{\ast }\right(\theta \left)\right(\lambda y_F{\alpha }_{F}x.f(y_F,x,{\alpha }_F))$$ How does it help to know that for any ${\theta }_F\in {\text{Br}}_F\left(\right(\iota {)}^{\ast }\Theta )$, then $({\text{el}}^{\iota }{)}_{\ast }{\theta }_F\in {\text{Br}}_{\Gamma }(\Theta )$? Well, for any particular ${\theta }_F$ chosen on the left-hand side, you can let the choice of $\theta$ for the right hand side be $({\text{el}}^{\iota }{)}_{\ast }{\theta }_F$, which lies in the appropriate set. Then, the contribution for the right-hand-side would be $\left({\text{el}}^{\iota }{)}^{\ast }\right(\left({\text{el}}^{\iota }{)}_{\ast }\right({\theta }_F\left)\right)$, which happens to be ${\theta }_F$. So anything the left-hand-side can do, the right-hand-side can do as well, showing our one remaining direction of inequality, and concluding the proof.

Well, actually, I should flesh out that claim that $\left({\text{el}}^{\iota }{)}^{\ast }\right(\left({\text{el}}^{\iota }{)}_{\ast }\right({\theta }_F\left)\right)={\theta }_F$. This happens because $$\left({\text{el}}^{\iota }{)}^{\ast }\right(\left({\text{el}}^{\iota }{)}_{\ast }\right({\theta }_F\left)\right)(\lambda y_F{\alpha }_{F}x.f(y_F,x,{\alpha }_F\left)\right)$$ $$=\left({\text{el}}^{\iota }{)}_{\ast }\right({\theta }_F\left)\right(\lambda y\alpha x.{\chi }_{y,\alpha \in {\text{el}}^F}\underset{y_F,{\alpha }_F\in \left({\text{el}}^{\iota }{)}^{-1}\right(y,\alpha )}{max}f(y_F,x,{\alpha }_F))$$ $$={\theta }_F(\lambda y_F{\alpha }_{F}x.{\chi }_{\iota \left(y_F\right),\iota \left({\alpha }_F\right)\in {\text{el}}^F}\underset{y_F^{\prime },{\alpha }_F^{\prime }\in \left({\text{el}}^{\iota }{)}^{-1}\right(\iota \left(y_F\right),\iota \left({\alpha }_F\right))}{max}f(y_F^{\prime },x,{\alpha }_F^{\prime }\left)\right)$$ Now,that initial indicator condition is always true because ${\theta }_F$ is supported on ${\text{el}}^F$, so we have $$={\theta }_F(\lambda y_F{\alpha }_{F}x.\underset{y_F^{\prime },{\alpha }_F^{\prime }\in \left({\text{el}}^{\iota }{)}^{-1}\right(\iota \left(y_F\right),\iota \left({\alpha }_F\right))}{max}f(y_F^{\prime },x,{\alpha }_F^{\prime }\left)\right)$$ And then, since ${\text{el}}^{\iota }$ is injective, applying it then taking the partial inverse is just identity, so we get $$={\theta }_F(\lambda y_F{\alpha }_{F}x.f(y_F,x,{\alpha }_F\left)\right)$$ And that's why we have equality. Alright, proof finally done. $■$

Proposition 2.15: Consider some ${\Gamma }_0$, ${\Gamma }_1$, $r:{\Gamma }_0\to {\Gamma }_1$, $\Phi$, $\Theta \in {\square }^c({\Gamma }_0\times \Phi )$. Let $\iota :{\Gamma }_0\to {\Gamma }_0\times {\Gamma }_1$ be given by $\iota \left(y\right):=(y,r(y\left)\right)$. Then, $${\text{Br}}_{{\Gamma }_0\times {\Gamma }_1}\left(\right(\iota \times {\text{id}}_{\Phi }{)}_{\ast }\Theta )=({\text{el}}^{\iota }\times {\text{id}}_{\Phi }{)}_{\ast }{\text{Br}}_{{\Gamma }_0}\left(\Theta \right)$$

This can be established by Proposition 2.14. Taking proposition 2.14, and using ${\Theta }^{\prime }$ as an abbreviation for $(\iota \times {\text{id}}_{\Phi }{)}_{\ast }\Theta$, and $im\left(\iota \right)$ as the $F$, we get $${\text{Br}}_{{\Gamma }_0\times {\Gamma }_1}({\Theta }^{\prime }\cap {\top }_{im\left(\iota \right)\times \Phi })$$ $$=({\text{id}}_{{\Gamma }_0\times {\Gamma }_1}\times {\cap }_{im\left(\iota \right)}\times {\text{id}}_{\Phi }{)}_{\ast }({\text{Br}}_{{\Gamma }_0\times {\Gamma }_1}\left({\Theta }^{\prime }\right)\cap {\top }_{im\left(\iota \right)\times 2^{\Gamma }\times \Phi })$$ We'll need to abbreviate in a bit, so ignore some of the identity functions to get $${\text{Br}}_{{\Gamma }_0\times {\Gamma }_1}({\Theta }^{\prime }\cap {\top }_{im\left(\iota \right)\times \Phi })$$ $$=\left({\cap }_{im\left(\iota \right)}{)}_{\ast }\right({\text{Br}}_{{\Gamma }_0\times {\Gamma }_1}\left({\Theta }^{\prime }\right)\cap {\top }_{im\left(\iota \right)\times 2^{\Gamma }\times \Phi })$$ Now, deabbreviating, ${\Theta }^{\prime }$ ie $(\iota \times {\text{id}}_{\Phi }{)}_{\ast }\Theta$ is already supported on $im\left(\iota \right)$, so intersecting with ${\top }_{im\left(\iota \right)\times \Phi }$ does nothing. $${\text{Br}}_{{\Gamma }_0\times {\Gamma }_1}({\Theta }^{\prime }\cap {\top }_{im\left(\iota \right)\times \Phi })$$ $$=\left({\cap }_{im\left(\iota \right)}{)}_{\ast }\right({\text{Br}}_{{\Gamma }_0\times {\Gamma }_1}({\Theta }^{\prime }\cap {\top }_{im\left(\iota \right)\times \Phi })\cap {\top }_{im\left(\iota \right)\times 2^{\Gamma }\times \Phi })$$ Now, since ${\Theta }^{\prime }\cap {\top }_{im\left(\iota \right)\times \Phi }$ is onl supported on $im\left(\iota \right)$, the bridge transform will only be supported on ${\text{el}}^{im\left(\iota \right)}$. So, we can pull back along the function ${\text{el}}^{\iota }$ and pushforward and it will be identity, as our ultracontribution is entirely supported on the area that can be pulled back. So, we get $${\text{Br}}_{{\Gamma }_0\times {\Gamma }_1}({\Theta }^{\prime }\cap {\top }_{im\left(\iota \right)\times \Phi })$$ $$=\left({\cap }_{im\left(\iota \right)}{)}_{\ast }\right(({\text{el}}^{\iota }\times {\text{id}}_{\Phi }{)}_{\ast }(({\text{el}}^{\iota }\times {\text{id}}_{\Phi }{)}^{\ast }({\text{Br}}_{{\Gamma }_0\times {\Gamma }_1}({\Theta }^{\prime }\cap {\top }_{im\left(\iota \right)\times \Phi })\left)\right)\cap {\top }_{im\left(\iota \right)\times 2^{\Gamma }\times \Phi })$$ Applying the second part of Proposition 2.14, this can be rewritten as $${\text{Br}}_{{\Gamma }_0\times {\Gamma }_1}({\Theta }^{\prime }\cap {\top }_{im\left(\iota \right)\times \Phi })$$ $$=\left({\cap }_{im\left(\iota \right)}{)}_{\ast }\right(({\text{el}}^{\iota }\times {\text{id}}_{\Phi }{)}_{\ast }({\text{Br}}_{{\Gamma }_0}\left(\right(\iota \times {\text{id}}_{\Phi }{)}^{\ast }({\Theta }^{\prime }\cap {\top }_{im\left(\iota \right)\times \Phi })\left)\right)\cap {\top }_{im\left(\iota \right)\times 2^{\Gamma }\times \Phi })$$ Since ${\Theta }^{\prime }$ deabbreviates as $(\iota \times {\text{id}}_{\Phi }{)}_{\ast }\Theta$, it's supported on $im\left(\iota \right)$, so intersecting with $im\left(\iota \right)$ does nothing. Getting rid of that part, and deabbreviating, we get $${\text{Br}}_{{\Gamma }_0\times {\Gamma }_1}\left(\right(\iota \times {\text{id}}_{\Phi }{)}_{\ast }\Theta )$$ $$=\left({\cap }_{im\left(\iota \right)}{)}_{\ast }\right(({\text{el}}^{\iota }\times {\text{id}}_{\Phi }{)}_{\ast }({\text{Br}}_{{\Gamma }_0}\left(\right(\iota \times {\text{id}}_{\Phi }{)}^{\ast }\left(\right(\iota \times {\text{id}}_{\Phi }{)}_{\ast }\Theta \left)\right))\cap {\top }_{im\left(\iota \right)\times 2^{\Gamma }\times \Phi })$$ Now, since $\iota$ is an injection, pushforward-then-pullback is identity, so we get $${\text{Br}}_{{\Gamma }_0\times {\Gamma }_1}\left(\right(\iota \times {\text{id}}_{\Phi }{)}_{\ast }\Theta )$$ $$=\left({\cap }_{im\left(\iota \right)}{)}_{\ast }\right(({\text{el}}^{\iota }\times {\text{id}}_{\Phi }{)}_{\ast }({\text{Br}}_{{\Gamma }_0}\left(\Theta \right))\cap {\top }_{im\left(\iota \right)\times 2^{\Gamma }\times \Phi })$$ Then, since the pushforward through ${\text{el}}^{\iota }$ is supported on $im\left(\iota \right)$, the intersection does nothing $${\text{Br}}_{{\Gamma }_0\times {\Gamma }_1}\left(\right(\iota \times {\text{id}}_{\Phi }{)}_{\ast }\Theta )=({\cap }_{im\left(\iota \right)}{)}_{\ast }\left(\right({\text{el}}^{\iota }\times {\text{id}}_{\Phi }{)}_{\ast }\left({\text{Br}}_{{\Gamma }_0}\Theta \right))$$ Then note that any set pushed forward through ${\text{el}}^{\iota }$ must be a subset of $im\left(\iota \right)$, so intersecting with $im\left(\iota \right)$ does nothing, and we get $${\text{Br}}_{{\Gamma }_0\times {\Gamma }_1}\left(\right(\iota \times {\text{id}}_{\Phi }{)}_{\ast }\Theta )=({\text{el}}^{\iota }\times {\text{id}}_{\Phi }{)}_{\ast }\left({\text{Br}}_{{\Gamma }_0}\Theta \right)$$ And the result is proven. $■$