Royal Road to Topology Chapter XXII
Chapter 22: Implementations and Refinements
Section titled “Chapter 22: Implementations and Refinements”全9節・全39ページの雑多な応用章。guide.md ロードマップの「XXII(9)」注記が示す通り、測度論的確率統計への到達目標として本質的なのは §9 のみ。§1–8（active boundary・topological defect・sequential cascade・subsequential topology・topologically maximal pretopology・Stone 位相の応用・homogeneity quest・非 Fréchet 正方形をもつコンパクト Fréchet 位相）は、収束の分類学（本書独自の高度な抽象化）を駆使した専門的な反例構成が中心で、§9 の証明・定義のいずれからも参照されない独立した節であることを PDF 精読で確認した（issue #16 コメント参照）。そのため 本章のカード化は §9 のみとし、§1–8 はカード化しない（辞書カードも不要——§9 が依拠しないため）。
数学的意味（原著より）
Section titled “数学的意味（原著より）”XXII.9 導入：測度論の列収束を filter 収束へ埋め込む
Section titled “XXII.9 導入：測度論の列収束を filter 収束へ埋め込む”著者は XXII.9 冒頭で、測度は可算加法的なので測度論の収束概念が列で定義されるのは自然だと述べる。その上で、古典的な列収束（測度収束・概一様収束・概収束）をまず確認し、ついで filter の収束理論へ埋め込むという方針を明示する。
出典:
refs/math/topology/royal-road-to-topology/pdfs/chp22-2024-implementations-and-refinements.pdfp.545
Definition XXII.9.1：三つの古典収束を同一面で比較
Section titled “Definition XXII.9.1：三つの古典収束を同一面で比較”XXII.9.1 では in measure / almost uniform / almost everywhere が並置され、以後の命題で含意関係や分岐を追う準備が整えられる。ここが本書で測度論を収束空間論へ接続する入口である。
出典: p.546
§9 の到達点：同値類上の位相化と非自明な分岐
Section titled “§9 の到達点：同値類上の位相化と非自明な分岐”後半では $\mu$-a.e. 同値類への商化、測度収束の距離化可能性、そして可算台修正や擬位相修正の間の非包含が示される。これは「列では自然に見える関係が filter 拡張で壊れる」ことを明確化し、測度論的収束の本質を抽出する節になっている。
出典: p.549–555
XXII.9. Measure-theoretic Convergences
Section titled “XXII.9. Measure-theoretic Convergences”測度論の3つの古典的な列収束（測度収束・概一様収束・概収束、Def XXII.9.1）を、収束空間論の一般装置（sequentially founded convergence・countably carried modification・pseudotopology・Urysohn modification）を使ってフィルターの言葉に埋め込み、含意関係・完備性・距離化可能性・（非）測度論的性・（非）擬位相性を確定する節。
- cards/topology/classical-measure-theoretic-convergences
- 📐 cards/topology/prop-xxii-9-2-uniform-implies-everywhere
- 📐 cards/topology/prop-xxii-9-4-egorov-theorem
- 📐 cards/topology/lemma-xxii-9-5-uniform-implies-measure
- cards/topology/example-xxii-9-6-measure-not-everywhere
- 📐 cards/topology/lemma-xxii-9-7-fundamental-measure-subsequence
- 📐 cards/topology/prop-xxii-9-8-measure-convergence-complete
- 📐 cards/topology/prop-xxii-9-9-modifier-sequentially-founded
- cards/topology/measure-theoretic-convergence
- 📐 cards/topology/prop-xxii-9-10-measure-theoretic-characterization
- cards/topology/filter-convergence-almost-everywhere
- cards/topology/example-xxii-9-12-everywhere-filter-not-measure-theoretic
- 📐 cards/topology/prop-xxii-9-13-countably-carried-everywhere-measure-theoretic
- cards/topology/filter-convergence-almost-uniform
- 📐 cards/topology/prop-xxii-9-15-uniform-finer-everywhere
- cards/topology/filter-convergence-in-measure
- 📐 cards/topology/prop-xxii-9-17-uniform-finer-measure
- 📐 cards/topology/prop-xxii-9-18-measure-finest-continuous-family
- 📐 cards/topology/cor-xxii-9-19-lebesgue-measure-metrizable
- 📐 cards/topology/cor-xxii-9-20-measure-urysohn-of-everywhere
- 📐 cards/topology/prop-xxii-9-21-countably-carried-uniform-not-pseudotopology
- cards/topology/example-xxii-9-24-everywhere-not-finer-uniform
- 📐 cards/topology/cor-xxii-9-25-pseudotopological-everywhere-not-finer-measure
[!IMPORTANT] 「素朴な列収束を測度論的なフィルター収束へ埋め込むと、直感的な包含関係の一部が壊れる」が §9 全体を貫く $$\text{測度}\mu\text{-収束（列）};\xleftarrow{\text{Egorov, 有限測度}};\text{概一様収束（列）};\Longrightarrow;\text{概収束（列）}$$ 列の世界（Def XXII.9.1）ではこの三者はきれいに整列する（概一様 ⟹ 概収束・測度収束、有限測度なら概収束 ⟹ 概一様＝Egorovの定理、測度収束は完備）。フィルターへ拡張すると（$e_\mu$: 概収束・$a_\mu$: 概一様・$m_\mu$: 測度収束）、$a_\mu\geq e_\mu,,a_\mu\geq m_\mu$ は保たれる（cards/topology/prop-xxii-9-15-uniform-finer-everywhere・cards/topology/prop-xxii-9-17-uniform-finer-measure）が、$e_\mu$ 自身は測度論的でない（cards/topology/example-xxii-9-12-everywhere-filter-not-measure-theoretic）——可算台修正 $\mathbb{E}$ を取って初めて測度論的になる（cards/topology/prop-xxii-9-13-countably-carried-everywhere-measure-theoretic）。
さらに一段深く、$\mathbb{E}a_\mu$ は擬位相ですらない（cards/topology/prop-xxii-9-21-countably-carried-uniform-not-pseudotopology：$[0,1]$上の「動く区間」列から作った超フィルター構成による）。そして $\mathbb{E}e_\mu\geq\mathbb{E}a_\mu$ という一見自然な包含も、Fremlin の反例（cards/topology/example-xxii-9-24-everywhere-not-finer-uniform）により成立しない。到達点は、$\mu$ が有界閉区間上の Lebesgue 測度のとき $[m_\mu]_\mu$ が距離化可能な位相になる（cards/topology/cor-xxii-9-19-lebesgue-measure-metrizable）という、測度論で馴染み深い事実の収束空間論的な再導出。
[!NOTE] 本書 ↔ Mathlib 規約ブリッジ（測度論的収束編）
本書 Mathlib 測度収束（$m_\mu$, Def XXII.9.16） MeasureTheory.TendstoInMeasure概収束（$e_\mu$, Def XXII.9.11） Filter.Eventually／MeasureTheory.ae（∀ᵐ x ∂μ, ...）概一様収束（$a_\mu$, Def XXII.9.14）・Egorov の定理（Prop XXII.9.4） MeasureTheory.Egorov（tendstoUniformlyOn_of_ae_tendsto等）測度論的収束（Def, $\xi=\Phi^-(\Phi\xi)$） 該当なし（Mathlib は最初から $\mu$-a.e. 同値類 MeasureTheory.Lp/AEEqFun上で作業するため、この区別自体が現れない）可算台修正 $\mathbb{E}$・sequentially founded・pseudotopology・Urysohn 修正 $U$ 該当なし（Mathlib の Filterは最初から超フィルターの言葉に自動的に還元されるため、本書のような収束の分類学は不要）$[m_\mu]_\mu$ の距離化可能性（Cor XXII.9.19） MeasureTheory.Lpの距離構造、またはMeasureTheory.TendstoInMeasure周辺の距離化補題
- 反例の要点: 概収束 $e_\mu$ は測度論的でなく（cards/topology/example-xxii-9-12-everywhere-filter-not-measure-theoretic）、可算台修正 $\mathbb{E}a_\mu$ は擬位相でなく（cards/topology/prop-xxii-9-21-countably-carried-uniform-not-pseudotopology）、$\mathbb{E}e_\mu\geq\mathbb{E}a_\mu$ も成立しない（cards/topology/example-xxii-9-24-everywhere-not-finer-uniform）——いずれも「可算個の例外集合の合併がなお測度0」という測度の可算加法性のギリギリの使い方に依存し、非可算個の例外・超フィルターの非構成的な性質が絡むと直ちに破綻する。
- 測度論への視線: 本節は「測度論の収束（測度収束・概一様収束・概収束）」を丸ごと収束空間論の言葉に翻訳する、本書の測度論的確率統計への到達目標の直接の到達点。Egorov の定理（cards/topology/prop-xxii-9-4-egorov-theorem）・測度収束の完備性（cards/topology/prop-xxii-9-8-measure-convergence-complete）・$L^0$ 位相の距離化可能性（cards/topology/cor-xxii-9-19-lebesgue-measure-metrizable）は確率論・関数解析で頻出する事実そのもの。「測度論的収束」という一般概念（$\mu$-a.e. の変更で収束が保たれる）は、確率変数の同値類上の収束を抽象的に特徴づける枠組みを与える。
- 深入り禁止: §1–8（active boundary・topological defect・sequential cascade・subsequential topology・topologically maximal pretopology・Stone 位相の応用・homogeneity quest・非 Fréchet 正方形）はカード化しない——§9 の証明・定義のいずれからも参照されないため（issue #16 コメントで確認済み）。§9 自身が依拠する第XVI章（sequentially founded convergence・Urysohn modification）・第XVIII章（pseudotopology・countably carried modification）も、guide.md が警告する「収束の分類学」への深入りを避け、§9 の理解に必要な最小限の辞書カードのみ（chapter16.md, chapter18.md 参照）で済ませた。