Proof of Suprema, Infima, Limits Inferior and Limits Superior of Measurable [0,∞]-Valued Maps

For a map $u$ from $X$ to $[0,\infty]$ and $a\in\mathbb{R}$, write $\{u>a\}=\{x\in X:u(x)>a\}$ and $\{u\ge a\}=\{x\in X:u(x)\ge a\}$, and for $a\in\mathbb{R}$ let $Q_{a}=\{q\in\mathbb{Q}:q>a\}$. We use that $\le$ is a total order on $[-\infty,\infty]$ which on $\mathbb{R}$ is the order of $\mathbb{R}$ (Order and Suprema in the Extended Real Line (i)), and that for real numbers $b<b'$ there is $q\in\mathbb{Q}$ with $b<q<b'$ (The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness (x)). For $k\in\mathbb{N}$ and $x\in X$, both varying, $f_{k}(x)$ is the value at $(f_{k},x)$ of the evaluation map from $[0,\infty]^{X}\times X$ to $[0,\infty]$ (Projection, Evaluation and Currying Maps (ii)).

Countable index sets. $\mathbb{N}$ and $\mathbb{Q}$ are countable by Countable Sets: a Bijection from ℕ onto ℕ×ℕ, Finite Sets, Subsets, Surjective Images, Images, Products, and the Integers and Rationals (i) and Countable Sets: a Bijection from ℕ onto ℕ×ℕ, Finite Sets, Subsets, Surjective Images, Images, Products, and the Integers and Rationals (ix), so every subset $J$ of $\mathbb{N}$ and every $Q_{a}$ is countable by Countable Sets: a Bijection from ℕ onto ℕ×ℕ, Finite Sets, Subsets, Surjective Images, Images, Products, and the Integers and Rationals (iv). Hence, for $I$ such a set and every map $i\mapsto A_{i}$ from $I$ to $\mathcal{F}$, $\bigcup_{i\in I}A_{i}\in\mathcal{F}$ by Unions and Intersections over a Countable Index Set in a σ-Algebra (i), and $\bigcap_{i\in I}A_{i}\in\mathcal{F}$ if $I\neq\emptyset$, by Unions and Intersections over a Countable Index Set in a σ-Algebra (ii).

A rational between. Let $a\in\mathbb{R}$ and $t\in[0,\infty]$ with $a<t$. Put $b=t$ if $t\neq\infty$, a real number by The Extended Real Line, Its Order, and [0,∞] (ii), and $b=a+1$ if $t=\infty$; in both cases $b$ is real and $a<b\le t$, as real numbers are $<\infty$ by The Extended Real Line, Its Order, and [0,∞] (iii) and The Extended Real Line, Its Order, and [0,∞] (i). Taking $q\in\mathbb{Q}$ with $a<q<b$ gives $q\in Q_{a}$ with $q<t$.

Measurable superlevel sets. For every $k\in\mathbb{N}$ and $a\in\mathbb{R}$, $\{f_{k}>a\}\in\mathcal{F}$ by Measurable Maps: Generators, Composition, Continuous Maps, Restrictions, and Criteria for Real- and [0,∞]-Valued Maps (vi), and $\{f_{k}\ge a\}=f_{k}^{-1}(\{y\in[0,\infty]:y\ge a\})$ (Preimages under a Map: Membership, the Preimage Map, Sequences of Preimages, and the Set of Sets with Preimage in a Given Set (ii)), which belongs to $\mathcal{F}$ by Borel Subsets of [0,∞]: Rays, the Point ∞, and Traces on ℝ (i) and Measurable Map, and the Set of Measurable Maps (i).

Suprema. Let $J$ be a nonempty subset of $\mathbb{N}$ and, for $x\in X$, $s(x)=\sup_{k\in J}f_{k}(x)$, which exists by Order and Suprema in the Extended Real Line (iii) and lies in $[0,\infty]$ by Order and Suprema in the Extended Real Line (ix), the set $\{f_{k}(x):k\in J\}\subseteq[0,\infty]$ being nonempty. So $s$, $x\mapsto\sup_{k\in J}f_{k}(x)$, is a map $X\to[0,\infty]$, its values lying in $[0,\infty]$. Let $a\in\mathbb{R}$ and $x\in X$. If $f_{k}(x)>a$ for some $k\in J$, then $s(x)\ge f_{k}(x)>a$, as $s(x)$ is an upper bound of that set (Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order (iv)). If $s(x)>a$, then $a<f_{k}(x)$ for some $k\in J$, by Order and Suprema in the Extended Real Line (x). Hence $\{s>a\}=\bigcup_{k\in J}\{f_{k}>a\}$, the union of the map $k\mapsto\{f_{k}>a\}$ from $J$ to $\mathcal{F}$, its values lying in $\mathcal{F}$ by the paragraph on measurable superlevel sets (Preimages, Unions and Intersections over an Index Set, Suprema and Infima, and Superlevel Sets as Typed Terms (vi), Preimages, Unions and Intersections over an Index Set, Suprema and Infima, and Superlevel Sets as Typed Terms (v)), which belongs to $\mathcal{F}$ by the paragraph on countable index sets. So $s$ is measurable by Measurable Maps: Generators, Composition, Continuous Maps, Restrictions, and Criteria for Real- and [0,∞]-Valued Maps (vi). With $J=\mathbb{N}$, which contains $1$, this proves (i).

Infima. Let $J$ be a subset of $\mathbb{N}$ and, for $x\in X$, $\iota(x)=\inf_{k\in J}f_{k}(x)$, which exists by Order and Suprema in the Extended Real Line (iii) and lies in $[0,\infty]$ by Order and Suprema in the Extended Real Line (ix). So $\iota$, $x\mapsto\inf_{k\in J}f_{k}(x)$, is a map $X\to[0,\infty]$, its values lying in $[0,\infty]$. Let $a\in\mathbb{R}$ and $x\in X$. We show that $\iota(x)>a$ if and only if there is $q\in Q_{a}$ with $f_{k}(x)\ge q$ for every $k\in J$. If there is such a $q$, it is a lower bound of $\{f_{k}(x):k\in J\}$, so $q\le\iota(x)$ by Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order (iv), and $a<q\le\iota(x)$. Conversely let $\iota(x)>a$. By the paragraph on a rational between there is $q\in Q_{a}$ with $q<\iota(x)$, and for $k\in J$, $f_{k}(x)\ge\iota(x)>q$, as $\iota(x)$ is a lower bound of the set. For $q\in Q_{a}$ let $C_{q}=\{x\in X:f_{k}(x)\ge q\text{ for every }k\in J\}$. Then

$$\{\iota>a\}=\bigcup_{q\in Q_{a}}C_{q}.$$

If $J=\emptyset$, then $C_{q}=X$, which belongs to $\mathcal{F}$ by σ-Algebra and Measurable Space (i); if $J\neq\emptyset$, then $C_{q}=\bigcap_{k\in J}\{f_{k}\ge q\}$, the intersection of the map $k\mapsto\{f_{k}\ge q\}$ from $J$ to $\mathcal{F}$, its values lying in $\mathcal{F}$ by the paragraph on measurable superlevel sets (Preimages, Unions and Intersections over an Index Set, Suprema and Infima, and Superlevel Sets as Typed Terms (vi), Preimages, Unions and Intersections over an Index Set, Suprema and Infima, and Superlevel Sets as Typed Terms (v)), which belongs to $\mathcal{F}$ by the paragraph on countable index sets. So the values $C_{q}$ lie in $\mathcal{F}$, and $q\mapsto C_{q}$ is a map from $Q_{a}$ to $\mathcal{F}$: for $J=\emptyset$ it is the map with constant value $X$ (Preimages, Unions and Intersections over an Index Set, Suprema and Infima, and Superlevel Sets as Typed Terms (vi)), and for $J\neq\emptyset$ it is $q\mapsto\bigcap_{k\in J}\{f_{k}\ge q\}$ (Preimages, Unions and Intersections over an Index Set, Suprema and Infima, and Superlevel Sets as Typed Terms (vi), Preimages, Unions and Intersections over an Index Set, Suprema and Infima, and Superlevel Sets as Typed Terms (ii), Preimages, Unions and Intersections over an Index Set, Suprema and Infima, and Superlevel Sets as Typed Terms (v)); and $\{\iota>a\}\in\mathcal{F}$ by the same paragraph. So $\iota$ is measurable by Measurable Maps: Generators, Composition, Continuous Maps, Restrictions, and Criteria for Real- and [0,∞]-Valued Maps (vi), and with $J=\mathbb{N}$ this proves (ii).

Limits inferior and superior. For $m\in\mathbb{N}$, $m\in\{k\ge m\}$, since $m\le m$ for the order of $\mathbb{N}_{0}$, a well-order by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (v); so $\{k\ge m\}$ is a nonempty subset of $\mathbb{N}$. Hence $m\mapsto\{k\ge m\}$ is a map $T$ from $\mathbb{N}$ to $\mathcal{P}(\mathbb{N})$ (Maps and Relations Given by Formulas (i)), and its value $T(m)=\{k\ge m\}$ is a term of type $\mathcal{P}(\mathbb{N})$ under the guard $m\in\mathbb{N}$ (Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iii)); it is the index set of the intersections and unions over $k\ge m$ below. For $x\in X$, $\inf_{k\ge m}f_{k}(x)$ and $\sup_{k\ge m}f_{k}(x)$ exist by Order and Suprema in the Extended Real Line (iii) and lie in $[0,\infty]$ by Order and Suprema in the Extended Real Line (ix); so, by the same two clauses, $L(x)=\sup_{m}\inf_{k\ge m}f_{k}(x)$ and $M(x)=\inf_{m}\sup_{k\ge m}f_{k}(x)$ exist and lie in $[0,\infty]$, and $L$ and $M$ are maps $X\to[0,\infty]$. Let $a\in\mathbb{R}$ and $x\in X$.

We show that $L(x)>a$ if and only if there are $q\in Q_{a}$ and $m\in\mathbb{N}$ with $f_{k}(x)\ge q$ for every $k\ge m$. If there are such $q$ and $m$, then $q$ is a lower bound of $\{f_{k}(x):k\ge m\}$, so $q\le\inf_{k\ge m}f_{k}(x)\le L(x)$ by Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order (iv), and $a<q\le L(x)$. Conversely, let $L(x)>a$. By Order and Suprema in the Extended Real Line (x) there is $m\in\mathbb{N}$ with $a<\inf_{k\ge m}f_{k}(x)$, and by the paragraph on a rational between there is $q\in Q_{a}$ with $q<\inf_{k\ge m}f_{k}(x)$; then $f_{k}(x)\ge\inf_{k\ge m}f_{k}(x)>q$ for every $k\ge m$. Hence

$$\{L>a\}=\bigcup_{q\in Q_{a}}\bigcup_{m\in\mathbb{N}}\bigcap_{k\ge m}\{f_{k}\ge q\}.$$

For $q\in Q_{a}$ and $m\in\mathbb{N}$, $k\mapsto\{f_{k}\ge q\}$ is a map from $\{k\ge m\}$ to $\mathcal{F}$, its values lying in $\mathcal{F}$ by the paragraph on measurable superlevel sets (Preimages, Unions and Intersections over an Index Set, Suprema and Infima, and Superlevel Sets as Typed Terms (vi), Preimages, Unions and Intersections over an Index Set, Suprema and Infima, and Superlevel Sets as Typed Terms (v)), so $E_{q,m}=\bigcap_{k\ge m}\{f_{k}\ge q\}\in\mathcal{F}$ by the paragraph on countable index sets, $\{k\ge m\}$ being nonempty. Then $m\mapsto E_{q,m}$, an intersection over the index set $T(m)=\{k\ge m\}$ that depends on $m$, is a map from $\mathbb{N}$ to $\mathcal{F}$, its values lying in $\mathcal{F}$ (Preimages, Unions and Intersections over an Index Set, Suprema and Infima, and Superlevel Sets as Typed Terms (vi), Preimages, Unions and Intersections over an Index Set, Suprema and Infima, and Superlevel Sets as Typed Terms (ii), Preimages, Unions and Intersections over an Index Set, Suprema and Infima, and Superlevel Sets as Typed Terms (v)), so $G_{q}=\bigcup_{m\in\mathbb{N}}E_{q,m}\in\mathcal{F}$, and $q\mapsto G_{q}$ is a map from $Q_{a}$ to $\mathcal{F}$, its values lying in $\mathcal{F}$ (Preimages, Unions and Intersections over an Index Set, Suprema and Infima, and Superlevel Sets as Typed Terms (vi), Preimages, Unions and Intersections over an Index Set, Suprema and Infima, and Superlevel Sets as Typed Terms (ii), Preimages, Unions and Intersections over an Index Set, Suprema and Infima, and Superlevel Sets as Typed Terms (v)), so $\{L>a\}=\bigcup_{q\in Q_{a}}G_{q}\in\mathcal{F}$, by the same paragraph. By Measurable Maps: Generators, Composition, Continuous Maps, Restrictions, and Criteria for Real- and [0,∞]-Valued Maps (vi), $L$ is measurable, which proves (iii).

We show that $M(x)>a$ if and only if there is $q\in Q_{a}$ such that for every $m\in\mathbb{N}$ some $k\ge m$ has $f_{k}(x)>q$. If there is such a $q$, then for every $m\in\mathbb{N}$ there is $k\ge m$ with $q<f_{k}(x)\le\sup_{k'\ge m}f_{k'}(x)$, the supremum being an upper bound; so $q$ is a lower bound of $\{\sup_{k\ge m}f_{k}(x):m\in\mathbb{N}\}$, and $a<q\le M(x)$ by Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order (iv). Conversely, let $M(x)>a$. By the paragraph on a rational between there is $q\in Q_{a}$ with $q<M(x)$. For $m\in\mathbb{N}$, $M(x)\le\sup_{k\ge m}f_{k}(x)$, as $M(x)$ is a lower bound of the set of these suprema, so $q<\sup_{k\ge m}f_{k}(x)$, and by Order and Suprema in the Extended Real Line (x) some $k\ge m$ has $q<f_{k}(x)$. Hence

$$\{M>a\}=\bigcup_{q\in Q_{a}}\bigcap_{m\in\mathbb{N}}\bigcup_{k\ge m}\{f_{k}>q\}.$$

For $q\in Q_{a}$ and $m\in\mathbb{N}$, $k\mapsto\{f_{k}>q\}$ is a map from $\{k\ge m\}$ to $\mathcal{F}$, its values lying in $\mathcal{F}$ by the paragraph on measurable superlevel sets (Preimages, Unions and Intersections over an Index Set, Suprema and Infima, and Superlevel Sets as Typed Terms (vi), Preimages, Unions and Intersections over an Index Set, Suprema and Infima, and Superlevel Sets as Typed Terms (v)), so $H_{q,m}=\bigcup_{k\ge m}\{f_{k}>q\}\in\mathcal{F}$ by the paragraph on countable index sets. Then $m\mapsto H_{q,m}$, a union over the index set $T(m)=\{k\ge m\}$ that depends on $m$, is a map from $\mathbb{N}$ to $\mathcal{F}$, its values lying in $\mathcal{F}$ (Preimages, Unions and Intersections over an Index Set, Suprema and Infima, and Superlevel Sets as Typed Terms (vi), Preimages, Unions and Intersections over an Index Set, Suprema and Infima, and Superlevel Sets as Typed Terms (ii), Preimages, Unions and Intersections over an Index Set, Suprema and Infima, and Superlevel Sets as Typed Terms (v)), so $K_{q}=\bigcap_{m\in\mathbb{N}}H_{q,m}\in\mathcal{F}$, $\mathbb{N}$ being nonempty as it contains $1$; and $q\mapsto K_{q}$ is a map from $Q_{a}$ to $\mathcal{F}$, its values lying in $\mathcal{F}$ (Preimages, Unions and Intersections over an Index Set, Suprema and Infima, and Superlevel Sets as Typed Terms (vi), Preimages, Unions and Intersections over an Index Set, Suprema and Infima, and Superlevel Sets as Typed Terms (ii), Preimages, Unions and Intersections over an Index Set, Suprema and Infima, and Superlevel Sets as Typed Terms (v)), so $\{M>a\}=\bigcup_{q\in Q_{a}}K_{q}\in\mathcal{F}$, by the same paragraph. By Measurable Maps: Generators, Composition, Continuous Maps, Restrictions, and Criteria for Real- and [0,∞]-Valued Maps (vi), $M$ is measurable, which proves (iv).