ファイナイト（有限）メジャースペース（測度空間）上方の非ネガティブ（負）メジャラブル（測定可能）エクステンデッド（拡張された）リアル（実）ファンクション（関数）に対して、ファンクション（関数）はインテグラブル（積分可能）である、もしも、ローワークローズド（下方閉）ポジティブナチュラルナンバー（正自然数）バウンデッド（有界）インターバル（区間）たちのプリイメージ（前像）たちのメジャー（測度）たちの合計がコンバージ（収束）する場合、そしてその場合に限って、ことの記述/証明
話題
About: メジャースペース（測度空間）
この記事の目次
開始コンテキスト
- 読者は、メジャースペース（測度空間）のメジャラブルサブセット（測度空間部分集合）上方のルベーグインテグラブルエクステンデッド（拡張された）リアル（実）ファンクション（積分可能関数）の定義を知っている。
- 読者は、セット（集合）の\(\sigma\)-アルジェブラ（多元環）上方のファイナイト（有限）メジャー（測度）の定義を知っている。
- 読者は、メトリックスペース（計量付き空間）上のシーケンス（列）のコンバージェンス（収束ポイント）の定義を知っている。
- 読者は、フロワーマップ（写像）の定義を知っている。
- 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. 読者は、任意のメジャラブルスペース（測定可能空間）たち間任意のメジャラブルマップ（測定可能写像）に対して、変更して任意のメジャラブルサブセット（測定可能部分集合）を任意のメジャラブル（測定可能）な\(1\)ポイントへマップするようにしたマップ（写像）はメジャラブル（測定可能）であるという命題を認めている。
- 読者は、\(1\)-ディメンショナル（次元）ユークリディアンメジャラブルスペース（測定可能空間）の中への任意の非ネガティブ（負）メジャラブルマップ（測定可能写像）に対して、当該マップ（写像）の後にフロワーマップ（写像）を行なうコンポジション（合成）はメジャラブル（測定可能）であるという命題を認めている。
- 読者は、任意のメジャースペース（測度空間）上方のメジャラブル（測定可能）エクステンデッド（拡張された）リアル（実）ファンクション（関数）でそのレンジ（値域）がナチュラルナンバー（自然数）たちセット（集合）とインフィニティ（無限）のユニオン（和集合）内にある任意のものに対して、当該マップ（写像）のルベーグインテグラル（積分）は、全てのクローズド（閉）ポジティブ（正）ナチュラルナンバー（自然数）またはインフィニティ（無限）ローワーバウンデッド（下方有界）インターバル（区間）たちのプリイメージ（前像）たちのメジャー（測度）たちの合計であるという命題を認めている。
- 読者は、任意のマップ（写像）に対して、レンジ（値域）のマップ（写像）プリイメージ（前像）はドメイン（定義域）全体であるという命題を認めている。
- 読者は、任意のマップ（写像）に対して、任意の、セット（集合）たちのユニオン（和集合）、のマップ（写像）プリイメージ（前像）は、それらセット（集合）たちのマップ（写像）プリイメージ（前像）たちのユニオン（和集合）であるという命題を認めている。
- 読者は、任意のマップ（写像）に対して、任意の、セット（集合）たちのユニオン（和集合）、のマップ（写像）プリイメージ（前像）は、それらセット（集合）たちのマップ（写像）プリイメージ（前像）たちのユニオン（和集合）であるという命題を認めている。
- 読者は、任意のディスジョイント（互いに素な）サブセット（部分集合）たちの任意のマップ（写像）下のプリイメージ（前像）たちはディスジョイント（互いに素）であるという命題を認めている。
ターゲットコンテキスト
- 読者は、任意のファイナイト（有限）メジャースペース（測度空間）上方の任意の非ネガティブ（負）メジャラブル（測定可能）エクステンデッド（拡張された）リアル（実）ファンクション（関数）に対して、当該ファンクション（関数）はインテグラブル（積分可能）である、もしも、全てのローワークローズド（下方閉）ポジティブナチュラルナンバー（正自然数）バウンデッド（有界）インターバル（区間）たちのプリイメージ（前像）たちのメジャー（測度）たちの合計がコンバージ（収束）する場合、そしてその場合に限って、という命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\((M, A, \mu)\): \(\in \{\text{ 全てのファイナイト（有限）メジャースペース（測度空間）たち }\}\)
\(f\): \(: M \to [0, \infty]\), \(\in \{\text{ 全てのメジャラブルマップ（測定可能写像）たち }\}\)
//
ステートメント（言明）たち:
\(f \in \{\text{ 全てのインテグラブルマップ（積分可能写像）たち }\}\)
\(\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: 証明
全体戦略: ステップ1: \(f\)を変更したもの\(f': M \to [0, \infty)\)を取る; ステップ2: \(f\)はインテグラブル（積分可能）であると仮定する; ステップ3: \(\int_M f d \mu = \int_M f' d \mu\)、\(fl' \circ f'\)はインテグラブル（積分可能）であること、\(\int_M fl' \circ f' d \mu = \sum_{n \in \mathbb{R} \setminus \{0\}} \mu (f^{-1} ([n, \infty]))\)を見る; ステップ4: \(\sum_{n \in \mathbb{R} \setminus \{0\}} \mu (f^{-1} ([n, \infty])) \lt \infty\)であると仮定する; ステップ5: \(f' \le fl' \circ (f' + 1)\)および\(\int_M fl' \circ (f' + 1) d \mu = \mu (M) + \sum_{n \in \mathbb{R} \setminus \{0\}} \mu (f^{-1} ([n, \infty]))\)であることを見る; ステップ6: \(\sum_{n \in \mathbb{R} \setminus \{0\}} \mu (f^{-1} ([n, \infty])) \lt \infty\)、もしも、\(\sum_{n \in \mathbb{R}} \mu (f^{-1} ([n, \infty])) \lt \infty\)である場合、そしてその場合に限って、であることを見る。
ステップ1:
\(f': M \to [0, \infty), m \mapsto f (m) \text{ 、 } m \notin f^{-1} (\{\infty\}) \text{ である時 }, \mapsto 0 \text{ 、 } m \in f^{-1} (\{\infty\}) \text{ である時 }\)を取ろう。
\(f'\)はメジャラブル（測定可能）である、任意のメジャラブルスペース（測定可能空間）たち間任意のメジャラブルマップ（測定可能写像）に対して、変更して任意のメジャラブルサブセット（測定可能部分集合）を任意のメジャラブル（測定可能）な\(1\)ポイントへマップするようにしたマップ（写像）はメジャラブル（測定可能）であるという命題によって: \(f^{-1} (\{\infty\}) \subseteq M\)はメジャラブル（測定可能）である、そして、\(\{0\} \subseteq [0, \infty]\)はメジャラブル（測定可能）である。
ステップ2:
\(f\)はインテグラブル（積分可能）であると仮定しよう。
ステップ3:
\(f\)はインテグラブル（積分可能）であるから、\(\mu (f^{-1} (\{\infty\})) = 0\)、なぜなら、そうでなかったら、メジャラブルシンプルマップ（測定可能単純写像）で任意の大きい値\(r\)を\(f^{-1} (\{\infty\})\)上方で持ったものがあることになり、当該インテグラル（積分）は、\(r \mu (f^{-1} (\{\infty\}))\)より任意に大きいことになる、それが意味することになるのは、\(\int_M f d \mu = \infty\)、矛盾。
したがって、\(\int_M f d \mu = \int_M f' d \mu\)、なぜなら、メジャー（測度）\(0\) \(f^{-1} (\{\infty\})\)上方の値たちの変更は当該インテグラル（積分）を変えない。
\(f'\)は\([0, \infty)\)の中へのものであるので、\(fl' \circ f': M \to \mathbb{R}\)、ここで、\(fl'\)は当該フロワーマップ（写像）のコドメイン（余域）エクステンション（拡張）、は妥当であり、メジャラブル（測定可能）である、\(1\)-ディメンショナル（次元）ユークリディアンメジャラブルスペース（測定可能空間）の中への任意の非ネガティブ（負）メジャラブルマップ（測定可能写像）に対して、当該マップ（写像）の後にフロワーマップ（写像）を行なうコンポジション（合成）はメジャラブル（測定可能）であるという命題によって。
\(fl' \circ f' \le f'\)、したがって、\(fl' \circ f'\)はインテグラブル（積分可能）である。
\(\int_M fl' \circ f' d \mu = \sum_{n \in (\mathbb{N} \cup \{\infty\}) \setminus \{0\}} \mu ((fl' \circ f')^{-1} ([n, \infty]))\)、任意のメジャースペース（測度空間）上方のメジャラブル（測定可能）エクステンデッド（拡張された）リアル（実）ファンクション（関数）でそのレンジ（値域）がナチュラルナンバー（自然数）たちセット（集合）とインフィニティ（無限）のユニオン（和集合）内にある任意のものに対して、当該マップ（写像）のルベーグインテグラル（積分）は、全てのクローズド（閉）ポジティブ（正）ナチュラルナンバー（自然数）またはインフィニティ（無限）ローワーバウンデッド（下方有界）インターバル（区間）たちのプリイメージ（前像）たちのメジャー（測度）たちの合計であるという命題によって。
\(= \sum_{n \in \mathbb{N} \setminus \{0\}} \mu ((fl' \circ f')^{-1} ([n, \infty]))\)、なぜなら、\(\mu ((fl' \circ f')^{-1} (\{\infty\})) = 0\)、\(= \sum_{n \in \mathbb{N} \setminus \{0\}} \mu ((fl' \circ f')^{-1} ([n, \infty)))\)、なぜなら、\(fl' \circ f'\)は\(\infty\)を取らない、いずれにせよ。
しかし、\((fl' \circ f')^{-1} ([n, \infty)) = f^{-1} ([n, \infty))\)、なぜなら、各\(m \in (fl' \circ f')^{-1} ([n, \infty))\)に対して、\(fl' \circ f' (m) \in [n, \infty)\)、しかし、\(fl' \circ f' (m) = fl' \circ f (m)\)、なぜなら、\(1 \le fl' \circ f' (m)\)であるので、\(f (m) \lt \infty\)、そして、\(n \le fl' \circ f (m) \le f (m)\)であるので、\(f (m) \in [n, \infty)\)、したがって、\(m \in f^{-1} ([n, \infty))\); 各\(m \in f^{-1} ([n, \infty))\)に対して、\(f (m) \in [n, \infty)\)、そして、\(fl' \circ f' (m) \in [n, \infty)\)、したがって、\(m \in (fl' \circ f')^{-1} ([n, \infty))\)。
したがって、\(= \sum_{n \in \mathbb{N} \setminus \{0\}} \mu (f^{-1} ([n, \infty))) = \sum_{n \in \mathbb{N} \setminus \{0\}} \mu (f^{-1} ([n, \infty]))\)、なぜなら、\(\mu (f^{-1} ([n, \infty])) = \mu (f^{-1} ([n, \infty) \cup \{\infty\})) = \mu (f^{-1} ([n, \infty)) \cup f^{-1} (\{\infty\}))\)、任意のマップ（写像）に対して、任意の、セット（集合）たちのユニオン（和集合）、のマップ（写像）プリイメージ（前像）は、それらセット（集合）たちのマップ（写像）プリイメージ（前像）たちのユニオン（和集合）であるという命題によって、\(= \mu (f^{-1} ([n, \infty)) + \mu (f^{-1} (\{\infty\})\)、任意のディスジョイント（互いに素な）サブセット（部分集合）たちの任意のマップ（写像）下のプリイメージ（前像）たちはディスジョイント（互いに素）であるという命題によって、\(= \mu (f^{-1} ([n, \infty)) + 0\)。
したがって、\(\sum_{n \in \mathbb{N} \setminus \{0\}} \mu (f^{-1} ([n, \infty])) = \int_M fl' \circ f' d \mu \lt \infty\)。
ステップ4:
\(\sum_{n \in \mathbb{R} \setminus \{0\}} \mu (f^{-1} ([n, \infty])) \lt \infty\)であると仮定しよう。
ステップ5:
\(f' \le fl' \circ (f' + 1)\)、なぜなら、各\(m \in M\)に対して、\(f' (m) = n + r'\)、ここで、\(n \in \mathbb{N}\)および\(0 \le r' \lt 1\)、そして、\(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]))\)、任意のメジャースペース（測度空間）上方のメジャラブル（測定可能）エクステンデッド（拡張された）リアル（実）ファンクション（関数）でそのレンジ（値域）がナチュラルナンバー（自然数）たちセット（集合）とインフィニティ（無限）のユニオン（和集合）内にある任意のものに対して、当該マップ（写像）のルベーグインテグラル（積分）は、全てのクローズド（閉）ポジティブ（正）ナチュラルナンバー（自然数）またはインフィニティ（無限）ローワーバウンデッド（下方有界）インターバル（区間）たちのプリイメージ（前像）たちのメジャー（測度）たちの合計であるという命題によって、\(= \sum_{n \in \mathbb{N} \setminus \{0\}} \mu ((fl' \circ (f' + 1))^{-1} ([n, \infty)))\)、なぜなら、\(fl' \circ (f' + 1)\)は\(\infty\)を取らない、いずれにせよ。
しかし、\((fl' \circ (f' + 1))^{-1} ([n, \infty))\)は\(M\)である、\(n = 1\)である時は、そして、\(f^{-1} ([n - 1 , \infty))\)である、\(1 \lt n\)である時は、なぜなら、\(n = 1\)である時は、\([n, \infty) = [1, \infty)\)は\(fl' \circ (f' + 1)\)のレンジ（値域）を包含する、なぜなら、\(f'\)は\([0, \infty)\)の中へのものであるから、\(f' + 1\)は\([1, \infty)\)の中へのものである、そして、\(fl' \circ (f' + 1)\)は\([1, \infty)\)の中へのものである、そして、任意のマップ（写像）に対して、レンジ（値域）のマップ（写像）プリイメージ（前像）はドメイン（定義域）全体であるという命題が適用される、そして、\(1 \lt n\)である時は、各\(m \in (fl' \circ (f' + 1))^{-1} ([n, \infty))\)に対して、\(fl' \circ (f' + 1) (m) \in [n, \infty)\)、\(f' (m) = n' + r'\)、ここで、\(n' \in \mathbb{N}\)および\(0 \le r' \lt 1\)、\(1 \lt n \le fl' \circ (f' + 1) (m) = n' + 1\)、したがって、\(0 \lt n'\)、したがって、\(f (m) = f' (m)\)、したがって、\(n - 1 \le n' \le f (m) \lt \infty\)、したがって、\(f (m) \in [n - 1 , \infty)\)、したがって、\(m \in f^{-1} ([n - 1 , \infty))\); 各\(m \in f^{-1} ([n - 1 , \infty))\)に対して、\(f (m) \in [n - 1 , \infty)\)、したがって、\(f' (m) = f (m) \in [n - 1, \infty)\)、そして、\(fl' \circ (f' + 1) (m) \in [n, \infty)\)、したがって、\(m \in (fl' \circ (f' + 1))^{-1} ([n, \infty))\)。
したがって、\(\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))\)。
しかし、\(\mu (f^{-1} (\{\infty\})) = 0\)、なぜなら、そうでなかったら、\(\mu (f^{-1} ([n, \infty]) = \mu (f^{-1} ([n, \infty) \cup \{\infty\}) = \mu (f^{-1} ([n, \infty) \cup f^{-1} (\{\infty\}))\)、任意のマップ（写像）に対して、任意の、セット（集合）たちのユニオン（和集合）、のマップ（写像）プリイメージ（前像）は、それらセット（集合）たちのマップ（写像）プリイメージ（前像）たちのユニオン（和集合）であるという命題によって、\(= \mu (f^{-1} ([n, \infty)) + \mu (f^{-1} (\{\infty\})\)、任意のディスジョイント（互いに素な）サブセット（部分集合）たちの任意のマップ（写像）下のプリイメージ（前像）たちはディスジョイント（互いに素）であるという命題によって、そして、\(\sum_{n \in \mathbb{N} \setminus \{0\}} \mu (f^{-1} ([n, \infty])\)は\(\infty\)であることになる、当該仮定に反する矛盾、したがって、\(\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\)。
したがって、\(\int_M f' d \mu \lt \infty\)。
\(\int_M f d \mu = \int_M f' d \mu\)、なぜなら、\(\mu (f^{-1} (\{\infty\})) = 0\)。
したがって、\(\int_M f d \mu \lt \infty\)。
ステップ6:
もしも、\(\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\)。
もしも、\(\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\)。
