description/proof of that for non-negative measurable extended real function over finite measure space, function is integrable iff sum of measures of preimages of lower-closed-positive-natural-number-bounded intervals converges
Topics
About: measure space
The table of contents of this article
Starting Context
- The reader knows a definition of extended real function Lebesgue integrable over measurable subset of measure space.
- The reader knows a definition of finite measure over \(\sigma\)-algebra of set.
- The reader knows a definition of convergence of sequence on metric space.
- The reader knows a definition of floor map.
- The reader admits the proposition that for any measurable map between any measurable spaces, the modified map that maps any measurable subset to any measurable \(1\) point is measurable.
- The reader admits 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.
- The reader admits the proposition that for any measurable extended real function over any measure space whose range is in the union of the natural numbers set and the infinity, the Lebesgue integral of the map is the sum of the measures of the preimages of the closed-positive-natural-number-or-infinity-lower-bounded intervals.
- The reader admits the proposition that for any map, the map preimage of the range is the whole domain.
- The reader admits the proposition that for any map, the map preimage of any union of sets is the union of the map preimages of the sets.
- The reader admits the proposition that for any map, the map preimage of any union of sets is the union of the map preimages of the sets.
- The reader admits the proposition that the preimages of any disjoint subsets under any map are disjoint.
Target Context
- The reader will have a description and a proof of the proposition that for any non-negative measurable extended real function over any finite measure space, the function is integrable if and only if the sum of the measures of the preimages of the lower-closed-positive-natural-number-bounded intervals converges.
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, A, \mu)\): \(\in \{\text{ the finite measure spaces }\}\)
\(f\): \(: M \to [0, \infty]\), \(\in \{\text{ the measurable maps }\}\)
//
Statements:
\(f \in \{\text{ the integrable maps }\}\)
\(\iff\)
\(\sum_{n \in \mathbb{R} \setminus \{0\}} \mu (f^{-1} ([n, \infty])) \lt \infty\)
\(\iff\)
\(\sum_{n \in \mathbb{R}} \mu (f^{-1} ([n, \infty])) \lt \infty\)
//
2: Proof
Whole Strategy: Step 1: take the modified \(f\), \(f': M \to [0, \infty)\); Step 2: suppose that \(f\) is integrable; Step 3: see that \(\int_M f d \mu = \int_M f' d \mu\), \(fl' \circ f'\) is integrable, and \(\int_M fl' \circ f' d \mu = \sum_{n \in \mathbb{R} \setminus \{0\}} \mu (f^{-1} ([n, \infty]))\); Step 4: suppose that \(\sum_{n \in \mathbb{R} \setminus \{0\}} \mu (f^{-1} ([n, \infty])) \lt \infty\); Step 5: see that \(f' \le fl' \circ (f' + 1)\) and \(\int_M fl' \circ (f' + 1) d \mu = \mu (M) + \sum_{n \in \mathbb{R} \setminus \{0\}} \mu (f^{-1} ([n, \infty]))\); Step 6: see that \(\sum_{n \in \mathbb{R} \setminus \{0\}} \mu (f^{-1} ([n, \infty])) \lt \infty\) if and only if \(\sum_{n \in \mathbb{R}} \mu (f^{-1} ([n, \infty])) \lt \infty\).
Step 1:
Let us take \(f': M \to [0, \infty), m \mapsto f (m) \text{ when } m \notin f^{-1} (\{\infty\}), \mapsto 0 \text{ when } m \in f^{-1} (\{\infty\})\).
\(f'\) is measurable, by the proposition that for any measurable map between any measurable spaces, the modified map that maps any measurable subset to any measurable \(1\) point is measurable: \(f^{-1} (\{\infty\}) \subseteq M\) is measurable and \(\{0\} \subseteq [0, \infty]\) is measurable.
Step 2:
Let us suppose that \(f\) is integrable.
Step 3:
As \(f\) is integrable, \(\mu (f^{-1} (\{\infty\})) = 0\), because otherwise, there would be the measurable simple map that had any large value, \(r\), over \(f^{-1} (\{\infty\})\), and the integral would be any larger than \(r \mu (f^{-1} (\{\infty\}))\), which would mean that \(\int_M f d \mu = \infty\), a contradiction.
So, \(\int_M f d \mu = \int_M f' d \mu\), because the change of the values over measure \(0\) \(f^{-1} (\{\infty\})\) does not change the integral.
As \(f'\) is into \([0, \infty)\), \(fl' \circ f': M \to \mathbb{R}\) where \(fl'\) is the codomain extension of the floor map, is valid and is measurable, by 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.
\(fl' \circ f' \le f'\), so, \(fl' \circ f'\) is integrable.
\(\int_M fl' \circ f' d \mu = \sum_{n \in (\mathbb{N} \cup \{\infty\}) \setminus \{0\}} \mu ((fl' \circ f')^{-1} ([n, \infty]))\), by the proposition that for any measurable extended real function over any measure space whose range is in the union of the natural numbers set and the infinity, the Lebesgue integral of the map is the sum of the measures of the preimages of the closed-positive-natural-number-or-infinity-lower-bounded intervals.
\(= \sum_{n \in \mathbb{N} \setminus \{0\}} \mu ((fl' \circ f')^{-1} ([n, \infty]))\), because \(\mu ((fl' \circ f')^{-1} (\{\infty\})) = 0\), \(= \sum_{n \in \mathbb{N} \setminus \{0\}} \mu ((fl' \circ f')^{-1} ([n, \infty)))\), because \(fl' \circ f'\) does not take \(\infty\) anyway.
But \((fl' \circ f')^{-1} ([n, \infty)) = f^{-1} ([n, \infty))\), because for each \(m \in (fl' \circ f')^{-1} ([n, \infty))\), \(fl' \circ f' (m) \in [n, \infty)\), but \(fl' \circ f' (m) = fl' \circ f (m)\), because as \(1 \le fl' \circ f' (m)\), \(f (m) \lt \infty\), and as \(n \le fl' \circ f (m) \le f (m)\), \(f (m) \in [n, \infty)\), so, \(m \in f^{-1} ([n, \infty))\); for each \(m \in f^{-1} ([n, \infty))\), \(f (m) \in [n, \infty)\), then, \(fl' \circ f' (m) \in [n, \infty)\), so, \(m \in (fl' \circ f')^{-1} ([n, \infty))\).
So, \(= \sum_{n \in \mathbb{N} \setminus \{0\}} \mu (f^{-1} ([n, \infty))) = \sum_{n \in \mathbb{N} \setminus \{0\}} \mu (f^{-1} ([n, \infty]))\), because \(\mu (f^{-1} ([n, \infty])) = \mu (f^{-1} ([n, \infty) \cup \{\infty\})) = \mu (f^{-1} ([n, \infty)) \cup f^{-1} (\{\infty\}))\), by the proposition that for any map, the map preimage of any union of sets is the union of the map preimages of the sets, \(= \mu (f^{-1} ([n, \infty)) + \mu (f^{-1} (\{\infty\})\), by the proposition that the preimages of any disjoint subsets under any map are disjoint, \(= \mu (f^{-1} ([n, \infty)) + 0\).
So, \(\sum_{n \in \mathbb{N} \setminus \{0\}} \mu (f^{-1} ([n, \infty])) = \int_M fl' \circ f' d \mu \lt \infty\).
Step 4:
Let us suppose that \(\sum_{n \in \mathbb{R} \setminus \{0\}} \mu (f^{-1} ([n, \infty])) \lt \infty\).
Step 5:
\(f' \le fl' \circ (f' + 1)\), because for each \(m \in M\), \(f' (m) = n + r'\) where \(n \in \mathbb{N}\) and \(0 \le r' \lt 1\), and \(fl' \circ (f' + 1) (m) = fl' (n + 1 + r') = n + 1\).
\(\int_M fl' \circ (f' + 1) d \mu = \sum_{n \in (\mathbb{N} \cup \{\infty\}) \setminus \{0\}} \mu ((fl' \circ (f' + 1))^{-1} ([n, \infty]))\), by the proposition that for any measurable extended real function over any measure space whose range is in the union of the natural numbers set and the infinity, the Lebesgue integral of the map is the sum of the measures of the preimages of the closed-positive-natural-number-or-infinity-lower-bounded intervals, \(= \sum_{n \in \mathbb{N} \setminus \{0\}} \mu ((fl' \circ (f' + 1))^{-1} ([n, \infty)))\), because \(fl' \circ (f' + 1)\) does not take \(\infty\) anyway.
But \((fl' \circ (f' + 1))^{-1} ([n, \infty))\) is \(M\) when \(n = 1\) and is \(f^{-1} ([n - 1 , \infty))\) when \(1 \lt n\), because when \(n = 1\), \([n, \infty) = [1, \infty)\) contains the range of \(fl' \circ (f' + 1)\), because as \(f'\) is into \([0, \infty)\), \(f' + 1\) is into \([1, \infty)\), and so, \(fl' \circ (f' + 1)\) is into \([1, \infty)\), and the proposition that for any map, the map preimage of the range is the whole domain applies, and when \(1 \lt n\), for each \(m \in (fl' \circ (f' + 1))^{-1} ([n, \infty))\), \(fl' \circ (f' + 1) (m) \in [n, \infty)\), \(f' (m) = n' + r'\) where \(n' \in \mathbb{N}\) and \(0 \le r' \lt 1\), \(1 \lt n \le fl' \circ (f' + 1) (m) = n' + 1\), so, \(0 \lt n'\), so, \(f (m) = f' (m)\), so, \(n - 1 \le n' \le f (m) \lt \infty\), so, \(f (m) \in [n - 1 , \infty)\), and so, \(m \in f^{-1} ([n - 1 , \infty))\); for each \(m \in f^{-1} ([n - 1 , \infty))\), \(f (m) \in [n - 1 , \infty)\), so, \(f' (m) = f (m) \in [n - 1, \infty)\), and \(fl' \circ (f' + 1) (m) \in [n, \infty)\), and so, \(m \in (fl' \circ (f' + 1))^{-1} ([n, \infty))\).
So, \(\int_M fl' \circ (f' + 1) d \mu = \sum_{n \in \mathbb{N} \setminus \{0\}} \mu ((fl' \circ (f' + 1))^{-1} ([n, \infty)) = \mu (M) + \sum_{n \in \mathbb{N} \setminus \{0, 1\}} \mu (f^{-1} ([n - 1, \infty))) = \mu (M) + \sum_{n \in \mathbb{N} \setminus \{0\}} \mu (f^{-1} ([n, \infty))\).
But \(\mu (f^{-1} (\{\infty\})) = 0\), because otherwise, \(\mu (f^{-1} ([n, \infty]) = \mu (f^{-1} ([n, \infty) \cup \{\infty\}) = \mu (f^{-1} ([n, \infty) \cup f^{-1} (\{\infty\}))\), by the proposition that for any map, the map preimage of any union of sets is the union of the map preimages of the sets, \(= \mu (f^{-1} ([n, \infty)) + \mu (f^{-1} (\{\infty\})\), by the proposition that the preimages of any disjoint subsets under any map are disjoint, and \(\sum_{n \in \mathbb{N} \setminus \{0\}} \mu (f^{-1} ([n, \infty])\) would be \(\infty\), a contradiction against the supposition, so, \(\mu (f^{-1} ([n, \infty)) = \mu (f^{-1} ([n, \infty])\).
\(\int_M fl' \circ (f' + 1) d \mu = \mu (M) + \sum_{n \in \mathbb{N} \setminus \{0\}} \mu (f^{-1} ([n, \infty]) \lt \infty\).
So, \(\int_M f' d \mu \lt \infty\).
\(\int_M f d \mu = \int_M f' d \mu\), because \(\mu (f^{-1} (\{\infty\})) = 0\).
So, \(\int_M f d \mu \lt \infty\).
Step 6:
If \(\sum_{n \in \mathbb{R} \setminus \{0\}} \mu (f^{-1} ([n, \infty])) \lt \infty\), \(\sum_{n \in \mathbb{R}} \mu (f^{-1} ([n, \infty])) = \mu (f^{-1} ([0, \infty])) + \sum_{n \in \mathbb{R} \setminus \{0\}} \mu (f^{-1} ([n, \infty])) = \mu (M) + \sum_{n \in \mathbb{R} \setminus \{0\}} \mu (f^{-1} ([n, \infty])) \lt \infty\).
If \(\sum_{n \in \mathbb{R}} \mu (f^{-1} ([n, \infty])) \lt \infty\), \(\sum_{n \in \mathbb{R} \setminus \{0\}} \mu (f^{-1} ([n, \infty])) \le \sum_{n \in \mathbb{R}} \mu (f^{-1} ([n, \infty])) \lt \infty\).
