Kit for def:lp-convergence

In the setting of Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity and of The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness, let $q\ge1$ be a metatheoretic number, let $x_{0},\dots,x_{q-1}$ be distinct set variables, and let $i_{0},\dots,i_{6}<q$, not necessarily distinct. Let $\mathbb{N}_{0}$, $\mathbb{N}$, $\le_{0}$, $+_{0}$, $\mathbb{R}$, $\le$, $<$, $+$, $\cdot$, $d_{\mathbb{R}}$, $\iota$, $\exp$, $\log$, $\mathcal{B}(\mathbb{R})$, $[0,\infty]$, $+_{\infty}$, $\cdot_{\infty}$, $[-\infty,\infty]$, $\le_{\infty}$, $\mathcal{B}([0,\infty])$, $\mathcal{S}^{+}_{\mathbb{R}}$, $\mathcal{M}^{+}_{\mathbb{R}}$, $\mathrm{Meas}_{\mathbb{R}}$ and $\mathbb{R}^{\mathbb{R}}$ be distinct class variables with values the sets $\mathbb{N}_{0}$ and $\mathbb{N}$ of The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (ii), the order and the addition of $\mathbb{N}_{0}$, the set $\mathbb{R}$ of real numbers, its order, its strict order, its addition and its multiplication, the distance on $\mathbb{R}$, the identity $\mathrm{id}_{\mathbb{R}}$ on $\mathbb{R}$, the exponential function, the natural logarithm, the Borel $\sigma$-algebra of Borel Sigma-Algebra of a Metric Space (ii), the set $[0,\infty]$ of The Extended Real Line, Its Order, and [0,∞] (ii), its sum and its product, the set $[-\infty,\infty]$ and its order, the Borel $\sigma$-algebra of The Borel σ-Algebra of [0,∞] (ii), the set $\mathcal{S}^{+}(\mathbb{R},\mathcal{B}(\mathbb{R}))$ of nonnegative simple functions, the set $\mathcal{M}^{+}(\mathbb{R},\mathcal{B}(\mathbb{R}))$ of measurable maps into $[0,\infty]$, the set $\mathrm{Meas}(\mathbb{R},\mathcal{B}(\mathbb{R});\mathbb{R},\mathcal{B}(\mathbb{R}))$ of measurable maps, and the class $\mathbb{R}^{\mathbb{R}}$ of functions from $\mathbb{R}$ to $\mathbb{R}$; and let $\infty$, $0$ and $1$ be distinct set variables, other than $x_{0},\dots,x_{q-1}$, with values the element $\infty$ of The Extended Real Line, Its Order, and [0,∞] (i) and the elements $0$ and $1$ of $\mathbb{R}$, which are also those of $[0,\infty]$ (Addition and Multiplication on [0,∞] (ii)). The parameters of the following results are variables above: of Kit for def:measure-measure-space (vi), its $E$, $L$, $Z$, $P$, $\mathbb{N}$, $R$, $Q$, $\infty$, $0$ and $1$ being $[-\infty,\infty]$, $\le_{\infty}$, $[0,\infty]$, $+_{\infty}$, $\mathbb{N}$, $\le_{0}$, $+_{0}$, $\infty$, $0$ and $1$; of Kit for def:measurable-function (ii) and Kit for def:measurable-function (iii), its $R$ being $\le_{0}$ and its others the variables of the same names; of Predicative Formulas for Convergence and Limits, and Maps Defined by Limits (i) with $X=\mathbb{R}$ and $d=d_{\mathbb{R}}$, the variables of the same names; and of The Simple, Nonnegative, Integrable and Signed Integrals Are Predicative in the Measure and the Function, at Any Variable Positions (iii), its $X$, $\mathcal{F}$, $\mathcal{S}^{+}$, $\mathcal{M}^{+}$, $\mathrm{Meas}$ and $\mathbb{R}^{X}$ being $\mathbb{R}$, $\mathcal{B}(\mathbb{R})$, $\mathcal{S}^{+}_{\mathbb{R}}$, $\mathcal{M}^{+}_{\mathbb{R}}$, $\mathrm{Meas}_{\mathbb{R}}$ and $\mathbb{R}^{\mathbb{R}}$, its elements $0$ and $1$ of $\mathbb{R}$ being $0$ and $1$, and its sets of numbers with their operations and orders being $\mathbb{N}_{0}$, $\mathbb{N}$, $\mathbb{R}$, $[0,\infty]$ and $[-\infty,\infty]$ with $\le_{0}$, $+_{0}$, $\le$, $<$, $+$, $\cdot$, $+_{\infty}$, $\cdot_{\infty}$ and $\le_{\infty}$. A condition on $x_{0},\dots,x_{q-1}$ is predicative if it is expressed by a predicative formula with $x_{0},\dots,x_{q-1}$ as the set variables of Conditions Expressed by a Predicative Formula, and Guards (i), no displayed variables, and the other variables above as parameters. $\lVert\cdot\rVert$ is the Euclidean norm.

(i) Convergence in $L^{p}$. With $\Omega=x_{i_{0}}$, $\mathcal{F}=x_{i_{1}}$, $P=x_{i_{2}}$, $k=x_{i_{3}}$, $p=x_{i_{4}}$, $(Y_{n})=x_{i_{5}}$ and $Y=x_{i_{6}}$, the condition "$(\Omega,\mathcal{F},P)$ is a probability space, $k\in\mathbb{N}$, $p$ is a real number with $p\ge1$, $(Y_{n})$ is a sequence of random vectors in $\mathbb{R}^{k}$, $Y$ is a random vector in $\mathbb{R}^{k}$, $\lVert Y_{n}-Y\rVert$ lies in the set $\mathcal{L}^{p}(P)$ of $p$-integrable functions for every $n\in\mathbb{N}$, and $(Y_{n})$ converges to $Y$ in $L^{p}$" on $x_{0},\dots,x_{q-1}$ is predicative.