5.4. Carathéodory条件との比較
Lebesgue外測度に関するCarathéodory可測性.
集合 A\subset\RR^d がLebesgue外測度 \lambda^* に関してCarathéodory可測であるとは，
任意の E\subset\RR^d に対して
\lambda^*(E)
=
\lambda^*(E\cap A)+\lambda^*(E\setminus A)
が成り立つことをいう．この等式をCarathéodory条件という．
Lean code for Definition5.4.1●1 definition
Associated Lean declarations
-
defdefined in NoteKsk/«05lebesgue-measure».leancomplete
def NoteKsk.Chapter05.LebesgueCaratheodoryMeasurable {d : ℕ} (A : Set (NoteKsk.Space d)) : Prop
def NoteKsk.Chapter05.LebesgueCaratheodoryMeasurable {d : ℕ} (A : Set (NoteKsk.Space d)) : Prop
Definition body
def LebesgueCaratheodoryMeasurable {d : ℕ} (A : Set (Space d)) : Prop := ∀ E : Set (Space d), lambdaStar E = lambdaStar (E ∩ A) + lambdaStar (E \ A)Carathéodory measurability for Lebesgue outer measure.
有限外測度集合のCarathéodory分割.
A\in\calL_d とし，E\subset\RR^d が \lambda^*(E)<\infty を満たすとする．
このとき
\lambda^*(E)
=
\lambda^*(E\cap A)+\lambda^*(E\setminus A)
である．
Lean code for Lemma5.4.2●1 theorem
Associated Lean declarations
-
theoremdefined in NoteKsk/«05lebesgue-measure».leancomplete
theorem NoteKsk.Chapter05.lebesgueMeasurable_caratheodory_finite {d : ℕ} {A E : Set (NoteKsk.Space d)} (hA : NoteKsk.Chapter05.LebesgueMeasurableSet A) (_hEfin : NoteKsk.Chapter03.lambdaStar E < ⊤) : NoteKsk.Chapter03.lambdaStar E = NoteKsk.Chapter03.lambdaStar (E ∩ A) + NoteKsk.Chapter03.lambdaStar (E \ A)
theorem NoteKsk.Chapter05.lebesgueMeasurable_caratheodory_finite {d : ℕ} {A E : Set (NoteKsk.Space d)} (hA : NoteKsk.Chapter05.LebesgueMeasurableSet A) (_hEfin : NoteKsk.Chapter03.lambdaStar E < ⊤) : NoteKsk.Chapter03.lambdaStar E = NoteKsk.Chapter03.lambdaStar (E ∩ A) + NoteKsk.Chapter03.lambdaStar (E \ A)
外測度の劣加法性（Theorem 3.5.2）より
\lambda^*(E)
\le
\lambda^*(E\cap A)+\lambda^*(E\setminus A)
である．逆向きの不等式を示す．
\eps>0 を任意に取る．開集合による外正則性
（Theorem 3.7.1）より，
E\subset G を満たす開集合 G で
\lambda^*(G)<\lambda^*(E)+\eps
となるものが取れる．特に \lambda^*(G)<\infty である．
開集合と閉集合の可測性
（Theorem 5.2.2.4）と
Lebesgue可測集合の集合演算
（Corollary 5.2.2.3）より，
G\cap A と G\setminus A はLebesgue可測である．
有限加法性（Lemma 5.3.4）より
\lambda(G)=\lambda(G\cap A)+\lambda(G\setminus A)
である．したがって，単調性より
\lambda^*(E\cap A)+\lambda^*(E\setminus A)
\le
\lambda(G\cap A)+\lambda(G\setminus A)
=
\lambda(G)
=
\lambda^*(G)
<
\lambda^*(E)+\eps.
\eps>0 は任意であり，逆向きの不等式も従う．
Lebesgue可測ならCarathéodory可測.
A\in\calL_d ならば，A は \lambda^* に関してCarathéodory可測である．
Lean code for Theorem5.4.3●1 theorem
Associated Lean declarations
-
theoremdefined in NoteKsk/«05lebesgue-measure».leancomplete
theorem NoteKsk.Chapter05.lebesgueMeasurable_implies_caratheodory {d : ℕ} {A : Set (NoteKsk.Space d)} (hA : NoteKsk.Chapter05.LebesgueMeasurableSet A) : NoteKsk.Chapter05.LebesgueCaratheodoryMeasurable A
theorem NoteKsk.Chapter05.lebesgueMeasurable_implies_caratheodory {d : ℕ} {A : Set (NoteKsk.Space d)} (hA : NoteKsk.Chapter05.LebesgueMeasurableSet A) : NoteKsk.Chapter05.LebesgueCaratheodoryMeasurable A
任意の E\subset\RR^d を取る．
\lambda^*(E)<\infty の場合は
Lemma 5.4.2 より従う．
\lambda^*(E)=\infty の場合は，外測度の劣加法性
（Theorem 3.5.2）より
\infty=\lambda^*(E)
\le
\lambda^*(E\cap A)+\lambda^*(E\setminus A)
だから右辺も \infty である．逆向きの不等式は自明なので，
Carathéodory条件が成り立つ．
Carathéodory可測ならLebesgue可測.
A\subset\RR^d が \lambda^* に関してCarathéodory可測ならば，
A はLebesgue可測である．
Lean code for Theorem5.4.4●1 theorem
Associated Lean declarations
-
theoremdefined in NoteKsk/«05lebesgue-measure».leancomplete
theorem NoteKsk.Chapter05.caratheodory_implies_lebesgueMeasurable {d : ℕ} {A : Set (NoteKsk.Space d)} (hA : NoteKsk.Chapter05.LebesgueCaratheodoryMeasurable A) : NoteKsk.Chapter05.LebesgueMeasurableSet A
theorem NoteKsk.Chapter05.caratheodory_implies_lebesgueMeasurable {d : ℕ} {A : Set (NoteKsk.Space d)} (hA : NoteKsk.Chapter05.LebesgueCaratheodoryMeasurable A) : NoteKsk.Chapter05.LebesgueMeasurableSet A
R>0 を任意に取り，Q_R=[-R,R]^d とおく．
Carathéodory条件を E=Q_R に適用すると
\lambda^*(Q_R)
=
\lambda^*(A\cap Q_R)+\lambda^*(Q_R\setminus A)
である．区間の外測度は体積
（Proposition 3.4.5）だから \lambda^*(Q_R)=|Q_R| であり，
また，Q_R\setminus A=Q_R\setminus(A\cap Q_R) である．よって
|Q_R|
=
\lambda^*(A\cap Q_R)+\lambda^*(Q_R\setminus (A \cap Q_R))
である．従って区間による外測度の分解 （Corollary 4.5.4）により
\lambda_*(A\cap Q_R)=\lambda^*(A\cap Q_R)
を得る．R>0 は任意なので，A はLebesgue可測である．
Lebesgue可測性とCarathéodory可測性の一致.
集合 A\subset\RR^d について，次は同値である．
-
AはLebesgue可測である -
Aは\lambda^*に関してCarathéodory可測である
Lean code for Corollary5.4.5●1 theorem
Associated Lean declarations
-
theoremdefined in NoteKsk/«05lebesgue-measure».leancomplete
theorem NoteKsk.Chapter05.lebesgueMeasurable_iff_caratheodory {d : ℕ} {A : Set (NoteKsk.Space d)} : NoteKsk.Chapter05.LebesgueMeasurableSet A ↔ NoteKsk.Chapter05.LebesgueCaratheodoryMeasurable A
theorem NoteKsk.Chapter05.lebesgueMeasurable_iff_caratheodory {d : ℕ} {A : Set (NoteKsk.Space d)} : NoteKsk.Chapter05.LebesgueMeasurableSet A ↔ NoteKsk.Chapter05.LebesgueCaratheodoryMeasurable A
thm:lebesgue-measurable-implies-caratheodory,thm:caratheodory-implies-lebesgue-measurable
より従う．