Proof of Kit for def:weak-convergence-measures-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 the given $x_{0},\dots,x_{q-1}$ are the first of distinct set variables $x_{0},x_{1},\dots$ as in Renaming and Substituting Variables in Predicative Formulas, so that $x_{0},\dots,x_{4}$ are distinct also when $q<5$. The letters $S$, $d$, $s$ and $\mu$ denote $x_{0}$, $x_{1}$, $x_{2}$ and $x_{3}$; every other letter used below as a variable denotes a further set variable, these being distinct from one another, from $x_{0},x_{1},\dots$ and from the parameters, and bound variables of formulas taken from other results are renamed where necessary so that none is captured. Routine facts about maps and predicative formulas are used without comment (Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity (iii), Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity (v), Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (v)), and so is the agreement of the earlier versions of definitions read by published results cited below with their current versions (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 Metric Spaces, Convergence, Continuity and Compactness Agree (vii), The Earlier and the New Versions of the Definitions of Sequences, Limits, Cauchy Sequences, Series and Iterated Operations Agree (i), The Earlier and the New Versions of the Definitions of Sequences, Limits, Cauchy Sequences, Series and Iterated Operations Agree (ii), The Earlier and the New Versions of the Definitions of σ-Algebras, Measures, Measurable Functions and Integrals Agree (i), The Earlier and the New Versions of the Definitions of σ-Algebras, Measures, Measurable Functions and Integrals Agree (ii), The Earlier and the New Versions of the Definitions of σ-Algebras, Measures, Measurable Functions and Integrals Agree (iii), The Earlier and the New Versions of the Definitions of σ-Algebras, Measures, Measurable Functions and Integrals Agree (iv), The Earlier and the New Versions of the Definitions of σ-Algebras, Measures, Measurable Functions and Integrals Agree (v), The Earlier and the New Versions of the Definitions of σ-Algebras, Measures, Measurable Functions and Integrals Agree (vi)).

Metric spaces and Borel $\sigma$-algebras. 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 (i) there is a predicative formula $\rho(S,d)$, with free variables among $S$, $d$ and the parameters, that holds if and only if $(S,d)$ is a metric space, and 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) a predicative formula $b(B,S,d)$ that holds if and only if $(S,d)$ is a metric space and $B\in\mathcal{B}(S,d)$. Let

$$\beta(S,d,F)=\forall B\,\bigl(B\in F\Leftrightarrow b(B,S,d)\bigr).$$

Let sets $S$ and $d$ be such that $(S,d)$ is a metric space. Its Borel $\sigma$-algebra $\mathcal{B}(S)=\mathcal{B}(S,d)=\sigma(\mathcal{T}_{d})$ is a set (The σ-Algebra Generated by a Set of Subsets (i)) and a $\sigma$-algebra on $S$ (Closure Properties of σ-Algebras, Intersections and Traces of σ-Algebras, and the Generated σ-Algebra (iii)), so $(S,\mathcal{B}(S))$ is a measurable space; and by the axiom of extensionality, a set $F$ satisfies $\beta(S,d,F)$ if and only if $F=\mathcal{B}(S)$. In the same way $\mathcal{B}(\mathbb{R})$, the Borel $\sigma$-algebra $\sigma(\mathcal{T}_{d_{\mathbb{R}}})$ of the metric space $(\mathbb{R},d_{\mathbb{R}})$ (Borel Sigma-Algebra of a Metric Space (ii), Borel Sigma-Algebra of a Metric Space (i)), is a $\sigma$-algebra on $\mathbb{R}$ (Closure Properties of σ-Algebras, Intersections and Traces of σ-Algebras, and the Generated σ-Algebra (iii)), so that $(\mathbb{R},\mathcal{B}(\mathbb{R}))$ is a measurable space.

Finite measures. By Kit for def:measure-measure-space (iv), with its $n$ equal to $3$ and its $i$, $j$, $k$ equal to $0$, $1$, $2$, and Renaming and Substituting Variables in Predicative Formulas (i), there is a predicative formula $\varphi(S,F,\mu)$ that holds if and only if $(S,F)$ is a measurable space and $\mu$ is a finite measure on it. Let $\Phi$ be the formula of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (vi) and

$$\eta(S,F,s)=\Phi(s)\wedge\forall p\,\bigl(p\in\mathbb{N}\Leftrightarrow\exists e\,((p,e)\in s)\bigr)\wedge\forall p\,\forall e\,\bigl((p,e)\in s\Rightarrow\varphi(S,F,e)\bigr).$$

Let $(S,d)$ be a metric space and $F=\mathcal{B}(S)$. By Kit for def:measure-measure-space (x), the finite measures on $(S,\mathcal{B}(S))$ form a set $\mathcal{M}_{\mathrm{fin}}$, a subset of $[0,\infty]^{\mathcal{B}(S)}$, so that for a set $e$, $\varphi(S,F,e)$ holds if and only if $e\in\mathcal{M}_{\mathrm{fin}}$. Write $\mu_{\mathrm{map}}$ for the formula $\mu$ of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (vii). Hence $\eta(S,F,s)$ holds exactly when $\mu_{\mathrm{map}}(s,\mathbb{N},\mathcal{M}_{\mathrm{fin}})$ does, that is, when $s$ is a map $s:\mathbb{N}\to\mathcal{M}_{\mathrm{fin}}$, a sequence of finite measures on $(S,\mathcal{B}(S))$; and $\varphi(S,F,\mu)$ holds exactly when $\mu$ is a finite measure on $(S,\mathcal{B}(S))$.

Bounded continuous functions. By Kit for def:continuous-map-metric-spaces (iv), with its $n$ equal to $5$ and its $i$, $j$, $k$, $l$, $p$ equal to $0,\dots,4$, there is a predicative formula in $x_{0},\dots,x_{4}$ expressing "$(x_{0},x_{1})$ and $(x_{2},x_{3})$ are metric spaces and $x_{4}$ is a continuous map $x_{4}:x_{0}\to x_{2}$". By Renaming and Substituting Variables in Predicative Formulas (iii), putting $S$, $d$, the parameters $\mathbb{R}$ and $d_{\mathbb{R}}$ (whose values are sets, by The Real Numbers (i) and, for $d_{\mathbb{R}}$, as an element of the class $\mathbb{R}^{\mathbb{R}\times\mathbb{R}}$, Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (ii), The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i), Elements Are Sets, and the Empty Set and the Pair of Two Sets Exist and Are Unique (i)), and $f$ for $x_{0},\dots,x_{4}$, it gives a predicative formula $c(S,d,f)$ that holds if and only if $(S,d)$ is a metric space and $f:S\to\mathbb{R}$ is a continuous map, $(\mathbb{R},d_{\mathbb{R}})$ being a metric space (The Absolute Value Metric on the Real Numbers (i)). By Predicative Formulas for Differences, Quotients, Absolute Values, Distances and the Strict Order of the Real Numbers, at Any Variable Positions (iii), with its $n$ equal to $2$, $i=0$ and $k=1$, renamed, there is a predicative formula $\alpha(y,t)$ that holds if and only if $y\in\mathbb{R}$ and $t=|y|$. Let

$$\chi(S,d,f)=c(S,d,f)\wedge\exists M\,\Bigl(M\in\mathbb{R}\wedge0\le M\wedge\forall x\,\forall y\,\forall t\,\bigl((x\in S\wedge(x,y)\in f\wedge\alpha(y,t))\Rightarrow t\le M\bigr)\Bigr).$$

Let $(S,d)$ be a metric space and $f$ a set. The first conjunct holds exactly when $f:S\to\mathbb{R}$ is a continuous map. In that case, for $x\in S$ the only $y$ with $(x,y)\in f$ is $f(x)$, and the only $t$ with $\alpha(f(x),t)$ is $|f(x)|$; so the second conjunct says that there is a real number $M\ge0$ with $|f(x)|\le M$ for every $x\in S$. By Bounded Continuous Functions on a Metric Space (i), $\chi(S,d,f)$ holds if and only if $f\in C_{b}(S)$.

Integrals through the image measure. The integral $\int_{S}f\,d\mu$ is taken on the measurable space $(S,\mathcal{B}(S))$, which varies with $S$ and $d$; it is moved to the fixed space $(\mathbb{R},\mathcal{B}(\mathbb{R}))$ as follows. Applying The Simple, Nonnegative, Integrable and Signed Integrals Are Predicative in the Measure and the Function, at Any Variable Positions (iii) with $X=\mathbb{R}$ and $\mathcal{F}=\mathcal{B}(\mathbb{R})$, with its $N$ equal to $3$ and its $i$, $j$, $k$ equal to $0$, $1$, $2$, putting the parameter $\iota$ for its variable $f$ (Renaming and Substituting Variables in Predicative Formulas (iii); the value $\iota$ is a set, as an element of the class $\mathbb{R}^{\mathbb{R}}$, The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i), Elements Are Sets, and the Empty Set and the Pair of Two Sets Exist and Are Unique (i)), and renaming $x_{0}$ and $x_{2}$ to $m$ and $r$ (Renaming and Substituting Variables in Predicative Formulas (i)), we obtain a predicative formula $\psi(m,r)$ that holds if and only if $m$ is a map $m:\mathcal{B}(\mathbb{R})\to[0,\infty]$, $\iota\in\mathcal{L}^{1}(m)$ and $r=\int\iota\,dm$. With $\mu_{\mathrm{map}}$ as above, let

$$\begin{aligned} \theta(\mu,f,\nu)={}&\mu_{\mathrm{map}}\bigl(\nu,\mathcal{B}(\mathbb{R}),[0,\infty]\bigr)\\ &\wedge\forall B\,\forall w\,\forall v'\,\Bigl(\bigl(B\in\mathcal{B}(\mathbb{R})\wedge\forall x\,\bigl(x\in w\Leftrightarrow\exists y\,(y\in B\wedge(x,y)\in f)\bigr)\wedge(B,v')\in\nu\bigr)\Rightarrow(w,v')\in\mu\Bigr),\\ J(\mu,f,r)={}&\exists\nu\,\bigl(\theta(\mu,f,\nu)\wedge\psi(\nu,r)\bigr). \end{aligned}$$

Both are predicative; in $\theta$ the parameters $\mathcal{B}(\mathbb{R})$ and $Z$, written there by their values $\mathcal{B}(\mathbb{R})$ and $[0,\infty]$, are put for the variables $A$ and $B$ of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (vii), the value $[0,\infty]$ being a set (The Extended Real Line, Its Order, and [0,∞] (ii)). Claim: let $(S,d)$ be a metric space, $\mu'$ a finite measure on $(S,\mathcal{B}(S))$ and $f\in C_{b}(S)$; then for every set $r$, $J(\mu',f,r)$ holds if and only if $r=\int_{S}f\,d\mu'$. Indeed, $f$ is $\mathcal{B}(S)/\mathcal{B}(\mathbb{R})$-measurable (Bounded Continuous Functions on a Metric Space: Measurability, Integrals, Operations, Lipschitz Functions and Approximation of Closed Sets (i)), so $f\in\mathrm{Meas}(S,\mathcal{B}(S);\mathbb{R},\mathcal{B}(\mathbb{R}))$ (Measurable Map, and the Set of Measurable Maps (ii)), and $(S,\mathcal{B}(S),\mu')$ is a measure space (Measure, Measure Space, and Probability Measure (ii)). Its image measure $\mu'\circ f^{-1}$ is a finite measure on $(\mathbb{R},\mathcal{B}(\mathbb{R}))$ (Image Measures and Measures with a Density: Measures, Integrals and Change of Variables (i)). For a set $\nu$, the first conjunct of $\theta(\mu',f,\nu)$ says that $\nu$ is a map $\nu:\mathcal{B}(\mathbb{R})\to[0,\infty]$. Let $B\in\mathcal{B}(\mathbb{R})$. A set $x$ satisfies $\exists y\,(y\in B\wedge(x,y)\in f)$ exactly when $x\in S$ and $f(x)\in B$, that is, when $x$ lies in the preimage $f^{-1}(B)$ (Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (ix)); this preimage belongs to $\mathcal{B}(S)$ by measurability (Measurable Map, and the Set of Measurable Maps (i)), so it is a set, and by extensionality it is the only set $w$ satisfying the middle conjunct of the antecedent. Then $(B,v')\in\nu$ means $v'=\nu(B)$, and $(f^{-1}(B),v')\in\mu'$ means $v'=\mu'(f^{-1}(B))$. So $\theta(\mu',f,\nu)$ holds if and only if $\nu$ is a map $\mathcal{B}(\mathbb{R})\to[0,\infty]$ with $\nu(B)=\mu'(f^{-1}(B))$ for every $B\in\mathcal{B}(\mathbb{R})$, that is, by Image Measure (i) and Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (iii), if and only if $\nu=\mu'\circ f^{-1}$. Hence $J(\mu',f,r)$ holds if and only if $\iota\in\mathcal{L}^{1}(\mu'\circ f^{-1})$ and $r=\int\iota\,d(\mu'\circ f^{-1})$. Now $\iota$ is $\mathcal{B}(\mathbb{R})/\mathcal{B}(\mathbb{R})$-measurable, as $\iota^{-1}(B)=B$ for every $B\in\mathcal{B}(\mathbb{R})$ (Measurable Map, and the Set of Measurable Maps (i)), and $\iota\circ f=f$, which lies in $\mathcal{L}^{1}(\mu')$ by Bounded Continuous Functions on a Metric Space: Measurability, Integrals, Operations, Lipschitz Functions and Approximation of Closed Sets (ii). By Image Measures and Measures with a Density: Measures, Integrals and Change of Variables (iii), with $f$ as its $T$ and $\iota$ as its $g$, therefore $\iota\in\mathcal{L}^{1}(\mu'\circ f^{-1})$ and

$$\int_{\mathbb{R}}\iota\,d(\mu'\circ f^{-1})=\int_{S}\iota\circ f\,d\mu'=\int_{S}f\,d\mu'.$$

This proves the claim. In particular $\int_{S}f\,d\mu'$ is a real number (Integrable Functions and Their Lebesgue Integral (iii)).

The formula for weak convergence. Let $\kappa(u,r)$ be the formula of Predicative Formulas for Convergence and Limits, and Maps Defined by Limits (i) for the metric space $(\mathbb{R},d_{\mathbb{R}})$, that is, with $X=\mathbb{R}$ and $d=d_{\mathbb{R}}$, its variables $s$ and $z$ being $u$ and $r$ and its auxiliary variables chosen as further set variables; it is predicative, and by Predicative Formulas for Convergence and Limits, and Maps Defined by Limits (iv) it holds if and only if $u$ is a sequence in $\mathbb{R}$ that converges to $r\in\mathbb{R}$. Let

$$\begin{aligned} \omega(S,d,s,\mu)={}&\rho(S,d)\wedge\exists F\,\Bigl(\beta(S,d,F)\wedge\eta(S,F,s)\wedge\varphi(S,F,\mu)\wedge\forall f\,\Bigl(\chi(S,d,f)\Rightarrow\exists u\,\exists r\,\bigl(\kappa(u,r)\wedge J(\mu,f,r)\\ &\qquad\wedge\forall m\,\forall v\,\forall t\,\bigl((m\in\mathbb{N}\wedge(m,v)\in s\wedge(m,t)\in u)\Rightarrow J(v,f,t)\bigr)\bigr)\Bigr)\Bigr). \end{aligned}$$

It is predicative, with free variables among $S$, $d$, $s$, $\mu$ and the parameters. Let sets $S$, $d$, $s$ and $\mu$ be assigned to $x_{0},\dots,x_{3}$. If $(S,d)$ is not a metric space, then $\rho$ fails, and $\omega$ fails together with the condition of (i). Let $(S,d)$ be a metric space. Then the only set $F$ satisfying $\beta(S,d,F)$ is $\mathcal{B}(S)$, so $\omega$ holds exactly when the bracket after $\exists F$ holds with $F=\mathcal{B}(S)$. If $s$ is not a sequence of finite measures on $(S,\mathcal{B}(S))$, or $\mu$ is not a finite measure on it, then $\eta$ or $\varphi$ fails, and again both $\omega$ and the condition fail. Let now $s=(\mu_{n})$ be a sequence of finite measures and $\mu$ a finite measure on $(S,\mathcal{B}(S))$. The sets $f$ satisfying $\chi(S,d,f)$ are the elements of $C_{b}(S)$; fix one. For sets $u$ and $r$, $\kappa(u,r)$ says that $u$ is a sequence in $\mathbb{R}$ converging to $r\in\mathbb{R}$, and, by the claim, $J(\mu,f,r)$ says that $r=\int_{S}f\,d\mu$. For $m\in\mathbb{N}$, the only $v$ with $(m,v)\in s$ is $\mu_{m}$ and the only $t$ with $(m,t)\in u$ is $u_{m}$, so by the claim the last conjunct says that $u_{m}=\int_{S}f\,d\mu_{m}$ for every $m\in\mathbb{N}$. Hence the part after $\chi(S,d,f)\Rightarrow$ holds if and only if some sequence $u$ in $\mathbb{R}$ with

$$u_{m}=\int_{S}f\,d\mu_{m}\qquad(m\in\mathbb{N})$$

converges to $\int_{S}f\,d\mu$. As each $\int_{S}f\,d\mu_{m}$ is a real number, Maps and Relations Given by Formulas (i) gives such a sequence, the sequence of integrals $(\int_{S}f\,d\mu_{m})_{m\in\mathbb{N}}$, and by Sequences: Enlarging the Codomain, Extensionality and the Range (ii) it is the only one. So that part holds if and only if $\int_{S}f\,d\mu_{n}\to\int_{S}f\,d\mu$, and $\omega$ holds if and only if this is so for every $f\in C_{b}(S)$, that is, by Weak Convergence of Finite Borel Measures on a Metric Space (i), if and only if $\mu_{n}\Rightarrow\mu$. In every case $\omega$ holds if and only if $(S,d)$ is a metric space, $s$ is a sequence of finite measures on $(S,\mathcal{B}(S))$, $\mu$ is a finite measure on $(S,\mathcal{B}(S))$ and $s$ converges weakly to $\mu$. So $\omega$ is a predicative formula in $x_{0},\dots,x_{3}$, in the sense of Renaming and Substituting Variables in Predicative Formulas, expressing this condition.

Weak convergence. By Renaming and Substituting Variables in Predicative Formulas (i), with its number of variables equal to $4$ and $\sigma(0)=i$, $\sigma(1)=j$, $\sigma(2)=k$ and $\sigma(3)=l$, the formula $\omega(x_{i},x_{j},x_{k},x_{l})$ is a predicative formula in $x_{0},\dots,x_{q-1}$ that holds, under every assignment of sets to $x_{0},\dots,x_{q-1}$, exactly when $(x_{i},x_{j})$ is a metric space, $x_{k}$ is a sequence of finite measures on $(x_{i},\mathcal{B}(x_{i}))$, $x_{l}$ is a finite measure on $(x_{i},\mathcal{B}(x_{i}))$ and $x_{k}$ converges weakly to $x_{l}$. This proves (i).

The set of measures to which a sequence converges weakly. Let $(S,d)$ be a metric space, $(\mu_{n})$ a sequence of finite measures on $(S,\mathcal{B}(S))$ and $\mathcal{M}_{\mathrm{fin}}$ the set of finite measures on $(S,\mathcal{B}(S))$, as above; $S$, $d$ and $(\mu_{n})$ are sets ($d\in\mathbb{R}^{S\times S}$ and $(\mu_{n})\in\mathcal{M}_{\mathrm{fin}}^{\mathbb{N}}$, Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (ii), The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i), Elements Are Sets, and the Empty Set and the Pair of Two Sets Exist and Are Unique (i)). Apply The Class Comprehension Theorem for Predicative Formulas (i) to $\omega$, with its abbreviations eliminated, with $x_{3}$ as its single variable and with $x_{0}$, $x_{1}$, $x_{2}$, assigned $S$, $d$, $(\mu_{n})$, and the parameters of the statement as its parameters (the one-entry tuple $\langle\mu\rangle$ being $\mu$, The Ordered Pair of Two Sets and Nested Tuples (ii)). By (i) it gives a class $C$ such that $\mu\in C$ if and only if $\mu$ is a finite measure on $(S,\mathcal{B}(S))$ and $\mu_{n}\Rightarrow\mu$, for every set $\mu$ and so for every class $\mu$ (the elements of $C$ and of $\mathcal{M}_{\mathrm{fin}}$ being sets). Finally $C\subseteq\mathcal{M}_{\mathrm{fin}}$, so $C$ is a set (Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper (i)). This proves (ii).

The set of sequences converging weakly to a measure. Let $(S,d)$ be a metric space and $\mu$ a finite measure on $(S,\mathcal{B}(S))$; as above, $S$, $d$ and $\mu\in\mathcal{M}_{\mathrm{fin}}$ are sets. Apply The Class Comprehension Theorem for Predicative Formulas (i) to $\omega$ with $x_{2}$ as its single variable and with $x_{0}$, $x_{1}$, $x_{3}$, assigned $S$, $d$, $\mu$, and the parameters of the statement as its parameters. By (i) it gives a class $C$ such that $a\in C$ if and only if $a$ is a sequence of finite measures on $(S,\mathcal{B}(S))$ converging weakly to $\mu$, for every set $a$ and so for every class $a$ (the elements of $C$ being sets, and such a sequence being a map $\mathbb{N}\to\mathcal{M}_{\mathrm{fin}}$, an element of the set $\mathcal{M}_{\mathrm{fin}}^{\mathbb{N}}$, Elements Are Sets, and the Empty Set and the Pair of Two Sets Exist and Are Unique (i), The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i), The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (ii)). So $C\subseteq\mathcal{M}_{\mathrm{fin}}^{\mathbb{N}}$, and $C$ is a set (Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper (i)). This proves (iii).