5.2. Lebesgue可測集合の性質
- No associated Lean code or declarations.
\sigma-加法族.
集合 X の部分集合族 \calS\subset\calP(X) が
X 上の \sigma-加法族であるとは,次の3条件を満たすことをいう.
-
X\in\calS -
A\in\calSならばX\setminus A\in\calS -
\{A_n\}_{n=1}^{\infty}\subset\calSならば
\bigcup_{n=1}^{\infty}A_n\in\calS
有限外測度集合の近似判定法.
\lambda^*(A)<\infty とする.このとき次は同値である.
-
AはLebesgue可測である -
任意の
\eps>0に対して,コンパクト集合K\subset Aで
\lambda^*(A\setminus K)<\eps
となるものが取れる
-
任意の
\eps>0に対して,開集合U\supset Aで
\lambda^*(U\setminus A)<\eps
となるものが取れる
Lean code for Lemma5.2.2●2 theorems
Associated Lean declarations
-
theoremdefined in NoteKsk/«05lebesgue-measure».leancomplete
theorem NoteKsk.Chapter05.finiteOuter_compact_approx_criterion {d : ℕ} {A : Set (NoteKsk.Space d)} (hAfin : NoteKsk.Chapter03.lambdaStar A < ⊤) (hA : NoteKsk.Chapter05.LebesgueMeasurableSet A) (ε : ENNReal) : ε ≠ 0 → ∃ K, IsCompact K ∧ K ⊆ A ∧ NoteKsk.Chapter03.lambdaStar (A \ K) < ε
theorem NoteKsk.Chapter05.finiteOuter_compact_approx_criterion {d : ℕ} {A : Set (NoteKsk.Space d)} (hAfin : NoteKsk.Chapter03.lambdaStar A < ⊤) (hA : NoteKsk.Chapter05.LebesgueMeasurableSet A) (ε : ENNReal) : ε ≠ 0 → ∃ K, IsCompact K ∧ K ⊆ A ∧ NoteKsk.Chapter03.lambdaStar (A \ K) < ε
-
theoremdefined in NoteKsk/«05lebesgue-measure».leancomplete
theorem NoteKsk.Chapter05.finiteOuter_open_approx_criterion {d : ℕ} {A : Set (NoteKsk.Space d)} (hAfin : NoteKsk.Chapter03.lambdaStar A < ⊤) (hA : NoteKsk.Chapter05.LebesgueMeasurableSet A) (ε : ENNReal) : ε ≠ 0 → ∃ U, A ⊆ U ∧ IsOpen U ∧ NoteKsk.Chapter03.lambdaStar (U \ A) < ε
theorem NoteKsk.Chapter05.finiteOuter_open_approx_criterion {d : ℕ} {A : Set (NoteKsk.Space d)} (hAfin : NoteKsk.Chapter03.lambdaStar A < ⊤) (hA : NoteKsk.Chapter05.LebesgueMeasurableSet A) (ε : ENNReal) : ε ≠ 0 → ∃ U, A ⊆ U ∧ IsOpen U ∧ NoteKsk.Chapter03.lambdaStar (U \ A) < ε
まず (1) と (2) が同値であることを示す.
A がLebesgue可測であるとする.有限外測度集合の可測性
(Theorem 5.1.2)より
\lambda_*(A)=\lambda^*(A)
である.内測度の定義から,任意の \eps>0 に対して
コンパクト集合 K\subset A で
\lambda^*(K)>\lambda^*(A)-\eps
となるものが取れる.
コンパクト集合による外測度の分解
(Lemma 3.8.4)を B=A と C=K に適用すると
\lambda^*(A)=\lambda^*(K)+\lambda^*(A\setminus K)
である.したがって
\lambda^*(A\setminus K)<\eps
である.
逆に,任意の \eps>0 に対して上のようなコンパクト集合 K\subset A が取れるとする.
コンパクト集合による外測度の分解
(Lemma 3.8.4)より
\lambda^*(A)=\lambda^*(K)+\lambda^*(A\setminus K)
である.また K\subset A はコンパクトだから,内測度の定義より
\lambda^*(K)\le \lambda_*(A)
である.よって
\lambda^*(A)<\lambda_*(A)+\eps
を得る.\eps>0 は任意であり,Lebesgue内測度の基本性質
(Proposition 4.2.1)より \lambda_*(A)\le\lambda^*(A) だから
\lambda_*(A)=\lambda^*(A)
である.有限外測度集合の可測性
(Theorem 5.1.2)より,A はLebesgue可測である.
次に (1) と (3) が同値であることを示す.
まず A がLebesgue可測であるとする.
有限外測度集合の可測性
(Theorem 5.1.2)より
\lambda_*(A)=\lambda^*(A)
である.\eps>0 を任意に取る.
開集合による外正則性
(Theorem 3.7.1)より,
A\subset U を満たす開集合 U で
\lambda^*(U)<\lambda^*(A)+\frac{\eps}{2}
となるものが取れる.また内測度の定義より,
コンパクト集合 K\subset A で
\lambda^*(K)>\lambda^*(A)-\frac{\eps}{2}
となるものが取れる.
K\subset U であり,\lambda^*(U)<\infty だから,
コンパクト集合による外測度の分解
(Lemma 3.8.4)を B=U と C=K に適用すると
\lambda^*(U)=\lambda^*(K)+\lambda^*(U\setminus K)
である.U\setminus A\subset U\setminus K なので
\lambda^*(U\setminus A)
\le
\lambda^*(U\setminus K)
=
\lambda^*(U)-\lambda^*(K)
<
\eps
である.したがって (3) が成り立つ.
逆に (3) を仮定する.\eps>0 を任意に取る.
仮定より,A\subset U を満たす開集合 U で
\lambda^*(U\setminus A)<\frac{\eps}{3}
となるものが取れる.このとき
\lambda^*(U)\le \lambda^*(A)+\lambda^*(U\setminus A)<\infty
である.開集合による外正則性
(Theorem 3.7.1)より,
U\setminus A\subset V を満たす開集合 V で
\lambda^*(V)<\lambda^*(U\setminus A)+\frac{\eps}{3}
<\frac{2\eps}{3}
となるものが取れる.
また,有限外測度の開集合をコンパクト集合で内側から近似できること
(Lemma 3.8.2)より,コンパクト集合 L\subset U で
\lambda^*(L)>\lambda^*(U)-\frac{\eps}{3}
となるものが取れる.
有限外測度の開集合とコンパクト集合の分解
(Lemma 3.8.3)を U と L に適用すると
\lambda^*(U)=\lambda^*(L)+\lambda^*(U\setminus L)
だから
\lambda^*(U\setminus L)<\frac{\eps}{3}
である.
K:=L\setminus V
とおく.L はコンパクトで V は開集合だから,K はコンパクトである.
さらに L\subset U かつ V\supset U\setminus A なので
K\subset U\setminus V\subset A
である.また
U\subset K\cup V\cup(U\setminus L)
だから,外測度の劣加法性 (Theorem 3.5.2)より
\lambda^*(A)
\le
\lambda^*(U)
\le
\lambda^*(K)+\lambda^*(V)+\lambda^*(U\setminus L)
<
\lambda^*(K)+\eps.
したがって
\lambda_*(A)\ge \lambda^*(K)>\lambda^*(A)-\eps
である.\eps>0 は任意なので,
Lebesgue内測度の基本性質
(Proposition 4.2.1)と合わせて
\lambda_*(A)=\lambda^*(A)
を得る.有限外測度集合の可測性
(Theorem 5.1.2)より,A はLebesgue可測である.
5.2.1. 有界閉区間上のLebesgue可測集合
有界な窓の中では,Lebesgue可測性は単に内外測度の一致として扱える.
以下,Q\subset\RR^d を有界閉区間とし,
\calL(Q):=\{A\subset Q\mid \lambda_*(A)=\lambda^*(A)\}
と書く.
有界閉区間内の補集合.
A\in\calL(Q) ならば Q\setminus A\in\calL(Q) である.
Lean code for Lemma5.2.1.1●3 declarations
Associated Lean declarations
-
defdefined in NoteKsk/«05lebesgue-measure».leancomplete
def NoteKsk.Chapter05.LocalLebesgueMeasurable {d : ℕ} (Q A : Set (NoteKsk.Space d)) : Prop
def NoteKsk.Chapter05.LocalLebesgueMeasurable {d : ℕ} (Q A : Set (NoteKsk.Space d)) : Prop
Definition body
def LocalLebesgueMeasurable {d : ℕ} (Q A : Set (Space d)) : Prop := A ⊆ Q ∧ LebesgueMeasurableSet AMeasurability inside a bounded window `Q`, written `𝓛(Q)` in the notes.
-
theoremdefined in NoteKsk/«05lebesgue-measure».leancomplete
theorem NoteKsk.Chapter05.localLebesgueMeasurable_iff {d : ℕ} {Q A : Set (NoteKsk.Space d)} : NoteKsk.Chapter05.LocalLebesgueMeasurable Q A ↔ A ⊆ Q ∧ NoteKsk.Chapter05.LebesgueMeasurableSet A
theorem NoteKsk.Chapter05.localLebesgueMeasurable_iff {d : ℕ} {Q A : Set (NoteKsk.Space d)} : NoteKsk.Chapter05.LocalLebesgueMeasurable Q A ↔ A ⊆ Q ∧ NoteKsk.Chapter05.LebesgueMeasurableSet A
-
theoremdefined in NoteKsk/«05lebesgue-measure».leancomplete
theorem NoteKsk.Chapter05.localLebesgueMeasurable_compl {d : ℕ} (Q : NoteKsk.Box d) {A : Set (NoteKsk.Space d)} (hA : NoteKsk.Chapter05.LocalLebesgueMeasurable Q.Icc A) : NoteKsk.Chapter05.LocalLebesgueMeasurable Q.Icc (Q.Icc \ A)
theorem NoteKsk.Chapter05.localLebesgueMeasurable_compl {d : ℕ} (Q : NoteKsk.Box d) {A : Set (NoteKsk.Space d)} (hA : NoteKsk.Chapter05.LocalLebesgueMeasurable Q.Icc A) : NoteKsk.Chapter05.LocalLebesgueMeasurable Q.Icc (Q.Icc \ A)
A\in\calL(Q) だから
\lambda_*(A)=\lambda^*(A)
である.区間による外測度の分解 (Corollary 4.5.4)より
|Q|=\lambda^*(A)+\lambda^*(Q\setminus A)
である.同じ区間による外測度の分解
(Corollary 4.5.4)を Q\setminus A\subset Q に適用すると,
この等式は
\lambda_*(Q\setminus A)=\lambda^*(Q\setminus A)
と同値である.したがって Q\setminus A\in\calL(Q) である.
有界閉区間内の有限和と有限加法性.
A,B\in\calL(Q) とする.このとき A\cup B\in\calL(Q) である.
さらに A\cap B=\emptyset ならば
\lambda^*(A\cup B)=\lambda^*(A)+\lambda^*(B)
である.
Lean code for Lemma5.2.1.2●2 theorems
Associated Lean declarations
-
theoremdefined in NoteKsk/«05lebesgue-measure».leancomplete
theorem NoteKsk.Chapter05.localLebesgueMeasurable_union {d : ℕ} (Q : NoteKsk.Box d) {A B : Set (NoteKsk.Space d)} (hA : NoteKsk.Chapter05.LocalLebesgueMeasurable Q.Icc A) (hB : NoteKsk.Chapter05.LocalLebesgueMeasurable Q.Icc B) : NoteKsk.Chapter05.LocalLebesgueMeasurable Q.Icc (A ∪ B)
theorem NoteKsk.Chapter05.localLebesgueMeasurable_union {d : ℕ} (Q : NoteKsk.Box d) {A B : Set (NoteKsk.Space d)} (hA : NoteKsk.Chapter05.LocalLebesgueMeasurable Q.Icc A) (hB : NoteKsk.Chapter05.LocalLebesgueMeasurable Q.Icc B) : NoteKsk.Chapter05.LocalLebesgueMeasurable Q.Icc (A ∪ B)
-
theoremdefined in NoteKsk/«05lebesgue-measure».leancomplete
theorem NoteKsk.Chapter05.localLebesgueMeasurable_union_additive {d : ℕ} (_Q : NoteKsk.Box d) {A B : Set (NoteKsk.Space d)} (_hA : NoteKsk.Chapter05.LocalLebesgueMeasurable _Q.Icc A) (hB : NoteKsk.Chapter05.LocalLebesgueMeasurable _Q.Icc B) (hdisj : Disjoint A B) : NoteKsk.Chapter03.lambdaStar (A ∪ B) = NoteKsk.Chapter03.lambdaStar A + NoteKsk.Chapter03.lambdaStar B
theorem NoteKsk.Chapter05.localLebesgueMeasurable_union_additive {d : ℕ} (_Q : NoteKsk.Box d) {A B : Set (NoteKsk.Space d)} (_hA : NoteKsk.Chapter05.LocalLebesgueMeasurable _Q.Icc A) (hB : NoteKsk.Chapter05.LocalLebesgueMeasurable _Q.Icc B) (hdisj : Disjoint A B) : NoteKsk.Chapter03.lambdaStar (A ∪ B) = NoteKsk.Chapter03.lambdaStar A + NoteKsk.Chapter03.lambdaStar B
まず有限和に関する閉性を示す.
A,B\subset Q なので,\lambda^*(A),\lambda^*(B)<\infty である.
A,B\in\calL(Q) と有限外測度集合の可測性
(Theorem 5.1.2)より,
A,B はLebesgue可測である.
有限外測度集合の近似判定法
(Lemma 5.2.2)より,任意の \eps>0 に対して
コンパクト集合 K_A\subset A,\ K_B\subset B で
\lambda^*(A\setminus K_A)<\frac{\eps}{2},
\qquad
\lambda^*(B\setminus K_B)<\frac{\eps}{2}
となるものが取れる. このとき
K:=K_A\cup K_B
は A\cup B に含まれるコンパクト集合であり,
(A\cup B)\setminus K
\subset
(A\setminus K_A)\cup(B\setminus K_B)
である.Lebesgue外測度の性質 (Theorem 3.5.2)より
\lambda^*((A\cup B)\setminus K)<\eps
である.したがって有限外測度集合の近似判定法
(Lemma 5.2.2)より A\cup B はLebesgue可測である.
また A\cup B\subset Q だから,有限外測度集合の可測性
(Theorem 5.1.2)より
\lambda_*(A\cup B)=\lambda^*(A\cup B)
である.よって A\cup B\in\calL(Q) である.
次に A\cap B=\emptyset とする.
外測度の劣加法性(Theorem 3.5.2)より
\lambda^*(A\cup B)\le \lambda^*(A)+\lambda^*(B)
である.逆向きの不等式を示す.\eps>0 を任意に取る.
A,B\in\calL(Q) だから,内測度の定義よりコンパクト集合
K_A\subset A,\ K_B\subset B で
\lambda^*(K_A)>\lambda^*(A)-\frac{\eps}{2},
\qquad
\lambda^*(K_B)>\lambda^*(B)-\frac{\eps}{2}
となるものが取れる.
A\cap B=\emptyset なので K_A と K_B は交わらない.
空でない場合には2つのコンパクト集合は正の距離だけ離れているから,
正距離集合に対する外測度の加法性
(Lemma 3.8.1)より
\lambda^*(K_A\cup K_B)
=
\lambda^*(K_A)+\lambda^*(K_B)
である.片方が空の場合もこの等式は自明である. したがって
\lambda^*(A\cup B)
\ge
\lambda^*(K_A\cup K_B)
>
\lambda^*(A)+\lambda^*(B)-\eps
である.\eps>0 は任意だから
\lambda^*(A\cup B)\ge \lambda^*(A)+\lambda^*(B)
を得る.
有界閉区間内の集合演算.
A,B\in\calL(Q) ならば
A\cap B,\qquad A\setminus B
も \calL(Q) に属する.
Lean code for Corollary5.2.1.3●2 theorems
Associated Lean declarations
-
theoremdefined in NoteKsk/«05lebesgue-measure».leancomplete
theorem NoteKsk.Chapter05.localLebesgueMeasurable_inter {d : ℕ} (Q : NoteKsk.Box d) {A B : Set (NoteKsk.Space d)} (hA : NoteKsk.Chapter05.LocalLebesgueMeasurable Q.Icc A) (hB : NoteKsk.Chapter05.LocalLebesgueMeasurable Q.Icc B) : NoteKsk.Chapter05.LocalLebesgueMeasurable Q.Icc (A ∩ B)
theorem NoteKsk.Chapter05.localLebesgueMeasurable_inter {d : ℕ} (Q : NoteKsk.Box d) {A B : Set (NoteKsk.Space d)} (hA : NoteKsk.Chapter05.LocalLebesgueMeasurable Q.Icc A) (hB : NoteKsk.Chapter05.LocalLebesgueMeasurable Q.Icc B) : NoteKsk.Chapter05.LocalLebesgueMeasurable Q.Icc (A ∩ B)
-
theoremdefined in NoteKsk/«05lebesgue-measure».leancomplete
theorem NoteKsk.Chapter05.localLebesgueMeasurable_diff {d : ℕ} (Q : NoteKsk.Box d) {A B : Set (NoteKsk.Space d)} (hA : NoteKsk.Chapter05.LocalLebesgueMeasurable Q.Icc A) (hB : NoteKsk.Chapter05.LocalLebesgueMeasurable Q.Icc B) : NoteKsk.Chapter05.LocalLebesgueMeasurable Q.Icc (A \ B)
theorem NoteKsk.Chapter05.localLebesgueMeasurable_diff {d : ℕ} (Q : NoteKsk.Box d) {A B : Set (NoteKsk.Space d)} (hA : NoteKsk.Chapter05.LocalLebesgueMeasurable Q.Icc A) (hB : NoteKsk.Chapter05.LocalLebesgueMeasurable Q.Icc B) : NoteKsk.Chapter05.LocalLebesgueMeasurable Q.Icc (A \ B)
有界閉区間内の補集合
(Lemma 5.2.1.1)より Q\setminus A,Q\setminus B\in\calL(Q) である.
有界閉区間内の有限和に関する閉性
(Lemma 5.2.1.2)より
(Q\setminus A)\cup(Q\setminus B)\in\calL(Q),
\qquad
(Q\setminus A)\cup B\in\calL(Q)
である.もう一度補集合に関する閉性を用いると
A\cap B
=
Q\setminus\bigl((Q\setminus A)\cup(Q\setminus B)\bigr)\in\calL(Q)
および
A\setminus B
=
Q\setminus\bigl((Q\setminus A)\cup B\bigr)\in\calL(Q)
を得る.
有界閉区間内の \sigma-加法性.
\calL(Q) は Q 上の \sigma-加法族である.
さらに,互いに素な列 \{A_n\}_{n=1}^{\infty}\subset\calL(Q) に対して
\lambda^*\left(\bigsqcup_{n=1}^{\infty}A_n\right)
=
\sum_{n=1}^{\infty}\lambda^*(A_n)
が成り立つ.
Lean code for Theorem5.2.1.4●2 theorems
Associated Lean declarations
-
theoremdefined in NoteKsk/«05lebesgue-measure».leancomplete
theorem NoteKsk.Chapter05.localLebesgueMeasurable_iUnion {d : ℕ} (Q : NoteKsk.Box d) (A : ℕ → Set (NoteKsk.Space d)) (hA : ∀ (n : ℕ), NoteKsk.Chapter05.LocalLebesgueMeasurable Q.Icc (A n)) : NoteKsk.Chapter05.LocalLebesgueMeasurable Q.Icc (⋃ n, A n)
theorem NoteKsk.Chapter05.localLebesgueMeasurable_iUnion {d : ℕ} (Q : NoteKsk.Box d) (A : ℕ → Set (NoteKsk.Space d)) (hA : ∀ (n : ℕ), NoteKsk.Chapter05.LocalLebesgueMeasurable Q.Icc (A n)) : NoteKsk.Chapter05.LocalLebesgueMeasurable Q.Icc (⋃ n, A n)
-
theoremdefined in NoteKsk/«05lebesgue-measure».leancomplete
theorem NoteKsk.Chapter05.localLebesgueMeasurable_iUnion_additive {d : ℕ} (_Q : NoteKsk.Box d) (A : ℕ → Set (NoteKsk.Space d)) (hA : ∀ (n : ℕ), NoteKsk.Chapter05.LocalLebesgueMeasurable _Q.Icc (A n)) (hdisj : ∀ ⦃m n : ℕ⦄, m ≠ n → Disjoint (A m) (A n)) : NoteKsk.Chapter03.lambdaStar (⋃ n, A n) = ∑' (n : ℕ), NoteKsk.Chapter03.lambdaStar (A n)
theorem NoteKsk.Chapter05.localLebesgueMeasurable_iUnion_additive {d : ℕ} (_Q : NoteKsk.Box d) (A : ℕ → Set (NoteKsk.Space d)) (hA : ∀ (n : ℕ), NoteKsk.Chapter05.LocalLebesgueMeasurable _Q.Icc (A n)) (hdisj : ∀ ⦃m n : ℕ⦄, m ≠ n → Disjoint (A m) (A n)) : NoteKsk.Chapter03.lambdaStar (⋃ n, A n) = ∑' (n : ℕ), NoteKsk.Chapter03.lambdaStar (A n)
まず Q\in\calL(Q) を確認する.
Q はコンパクト集合なので,コンパクト集合では内外が一致する
(Proposition 4.2.2)より
\lambda_*(Q)=\lambda^*(Q)
である.また有界閉区間内の補集合
(Lemma 5.2.1.1)より \emptyset=Q\setminus Q\in\calL(Q) である.
補集合に関する閉性は有界閉区間内の補集合 (Lemma 5.2.1.1)で示した. したがって,あとは可算和に関する閉性を示せばよい.
まず \{A_n\}_{n=1}^{\infty}\subset\calL(Q) が互いに素である場合を考える.
A:=\bigcup_{n=1}^{\infty}A_n,
\qquad
S_N:=\bigcup_{n=1}^{N}A_n
とおく.有界閉区間内の有限和に関する閉性と有限加法性 (Lemma 5.2.1.2)を繰り返し用いると
S_N\in\calL(Q),
\qquad
\lambda^*(S_N)=\sum_{n=1}^{N}\lambda^*(A_n)
である.単調性より
\sum_{n=1}^{N}\lambda^*(A_n)=\lambda^*(S_N)\le\lambda^*(A)
であるから,N\to\infty として
\sum_{n=1}^{\infty}\lambda^*(A_n)\le\lambda^*(A)
を得る.逆向きの不等式は外測度の可算劣加法性 (Theorem 3.5.2)から従う.よって
\lambda^*(A)=\sum_{n=1}^{\infty}\lambda^*(A_n)
である.
A\subset Q なので \lambda^*(A)<\infty である.
任意の \eps>0 を取る.上の等式より,ある N が存在して
\lambda^*(S_N)>\lambda^*(A)-\frac{\eps}{2}
である.S_N\in\calL(Q) かつ S_N\subset Q だから,有限外測度集合の可測性
(Theorem 5.1.2)より S_N はLebesgue可測である.
したがって有限外測度集合の近似判定法
(Lemma 5.2.2)より,
コンパクト集合 K\subset S_N で
\lambda^*(S_N\setminus K)<\frac{\eps}{2}
となるものが取れる.コンパクト集合による外測度の分解 (Lemma 3.8.4)より
\lambda^*(S_N)=\lambda^*(K)+\lambda^*(S_N\setminus K)
だから
\lambda^*(K)>\lambda^*(S_N)-\frac{\eps}{2}
>\lambda^*(A)-\eps
である.
したがって有限外測度集合の近似判定法
(Lemma 5.2.2)より A はLebesgue可測である.
さらに A\subset Q なので,有限外測度集合の可測性
(Theorem 5.1.2)より A\in\calL(Q) である.
互いに素な場合の可算和に関する閉性と加法性が示された.
一般の列 \{A_n\}_{n=1}^{\infty}\subset\calL(Q) に対しては
B_1:=A_1,\qquad
B_n:=A_n\setminus\bigcup_{j=1}^{n-1}A_j
\quad(n\ge2)
とおく.有界閉区間内の有限和に関する閉性
(Lemma 5.2.1.2)と
有界閉区間内の集合演算
(Corollary 5.2.1.3)より,すべての n について
B_n\in\calL(Q) である.また \{B_n\} は互いに素であり,
\bigcup_{n=1}^{\infty}B_n=\bigcup_{n=1}^{\infty}A_n
である.したがって上で示した互いに素な場合を適用すれば,
\bigcup_{n=1}^{\infty}A_n\in\calL(Q)
を得る.
5.2.2. 全空間上のLebesgue可測集合
次の性質を使用して,Lebesgue可測集合族の \sigma-加法性を示す.
A\subset\RR^d がLebesgue可測であること(A \in \calL_d)は,任意の R>0 に対して A\cap Q_R\in\calL(Q_R) であることと同値である.
Lean code for Proposition5.2.2.1●1 theorem
Associated Lean declarations
-
theoremdefined in NoteKsk/«05lebesgue-measure».leancomplete
theorem NoteKsk.Chapter05.lebesgueMeasurableSet_windows {d : ℕ} {A : Set (NoteKsk.Space d)} (hA : NoteKsk.Chapter05.LebesgueMeasurableSet A) (R : ℝ) : 0 < R → NoteKsk.Chapter04.lambdaInner (A ∩ NoteKsk.closedCube d R) = NoteKsk.Chapter03.lambdaStar (A ∩ NoteKsk.closedCube d R)
theorem NoteKsk.Chapter05.lebesgueMeasurableSet_windows {d : ℕ} {A : Set (NoteKsk.Space d)} (hA : NoteKsk.Chapter05.LebesgueMeasurableSet A) (R : ℝ) : 0 < R → NoteKsk.Chapter04.lambdaInner (A ∩ NoteKsk.closedCube d R) = NoteKsk.Chapter03.lambdaStar (A ∩ NoteKsk.closedCube d R)
Window form used in the lecture notes: every bounded cube sees equality of inner and outer measure.
証明は定義の言い換えから直ちに従う.
Lebesgue可測集合族の \sigma-加法性.
Lebesgue可測集合全体 \calL_d は \RR^d 上の \sigma-加法族である.
Lean code for Theorem5.2.2.2●4 theorems
Associated Lean declarations
-
theoremdefined in NoteKsk/«05lebesgue-measure».leancomplete
theorem NoteKsk.Chapter05.lebesgueMeasurableSet_univ {d : ℕ} : NoteKsk.Chapter05.LebesgueMeasurableSet Set.univ
theorem NoteKsk.Chapter05.lebesgueMeasurableSet_univ {d : ℕ} : NoteKsk.Chapter05.LebesgueMeasurableSet Set.univ
-
theoremdefined in NoteKsk/«05lebesgue-measure».leancomplete
theorem NoteKsk.Chapter05.lebesgueMeasurableSet_empty {d : ℕ} : NoteKsk.Chapter05.LebesgueMeasurableSet ∅
theorem NoteKsk.Chapter05.lebesgueMeasurableSet_empty {d : ℕ} : NoteKsk.Chapter05.LebesgueMeasurableSet ∅
-
theoremdefined in NoteKsk/«05lebesgue-measure».leancomplete
theorem NoteKsk.Chapter05.lebesgueMeasurableSet_compl {d : ℕ} {A : Set (NoteKsk.Space d)} (hA : NoteKsk.Chapter05.LebesgueMeasurableSet A) : NoteKsk.Chapter05.LebesgueMeasurableSet Aᶜ
theorem NoteKsk.Chapter05.lebesgueMeasurableSet_compl {d : ℕ} {A : Set (NoteKsk.Space d)} (hA : NoteKsk.Chapter05.LebesgueMeasurableSet A) : NoteKsk.Chapter05.LebesgueMeasurableSet Aᶜ
-
theoremdefined in NoteKsk/«05lebesgue-measure».leancomplete
theorem NoteKsk.Chapter05.lebesgueMeasurableSet_iUnion {d : ℕ} (A : ℕ → Set (NoteKsk.Space d)) (hA : ∀ (n : ℕ), NoteKsk.Chapter05.LebesgueMeasurableSet (A n)) : NoteKsk.Chapter05.LebesgueMeasurableSet (⋃ n, A n)
theorem NoteKsk.Chapter05.lebesgueMeasurableSet_iUnion {d : ℕ} (A : ℕ → Set (NoteKsk.Space d)) (hA : ∀ (n : ℕ), NoteKsk.Chapter05.LebesgueMeasurableSet (A n)) : NoteKsk.Chapter05.LebesgueMeasurableSet (⋃ n, A n)
まず \RR^d\in\calL_d である.実際,任意の R>0 に対して
\RR^d\cap Q_R=Q_R \in \calL(Q_R)
なので,Proposition 5.2.2.1 より \RR^d \in \calL_d である.
また同様に \emptyset\in\calL_d である.
次に A\in\calL_d とする.任意の R>0 に対して,
A\cap Q_R\in\calL(Q_R) である.有界閉区間内の \sigma-加法性
(Theorem 5.2.1.4)より
Q_R\setminus(A\cap Q_R)\in\calL(Q_R)
である.これは
(\RR^d\setminus A)\cap Q_R
=
Q_R\setminus(A\cap Q_R)
に等しい.したがって任意の R>0 で (\RR^d \setminus A) \cap Q_R \in \calL(Q_R) である.
よって \RR^d\setminus A\in\calL_d である.
最後に \{A_n\}_{n=1}^{\infty}\subset\calL_d とする.
任意の R>0 に対して,各 A_n\cap Q_R は \calL(Q_R) に属する.
有界閉区間内の \sigma-加法性
(Theorem 5.2.1.4)より
\bigcup_{n=1}^{\infty}(A_n\cap Q_R)\in\calL(Q_R)
である.ところが
\left(\bigcup_{n=1}^{\infty}A_n\right)\cap Q_R
=
\bigcup_{n=1}^{\infty}(A_n\cap Q_R)
である.したがって任意の R>0 で \left(\bigcup_{n=1}^{\infty}A_n\right)\cap Q_R \in \calL(Q_R) である.よって
\bigcup_{n=1}^{\infty}A_n\in\calL_d
である.
集合演算.
A,B\in\calL_d ならば
A\cup B,\qquad A\cap B,\qquad A\setminus B
も \calL_d に属する.また \{A_n\}_{n=1}^{\infty}\subset\calL_d ならば
\bigcap_{n=1}^{\infty}A_n\in\calL_d
である.
Lean code for Corollary5.2.2.3●4 theorems
Associated Lean declarations
-
theoremdefined in NoteKsk/«05lebesgue-measure».leancomplete
theorem NoteKsk.Chapter05.lebesgueMeasurableSet_union {d : ℕ} {A B : Set (NoteKsk.Space d)} (hA : NoteKsk.Chapter05.LebesgueMeasurableSet A) (hB : NoteKsk.Chapter05.LebesgueMeasurableSet B) : NoteKsk.Chapter05.LebesgueMeasurableSet (A ∪ B)
theorem NoteKsk.Chapter05.lebesgueMeasurableSet_union {d : ℕ} {A B : Set (NoteKsk.Space d)} (hA : NoteKsk.Chapter05.LebesgueMeasurableSet A) (hB : NoteKsk.Chapter05.LebesgueMeasurableSet B) : NoteKsk.Chapter05.LebesgueMeasurableSet (A ∪ B)
-
theoremdefined in NoteKsk/«05lebesgue-measure».leancomplete
theorem NoteKsk.Chapter05.lebesgueMeasurableSet_inter {d : ℕ} {A B : Set (NoteKsk.Space d)} (hA : NoteKsk.Chapter05.LebesgueMeasurableSet A) (hB : NoteKsk.Chapter05.LebesgueMeasurableSet B) : NoteKsk.Chapter05.LebesgueMeasurableSet (A ∩ B)
theorem NoteKsk.Chapter05.lebesgueMeasurableSet_inter {d : ℕ} {A B : Set (NoteKsk.Space d)} (hA : NoteKsk.Chapter05.LebesgueMeasurableSet A) (hB : NoteKsk.Chapter05.LebesgueMeasurableSet B) : NoteKsk.Chapter05.LebesgueMeasurableSet (A ∩ B)
-
theoremdefined in NoteKsk/«05lebesgue-measure».leancomplete
theorem NoteKsk.Chapter05.lebesgueMeasurableSet_diff {d : ℕ} {A B : Set (NoteKsk.Space d)} (hA : NoteKsk.Chapter05.LebesgueMeasurableSet A) (hB : NoteKsk.Chapter05.LebesgueMeasurableSet B) : NoteKsk.Chapter05.LebesgueMeasurableSet (A \ B)
theorem NoteKsk.Chapter05.lebesgueMeasurableSet_diff {d : ℕ} {A B : Set (NoteKsk.Space d)} (hA : NoteKsk.Chapter05.LebesgueMeasurableSet A) (hB : NoteKsk.Chapter05.LebesgueMeasurableSet B) : NoteKsk.Chapter05.LebesgueMeasurableSet (A \ B)
-
theoremdefined in NoteKsk/«05lebesgue-measure».leancomplete
theorem NoteKsk.Chapter05.lebesgueMeasurableSet_iInter {d : ℕ} (A : ℕ → Set (NoteKsk.Space d)) (hA : ∀ (n : ℕ), NoteKsk.Chapter05.LebesgueMeasurableSet (A n)) : NoteKsk.Chapter05.LebesgueMeasurableSet (⋂ n, A n)
theorem NoteKsk.Chapter05.lebesgueMeasurableSet_iInter {d : ℕ} (A : ℕ → Set (NoteKsk.Space d)) (hA : ∀ (n : ℕ), NoteKsk.Chapter05.LebesgueMeasurableSet (A n)) : NoteKsk.Chapter05.LebesgueMeasurableSet (⋂ n, A n)
Lebesgue可測集合族の \sigma-加法性
(Theorem 5.2.2.2)から,補集合と可算和に関する閉性が従う.
あとはDe Morganの法則と
A\setminus B=A\cap(\RR^d\setminus B)
を用いればよい.
開集合と閉集合.
\RR^d の開集合と閉集合はLebesgue可測である.
Lean code for Theorem5.2.2.4●2 theorems
Associated Lean declarations
-
theoremdefined in NoteKsk/«05lebesgue-measure».leancomplete
theorem NoteKsk.Chapter05.isClosed_lebesgueMeasurable {d : ℕ} {F : Set (NoteKsk.Space d)} (hF : IsClosed F) : NoteKsk.Chapter05.LebesgueMeasurableSet F
theorem NoteKsk.Chapter05.isClosed_lebesgueMeasurable {d : ℕ} {F : Set (NoteKsk.Space d)} (hF : IsClosed F) : NoteKsk.Chapter05.LebesgueMeasurableSet F
-
theoremdefined in NoteKsk/«05lebesgue-measure».leancomplete
theorem NoteKsk.Chapter05.isOpen_lebesgueMeasurable {d : ℕ} {G : Set (NoteKsk.Space d)} (hG : IsOpen G) : NoteKsk.Chapter05.LebesgueMeasurableSet G
theorem NoteKsk.Chapter05.isOpen_lebesgueMeasurable {d : ℕ} {G : Set (NoteKsk.Space d)} (hG : IsOpen G) : NoteKsk.Chapter05.LebesgueMeasurableSet G
まず閉集合 F\subset\RR^d を取る.任意の R>0 に対して
F\cap Q_R
はコンパクト集合である.コンパクト集合では内外が一致する (Proposition 4.2.2)より
\lambda_*(F\cap Q_R)=\lambda^*(F\cap Q_R)
である.したがって F はLebesgue可測である.
開集合 G については,\RR^d\setminus G が閉集合なのでLebesgue可測である.
Lebesgue可測集合族の \sigma-加法性
(Theorem 5.2.2.2)より,その補集合である G もLebesgue可測である.