Proof of Kit for def:random-element-law-metric

Throughout, formulas are written with abbreviations as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (vi), a formula being predicative when it is so with its abbreviations eliminated, and routine facts about sets, maps and predicative formulas are used without comment (Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity (i), Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity (iii), Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity (v)), and so is the agreement with the current versions of the earlier versions of the definitions of metric spaces and Borel $\sigma$-algebras that a cited item uses (The Earlier and the New Versions of the Definitions of Metric Spaces, Convergence, Continuity and Compactness Agree (i), The Earlier and the New Versions of the Definitions of σ-Algebras, Measures, Measurable Functions and Integrals Agree (ii)). We choose further set variables $x_{N},x_{N+1},\dots$, so that $x_{0},\dots,x_{9}$ are distinct also when $N<10$, then set variables $B$, $w$, $w'$, $v$, $u$, $y$ and the bound variables below, all of these distinct and other than the seventeen parameters, which are at their fixed values (Conditions Expressed by a Predicative Formula, and Guards (i)). A formula taken from another item is used, by renaming, at the variables named, its bound variables chosen other than all of these and its parameters being the parameters of the statement with the same values.

The two random elements. Apply Kit for def:probability-space-random-variable (iv) with its $N$ equal to $10$, its variables $x_{0},\dots,x_{9}$ being ours and its seventeen parameters being those of the statement, which have the values and kinds that kit prescribes: once with its indices $i,j,k,l,m,p$ equal to $0,1,2,6,7,8$, and once with them equal to $3,4,5,6,7,9$. This gives predicative formulas $\rho_{1}$ and $\rho_{2}$ in $x_{0},\dots,x_{9}$, taken at our variables, $x_{6}$, $x_{7}$ among them, by renaming, such that, for sets $\Omega,\mathcal{F},P,\Omega',\mathcal{F}',P',S,d,X,Y$ assigned to $x_{0},\dots,x_{9}$, $\rho_{1}$ holds if and only if $(\Omega,\mathcal{F})$ is a measurable space, $P$ is a measure on it, $(\Omega,\mathcal{F},P)$ is a probability space, $d:S\times S\to\mathbb{R}$ is a map, $(S,d)$ is a metric space and $X$ is a random element of $S$ on $(\Omega,\mathcal{F},P)$; and $\rho_{2}$ holds if and only if the same is true of $(\Omega',\mathcal{F}',P')$, $S$, $d$ and $Y$. So $\rho_{1}\wedge\rho_{2}$ expresses every part of the condition of (i), at the positions $0,\dots,9$, except that $X$ and $Y$ are identically distributed.

Borel sets. By Borel Sets of a Variable Metric Space as a Predicative Condition, and the Families of σ-Algebras Generated by Random Elements and of Their Composites (v), with its set variables $B$, $S$ and $d$ taken to be $B$, $x_{6}$ and $x_{7}$ by renaming, there is a predicative formula $\mathrm{bo}(B,x_{6},x_{7})$ expressing "$(x_{6},x_{7})$ is a metric space and $B\in\mathcal{B}(x_{6},x_{7})$", with the Borel $\sigma$-algebra $\mathcal{B}(x_{6},x_{7})$. The parameters $\mathbb{R}$, $\le$, $<$, $+$, $0$ and $\mathbb{N}$ of that clause have, in this order, the values of the parameters $\mathbb{R}$, $\le_{\mathbb{R}}$, $<_{\mathbb{R}}$, $+_{\mathbb{R}}$, $0_{\mathbb{R}}$ and $\mathbb{N}$ of the statement: for the first five both statements say so, and the value of our $\mathbb{N}$ is the set $\mathbb{N}$ of Sums of Sequences in [0,∞] as Typed Terms and as a Map (i), the set of natural numbers, which is the set $\mathbb{N}$ of The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (ii) that the clause uses. So, for sets $S$ and $d$ such that $d:S\times S\to\mathbb{R}$ is a map and $(S,d)$ is a metric space, and for every set $B$, $\mathrm{bo}(B,S,d)$ holds if and only if $B\in\mathcal{B}(S)$.

Equality of the laws. Let

$$\lambda=\forall B\,\forall w\,\forall w'\,\forall v\,\Bigl(\bigl(\mathrm{bo}(B,x_{6},x_{7})\wedge\forall u\,(u\in w\Leftrightarrow\exists y\,(y\in B\wedge(u,y)\in x_{8}))\wedge\forall u\,(u\in w'\Leftrightarrow\exists y\,(y\in B\wedge(u,y)\in x_{9}))\wedge(w,v)\in x_{2}\bigr)\Rightarrow(w',v)\in x_{5}\Bigr).$$

The formulas $(u,y)\in x_{8}$, $(u,y)\in x_{9}$, $(w,v)\in x_{2}$ and $(w',v)\in x_{5}$ are predicative (Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iii)), and so is $\mathrm{bo}$; as every quantifier added is over a set variable, $\lambda$ is predicative (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (v)), with free variables among $x_{2},x_{5},x_{6},x_{7},x_{8},x_{9}$ and the parameters. Let

$$\delta=\rho_{1}\wedge\rho_{2}\wedge\lambda,$$

a predicative formula in $x_{0},\dots,x_{9}$.

Let sets $\Omega,\mathcal{F},P,\Omega',\mathcal{F}',P',S,d,X,Y$ be assigned to $x_{0},\dots,x_{9}$. If $\rho_{1}$ or $\rho_{2}$ fails, then $\delta$ fails, and so does the condition of (i) at the positions $0,\dots,9$. Let $\rho_{1}$ and $\rho_{2}$ hold. We show that $\lambda$ holds if and only if

$$P\bigl(X^{-1}(B)\bigr)=P'\bigl(Y^{-1}(B)\bigr)\qquad\text{for every }B\in\mathcal{B}(S).$$

Fix a set $B$. If $B\notin\mathcal{B}(S)$, then $\mathrm{bo}(B,S,d)$ fails, as shown above, and the implication in $\lambda$ holds for this $B$ whatever $w$, $w'$ and $v$ are. Let $B\in\mathcal{B}(S)$. As $X:\Omega\to S$ is $\mathcal{F}/\mathcal{B}(S)$-measurable (Probability Spaces, Events and Random Elements (iii)), its preimage $X^{-1}(B)$ belongs to $\mathcal{F}$ (Measurable Map, and the Set of Measurable Maps (i)). For a set $u$, $\exists y\,(y\in B\wedge(u,y)\in X)$ holds if and only if $u\in\Omega$ and $X(u)\in B$, by the value form of a map, that is, if and only if $u\in X^{-1}(B)$, by the description of preimages; so the only set $w$ satisfying the second conjunct of the antecedent is $X^{-1}(B)$. Likewise the only set $w'$ satisfying the third is $Y^{-1}(B)$, an element of $\mathcal{F}'$. As $P:\mathcal{F}\to[0,\infty]$ and $P':\mathcal{F}'\to[0,\infty]$ are maps (Measure, Measure Space, and Probability Measure (i)), $(X^{-1}(B),v)\in P$ holds if and only if $v=P(X^{-1}(B))$, and $(Y^{-1}(B),v)\in P'$ if and only if $v=P'(Y^{-1}(B))$, by the value form of a map. So, for this $B$, the part of $\lambda$ after $\forall B$ says that the set $v=P(X^{-1}(B))$ satisfies $v=P'(Y^{-1}(B))$, that is, $P(X^{-1}(B))=P'(Y^{-1}(B))$. This proves the equivalence.

By The Law of a Random Element (i), the law $P_{X}$ is the image measure $P\circ X^{-1}$, the map $P_{X}:\mathcal{B}(S)\to[0,\infty]$ with

$$P_{X}(B)=P\bigl(X^{-1}(B)\bigr)\qquad(B\in\mathcal{B}(S)),$$

and likewise $P'_{Y}:\mathcal{B}(S)\to[0,\infty]$ is the map with $P'_{Y}(B)=P'(Y^{-1}(B))$. By extensionality of maps, two maps on $\mathcal{B}(S)$ with the same value at every $B\in\mathcal{B}(S)$ are equal, and equal maps have the same values. So $\lambda$ holds if and only if $P_{X}=P'_{Y}$, that is, by The Law of a Random Element (ii), if and only if $X$ and $Y$ are identically distributed. Hence $\delta$ expresses the condition of (i) with $\Omega,\mathcal{F},P,\Omega',\mathcal{F}',P',S,d,X,Y=x_{0},\dots,x_{9}$.

Identically distributed random elements. By renaming, with ten variables renamed and $\sigma(0),\dots,\sigma(9)$ equal to $i,j,k,l,m,p,q,r,s,t$, the formula $\delta(x_{i},x_{j},x_{k},x_{l},x_{m},x_{p},x_{q},x_{r},x_{s},x_{t})$ is a predicative formula in $x_{0},\dots,x_{N-1}$ that holds, under every assignment of sets to $x_{0},\dots,x_{N-1}$, if and only if $\delta$ holds with $x_{0},\dots,x_{9}$ assigned the sets assigned to $x_{i},x_{j},x_{k},x_{l},x_{m},x_{p},x_{q},x_{r},x_{s},x_{t}$, that is, if and only if the condition of (i) holds. This proves (i).