description/proof of that for non-negative measurable map into \(1\)-dimensional Euclidean measurable space, composition of floor Map after map is measurable
Topics
About: set
The table of contents of this article
Starting Context
- 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 measurable map between measurable spaces.
- The reader knows a definition of floor map.
- The reader knows a definition of subspace \(\sigma\)-algebra of subset of measurable space.
- The reader admits the proposition that for any measurable map between any measurable spaces, the restriction on any domain subspace and any codomain subspace is measurable.
- The reader admits the proposition that the floor map with the codomain extended to the \(1\)-dimensional Euclidean measurable space is measurable.
- The reader admits the proposition that for any measurable maps between any arbitrary subspaces of any measurable spaces, the composition is measurable.
Target Context
- The reader will have a description and a proof of the proposition that for any non-negative measurable map into the \(1\)-dimensional Euclidean measurable space, the composition of the floor Map after the map as into 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:
\(M_1\): \(\in \{\text{ the measurable spaces }\}\)
\(\mathbb{R}\): \(= \text{ the Euclidean topological space }\) with the Borel \(\sigma\)-algebra
\([0, \infty)\): \(\subseteq \mathbb{R}\), with the subspace \(\sigma\)-algebra
\(f\): \(: M_1 \to \mathbb{R}\), \(\in \{\text{ the measurable maps }\}\), such that \(0 \le f\)
\(f'\): \(: M_1 \to [0, \infty)\), \(= \text{ the codomain restriction of } f\)
\(fl\): \(: [0, \infty) \to \mathbb{N}\)
\(fl'\): \(: [0, \infty) \to \mathbb{R}\), \(= \text{ the codomain extension of } fl\)
\(fl' \circ f'\): \(: M_1 \to \mathbb{R}\)
//
Statements:
\(fl' \circ f' \in \{\text{ the measurable maps }\}\)
//
2: Note
\(fl' \circ f'\) is \(fl \circ f\) loosely speaking, but we need \(f'\) and \(fl'\) formally, because \(fl \circ f\) does not make sense strictly speaking, because any composition is allowed only when the codomain of a map is contained in the domain of the succeeding map and \(fl \circ f'\) is \(: M \to \mathbb{N}\).
3: Proof
Whole Strategy: Step 1: see that \(f'\) is measurable; Step 2: see that \(fl'\) is measurable; Step 3: conclude the proposition.
Step 1:
\(f'\) is measurable, by the proposition that for any measurable map between any measurable spaces, the restriction on any domain subspace and any codomain subspace is measurable.
Step 2:
\(fl'\) is measurable, by the proposition that the floor map with the codomain extended to the \(1\)-dimensional Euclidean measurable space is measurable.
Step 3:
\(fl' \circ f'\) is measurable, by the proposition that for any measurable maps between any arbitrary subspaces of any measurable spaces, the composition is measurable.
