Dyadic Approximations of a Map into [0,∞]

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $\infty$ and $[0,\infty]$ be as in The Extended Real Line, Its Order, and [0,∞] (i) and The Extended Real Line, Its Order, and [0,∞] (ii), so that $x\in[0,\infty]$ if and only if either $x\in\mathbb{R}$ and $0\le x$, or $x=\infty$. Natural numbers and integers are read in $\mathbb{R}$ as in The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness (v); in particular $2$, and $m\in\mathbb{N}$ below, standing where a real number is required, denote their images in $\mathbb{R}$ as numerals, as in Commutative Rings, Fields and Ordered Fields: Standard Notation (iv), which agrees with the reading of The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness (v) by The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness (iv). For $z\in\mathbb{R}$, $\lfloor z\rfloor$ is the integer part of $z$, an integer and so a real number. For $m\in\mathbb{N}$, $2^{m}$ is the power of $2$ in $\mathbb{R}$, which is $>0$ by Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality (vi), and $2^{-m}=1/2^{m}$. For $y,z\in\mathbb{R}$, $\min\{y,z\}$ is formed in $\mathbb{R}$ as in The Maximum and Minimum of Two Elements of a Total Order (i) (it is $y$ if $y\le z$ and $z$ if $z\le y$, by The Maximum and Minimum of Two Elements of a Total Order (ii)). For a set $X$, $\mathbb{R}^{X}$ is the set of maps from $X$ to $\mathbb{R}$ of The Class of All Functions from One Set to Another (i). Let $X$ be a set and let $g:X\to[0,\infty]$ be a map.

(i) For $m\in\mathbb{N}$, the dyadic approximation of $g$ of order $m$ is the map $s_{m}(g):X\to\mathbb{R}$ with

$$s_{m}(g)(x)=\min\bigl\{m,\;2^{-m}\lfloor2^{m}g(x)\rfloor\bigr\}\ \text{ if }g(x)\in\mathbb{R},\qquad s_{m}(g)(x)=m\ \text{ if }g(x)=\infty,$$

for $x\in X$. It exists and is unique by Maps Defined by Cases (i), applied to the predicative condition $g(x)\in\mathbb{R}$, to the expression $\min\{m,2^{-m}\lfloor2^{m}g(x)\rfloor\}$, an element of $\mathbb{R}$ whenever $g(x)\in\mathbb{R}$ (with $2^{m}g(x)$ the product in $\mathbb{R}$, $m$ read in $\mathbb{R}$ as in The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness (v), and $\lfloor2^{m}g(x)\rfloor$ the value at $2^{m}g(x)$ of the integer-part map of Maps Used to Build the Integral: Fibres of a Map, Pointwise Combinations with Finite Image, Tail Extrema of a Sequence of Maps, the Integer Part, and Indicators (iv)), and to the expression $m$, an element of $\mathbb{R}$ as $m\in\mathbb{N}$ is read in $\mathbb{R}$ by The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness (v); for $x\in X$ with $g(x)\notin\mathbb{R}$ we have $g(x)=\infty$.

(ii) The sequence of dyadic approximations of $g$ is the sequence $(s_{m}(g))_{m\in\mathbb{N}}$ in $\mathbb{R}^{X}$, that is, the map $\mathbb{N}\to\mathbb{R}^{X}$ with value $s_{m}(g)$ at every $m\in\mathbb{N}$ (it exists and is unique by Maps Formed Pointwise: Constant Maps, Pairs of Values, Maps Applied to Values, and Families of Maps (iv) and Maps Formed Pointwise: Constant Maps, Pairs of Values, Maps Applied to Values, and Families of Maps (iii), applied to the map $G:\mathbb{N}\times X\to\mathbb{R}$ with $G(m,x)=s_{m}(g)(x)$, which exists by Maps Defined by Cases (i) as in (i), with the set $\mathbb{N}\times X$ in place of $X$ and the condition and the expressions written, for $p=(m,x)\in\mathbb{N}\times X$, in the components $p_{1}=m$ and $p_{2}=x$ of $p$; its value $G(m,\cdot)$ at $m$ is $s_{m}(g)$ by the uniqueness in (i)).