Proof of Kit for def:lp-convergence

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_{6}$ are distinct also when $q<7$. Every letter used below as a variable denotes a 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 σ-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), 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 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 Sequences, Limits, Cauchy Sequences, Series and Iterated Operations Agree (vi), The Earlier and the New Versions of the Definitions of Euclidean Space, Real Matrices and Normed Spaces Agree (i)).

Formulas from other results. Write $\mathrm{mp}(F,A,B)$ 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), which holds exactly when $F$ is a map $F:A\to B$, and $\Phi$ for 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); formulas $(a,b)\in c$ and $((a,b),c)\in e$ are predicative and mean what they say (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), Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iv)). By Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness (i), with $\mathbb{N}$ and $\le_{0}$ as its $Y$ and $R$, there is a predicative formula $\mathrm{seg}(z,k)$ that holds, for a set $z$ and $k\in\mathbb{N}_{0}$, exactly when $z=[k]$. By Iterated Operations Are Given by a Predicative Formula (i), with $\mathbb{R}$, $+$, $\mathbb{N}$, $\le_{0}$ and $+_{0}$ as its $X$, $F$, $Y$, $R$ and $P$, there is a predicative formula $\mathrm{it}(s,k,a)$ that holds, for $k\in\mathbb{N}$, a map $a:[k]\to\mathbb{R}$ and a set $s$, exactly when $s=\sum_{j=1}^{k}a_{j}$, the finite sum of Iterated Operations: Finite Sums and Finite Products (iii).

The Euclidean norm of a difference. Let

$$\begin{aligned} \varpi(z,k,x,y,r)={}&\mathrm{mp}(x,z,\mathbb{R})\wedge\mathrm{mp}(y,z,\mathbb{R})\wedge\exists a\,\exists s\,\Bigl(\mathrm{mp}(a,z,\mathbb{R})\wedge\forall j\,\forall u\,\forall v\,\forall t\,\bigl(((j,u)\in x\wedge(j,v)\in y\wedge(j,t)\in a)\\ &\Rightarrow\exists c\,(((c,v),u)\in{+}\wedge((c,c),t)\in{\cdot})\bigr)\wedge\mathrm{it}(s,k,a)\wedge r\in\mathbb{R}\wedge(0,r)\in{\le}\wedge((r,r),s)\in{\cdot}\Bigr). \end{aligned}$$

It is predicative. Claim A: let $k\in\mathbb{N}$, $z=[k]$, and let $x$, $y$ and $r$ be sets; then $\varpi(z,k,x,y,r)$ holds if and only if $x,y\in\mathbb{R}^{k}$ and $r=\lVert x-y\rVert$. By Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (ii), the first two conjuncts hold exactly when $x,y\in\mathbb{R}^{k}$; let them hold, and let $w=x-y\in\mathbb{R}^{k}$, so that $w_{j}=x_{j}-y_{j}$ for $j\in[k]$ (Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (iv)). Let $a:[k]\to\mathbb{R}$ be a map. The sets $j$, $u$, $v$ and $t$ satisfying the antecedent are the $j\in[k]$ with $u=x_{j}$, $v=y_{j}$ and $t=a_{j}$; and as $+$ is a binary operation on $\mathbb{R}$, a set $c$ with $((c,y_{j}),x_{j})\in{+}$ is a real number with $c+y_{j}=x_{j}$, that is, $c=w_{j}$. So the second conjunct of the bracket says that $a_{j}=w_{j}w_{j}$ for every $j\in[k]$, which holds exactly when $a$ is the pointwise product $ww\in\mathbb{R}^{[k]}$ of Pointwise Operations on Real-Valued Maps (i) (Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (iii)). For $a=ww$, $\mathrm{it}(s,k,a)$ holds exactly when

$$s=\sum_{j=1}^{k}w_{j}w_{j}=w\cdot w,$$

the dot product of The Dot Product on $\mathbb{R}^n$ (i), a real number with $w\cdot w\ge0$ (The Dot Product on $\mathbb{R}^n$ Is Symmetric, Bilinear and Positive Definite (iv)). The last three conjuncts then say that $r$ is a real number with $r\ge0$ and $r\cdot r=w\cdot w$, where $r\cdot r=r^{2}$; by The k-th Root and the Square Root of a Nonnegative Real Number (i) and The k-th Root and the Square Root of a Nonnegative Real Number (ii) this holds exactly when $r=\sqrt{w\cdot w}$, which is $\lVert w\rVert=\lVert x-y\rVert$ by The Euclidean Norm on $\mathbb{R}^n$ (i). This proves Claim A.

The formula for norm differences. Let

$$\begin{aligned} \delta(\Omega,k,Z,Y,h)={}&k\in\mathbb{N}\wedge\exists z\,\exists E\,\Bigl(\mathrm{seg}(z,k)\wedge\forall e\,\bigl(e\in E\Leftrightarrow\mathrm{mp}(e,z,\mathbb{R})\bigr)\wedge\mathrm{mp}(Z,\Omega,E)\wedge\mathrm{mp}(Y,\Omega,E)\wedge\mathrm{mp}(h,\Omega,\mathbb{R})\\ &\wedge\forall\omega\,\forall x\,\forall y\,\forall r\,\bigl(((\omega,x)\in Z\wedge(\omega,y)\in Y\wedge(\omega,r)\in h)\Rightarrow\varpi(z,k,x,y,r)\bigr)\Bigr). \end{aligned}$$

It is predicative, with free variables among $\Omega$, $k$, $Z$, $Y$, $h$ and the parameters. Claim D: for sets $\Omega$, $k$, $Z$, $Y$ and $h$, $\delta(\Omega,k,Z,Y,h)$ holds if and only if $k\in\mathbb{N}$, $Z$ and $Y$ are maps from $\Omega$ to $\mathbb{R}^{k}$, and $h$ is a map $h:\Omega\to\mathbb{R}$ with $h(\omega)=\lVert Z(\omega)-Y(\omega)\rVert$ for every $\omega\in\Omega$. If $k\notin\mathbb{N}$, both sides fail. Let $k\in\mathbb{N}$, so $k\in\mathbb{N}_{0}$ and the only set $z$ with $\mathrm{seg}(z,k)$ is $[k]$. For $z=[k]$, the sets $e$ with $\mathrm{mp}(e,z,\mathbb{R})$ are the elements of the set $\mathbb{R}^{k}$ (Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (i), Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (ii)), so by the axiom of extensionality the only set $E$ satisfying the second conjunct is $\mathbb{R}^{k}$. So $\delta$ holds exactly when $Z,Y:\Omega\to\mathbb{R}^{k}$ and $h:\Omega\to\mathbb{R}$ are maps and the last conjunct holds with $z=[k]$. For such maps, the sets $\omega$, $x$, $y$ and $r$ satisfying its antecedent are the $\omega\in\Omega$ with $x=Z(\omega)$, $y=Y(\omega)$ and $r=h(\omega)$ (Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (ii)), and by Claim A, as $Z(\omega),Y(\omega)\in\mathbb{R}^{k}$, the formula $\varpi([k],k,Z(\omega),Y(\omega),h(\omega))$ holds exactly when $h(\omega)=\lVert Z(\omega)-Y(\omega)\rVert$. This proves Claim D; so this condition on $\Omega$, $k$, $Z$, $Y$ and $h$ is expressed by the predicative formula $\delta$. In particular, for a set $\Omega$, $k\in\mathbb{N}$ and maps $Z,Y:\Omega\to\mathbb{R}^{k}$, exactly one set $h$ satisfies $\delta(\Omega,k,Z,Y,h)$: the map

$$\lVert Z-Y\rVert:\Omega\to\mathbb{R},\qquad\omega\mapsto\lVert Z(\omega)-Y(\omega)\rVert,$$

the function of Probability Spaces: Notation (iv), which exists by Maps and Relations Given by Formulas (i), each $\lVert Z(\omega)-Y(\omega)\rVert$ being a real number, and is unique by Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (iii). Its values are $\ge0$, being square roots (The Euclidean Norm on $\mathbb{R}^n$ (i), The k-th Root and the Square Root of a Nonnegative Real Number (i)).

Probability spaces, random vectors and measurable real functions. By Kit for def:measure-measure-space (vi), with its $n$ equal to $3$ and its $i$, $j$, $k$ equal to $0$, $1$, $2$, renamed, and with its parameters the variables the statement lists for it, there is a predicative formula $\pi(\Omega,\mathcal{F},P)$ that holds if and only if $(\Omega,\mathcal{F})$ is a measurable space and $P$ is a measure on it with $P(\Omega)=1$; by Measure, Measure Space, and Probability Measure (ii) and Probability Spaces, Events and Random Elements (i), this is the case exactly when $(\Omega,\mathcal{F},P)$ is a probability space. By Kit for def:measurable-function (iii), with its $N$ equal to $4$ and its $i$, $j$, $k$, $l$ equal to $0,\dots,3$, renamed, and with its $R$ the variable $\le_{0}$ and its other parameters the variables of the same names, as the statement lists them, there is a predicative formula $\rho_{E}(\Omega,\mathcal{F},k,e)$ that holds if and only if $(\Omega,\mathcal{F})$ is a measurable space, $k\in\mathbb{N}$ and $e:\Omega\to\mathbb{R}^{k}$ is a map that is measurable as a map into $\mathbb{R}^{k}$; when $(\Omega,\mathcal{F},P)$ is a probability space and $k\in\mathbb{N}$, this says, by Probability Spaces, Events and Random Elements (v), that $e$ is a random vector in $\mathbb{R}^{k}$, that is, $e\in M_{k}$ for the set $M_{k}=\mathrm{Meas}(\Omega,\mathcal{F};\mathbb{R}^{k},\mathcal{B}(\mathbb{R}^{k}))$ (Measurable Map, and the Set of Measurable Maps (iv), Measurable Map, and the Set of Measurable Maps (ii)). By Kit for def:measurable-function (ii), with its $N$ equal to $3$ and its $i$, $j$, $k$ equal to $0$, $1$, $2$, renamed, and with its parameters chosen in the same way, there is a predicative formula $\rho_{\mathbb{R}}(\Omega,\mathcal{F},h)$ that holds if and only if $(\Omega,\mathcal{F})$ is a measurable space and $h:\Omega\to\mathbb{R}$ is a map that is measurable as a map into $\mathbb{R}$, that is, $h\in\mathrm{Meas}(\Omega,\mathcal{F};\mathbb{R},\mathcal{B}(\mathbb{R}))$ (Measurable Map, and the Set of Measurable Maps (iii), Measurable Map, and the Set of Measurable Maps (ii)). Let

$$\eta(s)=\Phi(s)\wedge\forall m\,\bigl(m\in\mathbb{N}\Leftrightarrow\exists e\,((m,e)\in s)\bigr)\wedge\forall m\,\forall e\,\bigl((m,e)\in s\Rightarrow\rho_{E}(\Omega,\mathcal{F},k,e)\bigr).$$

When $(\Omega,\mathcal{F},P)$ is a probability space and $k\in\mathbb{N}$, a set $e$ satisfies $\rho_{E}(\Omega,\mathcal{F},k,e)$ if and only if $e\in M_{k}$, so $\eta(s)$ holds exactly when $\mathrm{mp}(s,\mathbb{N},M_{k})$ does, that is, when $s$ is a map $s:\mathbb{N}\to M_{k}$, a sequence of random vectors in $\mathbb{R}^{k}$ (Sequences (i)).

Powers with a real exponent. Let

$$\mathrm{pw}(t,p,z)=\Bigl((0,t)\in{<}\wedge\exists l\,\exists m\,\bigl((t,l)\in\log\wedge((p,l),m)\in{\cdot}\wedge(m,z)\in\exp\bigr)\Bigr)\vee\bigl(t=0\wedge z=0\bigr).$$

Let $t$ and $p$ be real numbers with $t\ge0$ and $p>0$; then a set $z$ satisfies $\mathrm{pw}(t,p,z)$ if and only if $z=t^{p}$, the real power, with Real Powers (ii) for $t=0$. If $t>0$, the second disjunct fails; as $\log$ is a map $(0,\infty)\to\mathbb{R}$ on the ray $(0,\infty)$ and $\exp$ a map $\mathbb{R}\to\mathbb{R}$, the sets $l$ and $m$ in the first disjunct must be $\log t$ and $p\log t$, and it holds exactly when $z=\exp(p\log t)=t^{p}$ (Real Powers (i)). If $t=0$, the first disjunct fails, as $0<0$ is false, and the second holds exactly when $z=0=0^{p}$ (Real Powers (ii)). Let

$$\tau(\Omega,h,p,T)=\mathrm{mp}(T,\Omega,\mathbb{R})\wedge\forall\omega\,\forall t\,\forall z\,\bigl(((\omega,t)\in h\wedge(\omega,z)\in T)\Rightarrow\mathrm{pw}(t,p,z)\bigr).$$

For a set $\Omega$, a map $h:\Omega\to\mathbb{R}$ with values $\ge0$ and a real number $p>0$, it follows that a set $T$ satisfies $\tau(\Omega,h,p,T)$ if and only if $T$ is a map $T:\Omega\to\mathbb{R}$ with $T(\omega)=h(\omega)^{p}$ for every $\omega\in\Omega$; there is exactly one such map (Maps and Relations Given by Formulas (i), Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (iii)), and as $|h(\omega)|=h(\omega)$ (Absolute Value in an Ordered Field (i)), it is the map $|h|^{p}$, $\omega\mapsto|h(\omega)|^{p}$, of Power-Integrable Functions and the p-Seminorm (i) and Real Powers of the Absolute Value of a Measurable Function Are Measurable (i).

Integrals through the image measure. The set $\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 set (The σ-Algebra Generated by a Set of Subsets (i)) and a $\sigma$-algebra on $\mathbb{R}$ (Closure Properties of σ-Algebras, Intersections and Traces of σ-Algebras, and the Generated σ-Algebra (iii)), so $(\mathbb{R},\mathcal{B}(\mathbb{R}))$ is a measurable space. Integrals over $\Omega$ are reached through image measures on $\mathbb{R}$ because The Simple, Nonnegative, Integrable and Signed Integrals Are Predicative in the Measure and the Function, at Any Variable Positions has the measurable space, its $X$ and $\mathcal{F}$, as parameters, while $\Omega$ and $\mathcal{F}$ are variables here. With $X=\mathbb{R}$ and $\mathcal{F}=\mathcal{B}(\mathbb{R})$, each parameter of The Simple, Nonnegative, Integrable and Signed Integrals Are Predicative in the Measure and the Function, at Any Variable Positions (iii) is the variable that the statement lists for it. 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=\mathrm{id}_{\mathbb{R}}$ is a set, being a map $\mathbb{R}\to\mathbb{R}$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (iii), so an element of the class $\mathbb{R}^{\mathbb{R}}$ by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i), and elements are sets by Elements Are Sets, and the Empty Set and the Pair of Two Sets Exist and Are Unique (i)), and renaming, we obtain a predicative formula $\psi(\nu,r)$ that holds if and only if $\nu$ is a map $\nu:\mathcal{B}(\mathbb{R})\to[0,\infty]$, $\iota\in\mathcal{L}^{1}(\nu)$ and $r=\int\iota\,d\nu$. Let

$$\theta(P,T,\nu)=\mathrm{mp}\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 a\,\bigl(a\in w\Leftrightarrow\exists b\,(b\in B\wedge(a,b)\in T)\bigr)\wedge(B,v)\in\nu\bigr)\Rightarrow(w,v)\in P\Bigr).$$

It is predicative, the parameters $\mathcal{B}(\mathbb{R})$ and $[0,\infty]$ being 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). Claim C: let $(\Omega,\mathcal{F},P)$ be a probability space and $T\in\mathrm{Meas}(\Omega,\mathcal{F};\mathbb{R},\mathcal{B}(\mathbb{R}))$; then for every set $r$, some set $\nu$ satisfies $\theta(P,T,\nu)\wedge\psi(\nu,r)$ if and only if $T\in\mathcal{L}^{1}(P)$ and $r=\int_{\Omega}T\,dP$. Indeed, $(\Omega,\mathcal{F},P)$ is a measure space, and the image measure $P\circ T^{-1}$ is a map $\mathcal{B}(\mathbb{R})\to[0,\infty]$ with $(P\circ T^{-1})(B)=P(T^{-1}(B))$ for $B\in\mathcal{B}(\mathbb{R})$. For a set $\nu$, the first conjunct of $\theta(P,T,\nu)$ says that $\nu$ is a map $\nu:\mathcal{B}(\mathbb{R})\to[0,\infty]$. Let $B\in\mathcal{B}(\mathbb{R})$. A set $a$ satisfies $\exists b\,(b\in B\wedge(a,b)\in T)$ exactly when $a\in\Omega$ and $T(a)\in B$, that is, when $a\in T^{-1}(B)$ (Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (ix)); this preimage lies in $\mathcal{F}$ 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 $(T^{-1}(B),v)\in P$ means $v=P(T^{-1}(B))$. So $\theta(P,T,\nu)$ holds if and only if $\nu(B)=P(T^{-1}(B))$ for every $B\in\mathcal{B}(\mathbb{R})$, that is, if and only if $\nu=P\circ T^{-1}$ (Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (iii)). Hence some $\nu$ satisfies $\theta(P,T,\nu)\wedge\psi(\nu,r)$ if and only if $\iota\in\mathcal{L}^{1}(P\circ T^{-1})$ and $r=\int\iota\,d(P\circ T^{-1})$. Now $\iota=\mathrm{id}_{\mathbb{R}}$ is $\mathcal{B}(\mathbb{R})/\mathcal{B}(\mathbb{R})$-measurable (Measurable Maps: Generators, Composition, Continuous Maps, Restrictions, and Criteria for Real- and [0,∞]-Valued Maps (iii)), and $\iota\circ T=T$ (Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (iv)). By Image Measures and Measures with a Density: Measures, Integrals and Change of Variables (iii), with $(\Omega,\mathcal{F},P)$ as its $(X,\mathcal{F},\mu)$, $(\mathbb{R},\mathcal{B}(\mathbb{R}))$ as its $(Y,\mathcal{G})$, $T$ as its $T$, $\iota$ as its $g$, and as its $h$ the map $\Omega\to[0,\infty]$ with value $0$ everywhere, which lies in $\mathcal{M}^{+}(\Omega,\mathcal{F})$ by Measurable Maps: Generators, Composition, Continuous Maps, Restrictions, and Criteria for Real- and [0,∞]-Valued Maps (iii), $\iota\in\mathcal{L}^{1}(P\circ T^{-1})$ if and only if $T\in\mathcal{L}^{1}(P)$, and in that case

$$\int_{\mathbb{R}}\iota\,d(P\circ T^{-1})=\int_{\Omega}\iota\circ T\,dP=\int_{\Omega}T\,dP.$$

This proves Claim C.

The $p$-th moment of a norm difference. Let

$$\Lambda(e,t)=\exists h\,\exists T\,\exists\nu\,\bigl(\delta(\Omega,k,e,Y,h)\wedge\rho_{\mathbb{R}}(\Omega,\mathcal{F},h)\wedge\tau(\Omega,h,p,T)\wedge\theta(P,T,\nu)\wedge\psi(\nu,t)\bigr).$$

It is predicative, with free variables among $e$, $t$, $\Omega$, $\mathcal{F}$, $P$, $k$, $p$, $Y$ and the parameters. Claim B: let $(\Omega,\mathcal{F},P)$ be a probability space, $k\in\mathbb{N}$, $p$ a real number with $p\ge1$, and $e$ and $Y$ random vectors in $\mathbb{R}^{k}$; then for every set $t$, $\Lambda(e,t)$ holds if and only if $\lVert e-Y\rVert\in\mathcal{L}^{p}(P)$ and $t=\mathbb{E}\lVert e-Y\rVert^{p}$, which is then a real number. As $e,Y:\Omega\to\mathbb{R}^{k}$ are maps, the only set $h$ with $\delta(\Omega,k,e,Y,h)$ is $\lVert e-Y\rVert$, by Claim D, and $\rho_{\mathbb{R}}(\Omega,\mathcal{F},\lVert e-Y\rVert)$ holds exactly when $\lVert e-Y\rVert$ is measurable. If it is not, $\Lambda(e,t)$ fails, and $\lVert e-Y\rVert\notin\mathcal{L}^{p}(P)$, as the elements of $\mathcal{L}^{p}(P)$ are measurable (Power-Integrable Functions and the p-Seminorm (ii)). Let $\lVert e-Y\rVert$ be measurable. Its values are $\ge0$ and $p>0$, so the only set $T$ with $\tau(\Omega,\lVert e-Y\rVert,p,T)$ is $|\lVert e-Y\rVert|^{p}$, which is $\lVert e-Y\rVert^{p}$ (Lᵖ Spaces: Notation (ii)) and lies in $\mathrm{Meas}(\Omega,\mathcal{F};\mathbb{R},\mathcal{B}(\mathbb{R}))$ and in $\mathcal{M}^{+}(\Omega,\mathcal{F})$ (Real Powers of the Absolute Value of a Measurable Function Are Measurable (i)). By Claim C, $\Lambda(e,t)$ then holds if and only if $\lVert e-Y\rVert^{p}\in\mathcal{L}^{1}(P)$ and $t=\int_{\Omega}\lVert e-Y\rVert^{p}\,dP$, the integral of an element of $\mathcal{L}^{1}(P)$, a real number (Integrable Functions and Their Lebesgue Integral (iii)). By Elementary Properties of the p-Seminorm (ii), $\lVert e-Y\rVert\in\mathcal{L}^{p}(P)$ if and only if $\lVert e-Y\rVert^{p}\in\mathcal{L}^{1}(P)$, $\lVert e-Y\rVert$ being measurable, and in that case this integral equals the integral of $\lVert e-Y\rVert^{p}$ as an element of $\mathcal{M}^{+}(\Omega,\mathcal{F})$, which is $\mathbb{E}\lVert e-Y\rVert^{p}$ by Probability Spaces: Notation (v) and Expectation (i) (and, $\lVert e-Y\rVert^{p}$ being an integrable random variable, by Expectation (ii) as well). This proves Claim B.

The formula for convergence in $L^{p}$. Apply Predicative Formulas for Convergence and Limits, and Maps Defined by Limits (i) with $X=\mathbb{R}$ and $d=d_{\mathbb{R}}$, its parameters being the variables of the same names, as the statement lists them, with $u$ as its variable $s$ and its other variables chosen as further set variables, and put the parameter $0$ for its variable $z$ (Renaming and Substituting Variables in Predicative Formulas (iii)); let $\kappa(u)$ be the resulting formula. 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 $0$. Let

$$\begin{aligned} \alpha(\Omega,\mathcal{F},P,k,p,s,Y)={}&\pi(\Omega,\mathcal{F},P)\wedge k\in\mathbb{N}\wedge p\in\mathbb{R}\wedge(1,p)\in{\le}\wedge\eta(s)\wedge\rho_{E}(\Omega,\mathcal{F},k,Y)\wedge\forall m\,\forall e\,\bigl((m,e)\in s\Rightarrow\exists t\,\Lambda(e,t)\bigr)\\ &\wedge\exists u\,\Bigl(\kappa(u)\wedge\forall m\,\forall e\,\forall t\,\bigl(((m,e)\in s\wedge(m,t)\in u)\Rightarrow\Lambda(e,t)\bigr)\Bigr). \end{aligned}$$

It is predicative, with free variables among $\Omega$, $\mathcal{F}$, $P$, $k$, $p$, $s$, $Y$ and the parameters. Let sets $\Omega$, $\mathcal{F}$, $P$, $k$, $p$, $s$ and $Y$ be assigned to these variables. If $(\Omega,\mathcal{F},P)$ is not a probability space, or $k\notin\mathbb{N}$, or $p$ is not a real number with $1\le p$, then $\alpha$ fails together with the condition of (i). Let $(\Omega,\mathcal{F},P)$ be a probability space, $k\in\mathbb{N}$ and $p$ a real number with $p\ge1$. If $s$ is not a sequence of random vectors in $\mathbb{R}^{k}$, or $Y$ is not a random vector in $\mathbb{R}^{k}$, then $\eta(s)$ or $\rho_{E}(\Omega,\mathcal{F},k,Y)$ fails, and again both $\alpha$ and the condition fail. Let now $s=(Y_{n})$ be a sequence of random vectors in $\mathbb{R}^{k}$ and $Y$ a random vector in $\mathbb{R}^{k}$. The sets $m$ and $e$ with $(m,e)\in s$ are the $m\in\mathbb{N}$ with $e=Y_{m}$, so by Claim B the seventh conjunct of $\alpha$ says that $\lVert Y_{m}-Y\rVert\in\mathcal{L}^{p}(P)$ for every $m\in\mathbb{N}$; if this fails, $\alpha$ and the condition fail. Let it hold. For a set $u$, $\kappa(u)$ says that $u$ is a sequence in $\mathbb{R}$ converging to $0$, and then the only $t$ with $(m,t)\in u$, for $m\in\mathbb{N}$, is $u_{m}$; so by Claim B the bracket after $\exists u$ says that $u$ converges to $0$ and

$$u_{m}=\mathbb{E}\lVert Y_{m}-Y\rVert^{p}\qquad(m\in\mathbb{N}).$$

As each $\mathbb{E}\lVert Y_{m}-Y\rVert^{p}$ is a real number, Maps and Relations Given by Formulas (i) gives such a sequence, the sequence $(\mathbb{E}\lVert Y_{n}-Y\rVert^{p})_{n\in\mathbb{N}}$, and by Sequences: Enlarging the Codomain, Extensionality and the Range (ii) it is the only one. So the last conjunct holds if and only if

$$\mathbb{E}\lVert Y_{n}-Y\rVert^{p}\to0\qquad(n\to\infty),$$

convergence of real numbers as in Convergent Sequences of Real Numbers (i), that is, by Convergence in Lᵖ of Random Vectors (i), if and only if $(Y_{n})$ converges to $Y$ in $L^{p}$. In every case $\alpha$ holds if and only if the condition of (i) holds with $\Omega,\mathcal{F},P,k,p,(Y_{n}),Y$ the sets assigned. With $\Omega,\mathcal{F},P,k,p,s,Y$ renamed to $x_{0},\dots,x_{6}$, $\alpha$ is therefore a predicative formula in $x_{0},\dots,x_{6}$, in the sense of Renaming and Substituting Variables in Predicative Formulas, expressing this condition.

Convergence in $L^{p}$. By Renaming and Substituting Variables in Predicative Formulas (i), with its $\varphi$ equal to $\alpha$, its $k$ equal to $7$, its $n$ equal to $q$ and $\sigma(m)=i_{m}$ for $m<7$, the formula $\alpha(x_{i_{0}},\dots,x_{i_{6}})$ 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_{0}},x_{i_{1}},x_{i_{2}})$ is a probability space, $x_{i_{3}}\in\mathbb{N}$, $x_{i_{4}}$ is a real number with $x_{i_{4}}\ge1$, $x_{i_{5}}$ is a sequence of random vectors in $\mathbb{R}^{x_{i_{3}}}$, $x_{i_{6}}$ is a random vector in $\mathbb{R}^{x_{i_{3}}}$, $\lVert x_{i_{5}}(n)-x_{i_{6}}\rVert\in\mathcal{L}^{p}(x_{i_{2}})$ for every $n\in\mathbb{N}$ with $p=x_{i_{4}}$, and $x_{i_{5}}$ converges to $x_{i_{6}}$ in $L^{x_{i_{4}}}$. This proves (i).