Kit for def:independence-events-rvs

In the setting of Measurable Functions and the Lebesgue Integral: Standing Notation and Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity, let $N\ge1$ be a metatheoretic number, let $x_{0},\dots,x_{N-1}$ be distinct set variables, and let $i,j,k,l,m,p,q,r,s<N$, not necessarily distinct. Let $E$, $L$, $Z$, $\oplus$, $\mathbb{N}$, $R$ and $Q$ be distinct class variables with the values of the class variables $E$, $L$, $Z$, $P$, $N$, $R$ and $Q$ of Sums of Sequences in [0,∞] as Typed Terms and as a Map (i) (its $P$ being written $\oplus$ and its $N$ being written $\mathbb{N}$ here), and let $\infty$, $0$ and $1$ be distinct set variables, other than $x_{0},\dots,x_{N-1}$, whose values are the element $\infty$ of The Extended Real Line, Its Order, and [0,∞] (i) and the elements $0$ and $1$ of $[0,\infty]$ (Addition and Multiplication on [0,∞] (ii)). Let $\mathbb{R}$, $\le_{\mathbb{R}}$, $<_{\mathbb{R}}$, $+_{\mathbb{R}}$, $0_{\mathbb{R}}$, $\mathcal{B}(\mathbb{R})$, $\mathcal{B}([0,\infty])$ and $\cdot_{\mathbb{R}}$ be further distinct class variables with values, in this order, the set of real numbers, its order, its strict order, its addition, its zero, the Borel $\sigma$-algebra of Borel Sigma-Algebra of a Metric Space (ii), the Borel $\sigma$-algebra of The Borel σ-Algebra of [0,∞] (ii), and the multiplication of the real numbers. A condition on $x_{0},\dots,x_{N-1}$ is predicative if it is expressed by a predicative formula, with $x_{0},\dots,x_{N-1}$ as the variables of Conditions Expressed by a Predicative Formula, and Guards (i), no displayed variables, and these eighteen variables as parameters. Families indexed by a set are as in Indexed Families of Sets and Their Union, Intersection and Product (i).

(i) Independent events. With $\Omega=x_{i}$, $\mathcal{F}=x_{j}$, $P=x_{k}$, $J=x_{l}$ and $A=x_{m}$, the condition "$(\Omega,\mathcal{F})$ is a measurable space, $P$ is a measure on $(\Omega,\mathcal{F})$, $(\Omega,\mathcal{F},P)$ is a probability space, $A=(A_{t})_{t\in J}$ is a family indexed by $J$ in which each $A_{t}$ is an event of $(\Omega,\mathcal{F},P)$, and $(A_{t})_{t\in J}$ is independent" is predicative.

(ii) Independent random elements. With $\Omega=x_{i}$, $\mathcal{F}=x_{j}$, $P=x_{k}$, $J=x_{l}$, $S=x_{m}$, $d=x_{p}$ and $X=x_{q}$, the condition "$(\Omega,\mathcal{F})$ is a measurable space, $P$ is a measure on $(\Omega,\mathcal{F})$, $(\Omega,\mathcal{F},P)$ is a probability space, $S=(S_{t})_{t\in J}$, $d=(d_{t})_{t\in J}$ and $X=(X_{t})_{t\in J}$ are families indexed by $J$, for every $t\in J$, $d_{t}$ is a map from the Cartesian product $S_{t}\times S_{t}$ to $\mathbb{R}$, $(S_{t},d_{t})$ is a metric space and $X_{t}$ is a random element of $S_{t}$, and $(X_{t})_{t\in J}$ is independent" is predicative.

(iii) Two independent random elements. With $\Omega=x_{i}$, $\mathcal{F}=x_{j}$, $P=x_{k}$, $S=x_{l}$, $d=x_{m}$, $X=x_{p}$, $T=x_{q}$, $e=x_{r}$ and $Y=x_{s}$, the condition "$(\Omega,\mathcal{F})$ is a measurable space, $P$ is a measure on $(\Omega,\mathcal{F})$, $(\Omega,\mathcal{F},P)$ is a probability space, $d$ is a map from $S\times S$ to $\mathbb{R}$, $(S,d)$ is a metric space, $X$ is a random element of $S$, $e$ is a map from $T\times T$ to $\mathbb{R}$, $(T,e)$ is a metric space, $Y$ is a random element of $T$, and $X$ and $Y$ are independent" is predicative.

(iv) A random element independent of a $\sigma$-algebra. With $\Omega=x_{i}$, $\mathcal{F}=x_{j}$, $P=x_{k}$, $S=x_{l}$, $d=x_{m}$, $X=x_{p}$ and $\mathcal{G}=x_{q}$, the condition "$(\Omega,\mathcal{F})$ is a measurable space, $P$ is a measure on $(\Omega,\mathcal{F})$, $(\Omega,\mathcal{F},P)$ is a probability space, $d$ is a map from $S\times S$ to $\mathbb{R}$, $(S,d)$ is a metric space, $X$ is a random element of $S$, $\mathcal{G}$ is a $\sigma$-algebra on $\Omega$ with $\mathcal{G}\subseteq\mathcal{F}$, and $X$ is independent of $\mathcal{G}$" is predicative.

(v) Iid sequences. With $\Omega=x_{i}$, $\mathcal{F}=x_{j}$, $P=x_{k}$, $S=x_{l}$, $d=x_{m}$ and $X=x_{p}$, the condition "$(\Omega,\mathcal{F})$ is a measurable space, $P$ is a measure on $(\Omega,\mathcal{F})$, $(\Omega,\mathcal{F},P)$ is a probability space, $d$ is a map from $S\times S$ to $\mathbb{R}$, $(S,d)$ is a metric space, $X=(X_{n})_{n\in\mathbb{N}}$ is a family indexed by $\mathbb{N}$ in which each $X_{n}$ is a random element of $S$, and $(X_{n})_{n\in\mathbb{N}}$ is independent and identically distributed" is predicative.