description/proof of that floor map with codomain extended to \(1\)-dimensional Euclidean measurable space is measurable
Topics
About: measurable space
The table of contents of this article
Starting Context
- The reader knows a definition of floor map.
- The reader knows a definition of Euclidean topological space.
- The reader knows a definition of Borel \(\sigma\)-algebra of topological space.
- The reader knows a definition of subspace \(\sigma\)-algebra of subset of measurable space.
- The reader knows a definition of measurable map between measurable spaces.
- The reader admits the proposition that the Borel \(\sigma\)-algebra of the \(1\)-dimensional Euclidean topological space is generated by the set of the upper-open-bounded intervals, the set of the upper-closed-bounded intervals, the set of the lower-open-bounded intervals, the set of the lower-closed-bounded intervals, the set of the lower-open-upper-open-bounded intervals, the set of the lower-open-upper-closed-bounded intervals, the set of the lower-closed-upper-open-bounded intervals, or the set of the lower-closed-upper-closed-bounded intervals.
- The reader admits the proposition that for any map between any measurable spaces, if the preimage of each element of any generator of the codomain \(\sigma\)-algebra is measurable, the map is measurable.
Target Context
- The reader will have a description and a proof of the proposition that the floor map with the codomain extended to the \(1\)-dimensional Euclidean measurable space is measurable.
Orientation
There is a list of definitions discussed so far in this site.
There is a list of propositions discussed so far in this site.
Main Body
1: Structured Description
Here is the rules of Structured Description.
Entities:
\(\mathbb{R}\): \(= \text{ the Euclidean topological space }\) with the Borel \(\sigma\)-algebra
\([0, \infty)\): \(\subseteq \mathbb{R}\), with the subspace \(\sigma\)-algebra
\(fl\): \(: [0, \infty) \to \mathbb{N}, r \mapsto Max (\{n \in \mathbb{N} \vert n \le r\})\)
\(fl'\): \(: [0, \infty) \to \mathbb{R}\), \(= \text{ the codomain extension of } fl\)
//
Statements:
\(fl' \in \{\text{ the measurable maps }\}\)
//
2: Note
As an immediate corollary, \(fl\) is measurable with \(\mathbb{N}\) as the subspace \(\sigma\)-algebra, by the proposition that for any measurable map between any measurable spaces, the restriction on any domain subspace and any codomain subspace is measurable.
3: Proof
Whole Strategy: Step 1: see that \(B (\mathbb{R})\) is generated by \(\{(- \infty, r] \subseteq \mathbb{R} \vert r \in \mathbb{R}\}\); Step 2: see that \({fl'}^{-1} ((- \infty, r])\) is measurable; Step 3: conclude the proposition.
Step 1:
\(B (\mathbb{R})\) is generated by \(\{(- \infty, r] \subseteq \mathbb{R} \vert r \in \mathbb{R}\}\), by the proposition that the Borel \(\sigma\)-algebra of the \(1\)-dimensional Euclidean topological space is generated by the set of the upper-open-bounded intervals, the set of the upper-closed-bounded intervals, the set of the lower-open-bounded intervals, the set of the lower-closed-bounded intervals, the set of the lower-open-upper-open-bounded intervals, the set of the lower-open-upper-closed-bounded intervals, the set of the lower-closed-upper-open-bounded intervals, or the set of the lower-closed-upper-closed-bounded intervals.
Step 2:
Let us see that \({fl'}^{-1} ((- \infty, r]) \subseteq [0, \infty)\) is measurable.
When \(r \lt 0\), \({fl'}^{-1} ((- \infty, r]) = \emptyset\) is measurable.
Otherwise, \({fl'}^{-1} ((- \infty, r]) = [0, fl (r + 1))\), because for each \(r' \in {fl'}^{-1} ((- \infty, r])\), \(fl' (r') \in (- \infty, r]\), so, \(fl (r') = fl' (r') \le r\), so, \(r' \lt fl (r + 1)\), by the property 5) mentioned in Note for the definition of floor map, so, \(r' \in [0, fl (r + 1))\); for each \(r' \in [0, fl (r + 1))\), \(r' \lt fl (r + 1)\), so, \(fl' (r') = fl (r') \le r\), by the property 5) mentioned in Note for the definition of floor map, so, \(fl' (r') \in (- \infty, r]\), so, \(r' \in {fl'}^{-1} ((- \infty, r])\), and \([0, fl (r + 1)) = (- \infty, fl (r + 1)) \cap [0, \infty)\) is measurable.
Step 3:
So, \(fl'\) is measurable, by the proposition that for any map between any measurable spaces, if the preimage of each element of any generator of the codomain \(\sigma\)-algebra is measurable, the map is measurable.
