Lebesgue積分講義ノート

5.2. Lebesgue可測集合の性質🔗

Definition5.2.1
uses 0used by 0XL∃∀N

\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

Lemma5.2.2
Statement uses 2
Statement dependency previews
Preview
Theorem 3.7.1
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
used by 1L∃∀N

有限外測度集合の近似判定法. \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.22 theorems
  • theoremdefined in NoteKsk/«05lebesgue-measure».lean
    complete
    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».lean
    complete
    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) <
                ε
Proof for Lemma 5.2.2
uses 0

まず (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=AC=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=UC=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)を UL に適用すると

\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)\}

と書く.

Lemma5.2.1.1
uses 1
Used by 2
Reverse dependency previews
Preview
Lemma 5.2.1.2
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
L∃∀N

有界閉区間内の補集合. A\in\calL(Q) ならば Q\setminus A\in\calL(Q) である.

Lean code for Lemma5.2.1.13 declarations
  • defdefined in NoteKsk/«05lebesgue-measure».lean
    complete
    def NoteKsk.Chapter05.LocalLebesgueMeasurable {d : }
      (Q A : Set (NoteKsk.Space d)) : Prop
    def NoteKsk.Chapter05.LocalLebesgueMeasurable
      {d : } (Q A : Set (NoteKsk.Space d)) :
      Prop
    def LocalLebesgueMeasurable {d : ℕ} (Q A : Set (Space d)) : Prop :=
      A ⊆ Q ∧ LebesgueMeasurableSet A
    Measurability inside a bounded window `Q`, written `𝓛(Q)` in the notes. 
  • theoremdefined in NoteKsk/«05lebesgue-measure».lean
    complete
    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».lean
    complete
    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)
Proof for Lemma 5.2.1.1
uses 0

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) である.

Lemma5.2.1.2
Statement uses 2
Statement dependency previews
Preview
Lemma 5.2.2
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
Used by 3
Reverse dependency previews
L∃∀N

有界閉区間内の有限和と有限加法性. 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.22 theorems
  • theoremdefined in NoteKsk/«05lebesgue-measure».lean
    complete
    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».lean
    complete
    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
Proof for Lemma 5.2.1.2
uses 0

まず有限和に関する閉性を示す. 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_AK_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)

を得る.

Corollary5.2.1.3
Statement uses 2
Statement dependency previews
Preview
Lemma 5.2.1.1
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
used by 1L∃∀N

有界閉区間内の集合演算. A,B\in\calL(Q) ならば

A\cap B,\qquad A\setminus B

\calL(Q) に属する.

Lean code for Corollary5.2.1.32 theorems
  • theoremdefined in NoteKsk/«05lebesgue-measure».lean
    complete
    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».lean
    complete
    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)
Proof for Corollary 5.2.1.3
uses 0

有界閉区間内の補集合 (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)

を得る.

Theorem5.2.1.4
Statement uses 2
Statement dependency previews
Preview
Lemma 5.2.1.2
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
Used by 3
Reverse dependency previews
L∃∀N

有界閉区間内の \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.42 theorems
  • theoremdefined in NoteKsk/«05lebesgue-measure».lean
    complete
    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».lean
    complete
    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)
Proof for Theorem 5.2.1.4
uses 0

まず 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-加法性を示す.

Proposition5.2.2.1
uses 1used by 1L∃∀N

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.11 theorem
  • theoremdefined in NoteKsk/«05lebesgue-measure».lean
    complete
    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.
    

証明は定義の言い換えから直ちに従う.

Theorem5.2.2.2
Statement uses 2
Statement dependency previews
Preview
Theorem 5.2.1.4
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
L∃∀N

Lebesgue可測集合族の \sigma-加法性. Lebesgue可測集合全体 \calL_d\RR^d 上の \sigma-加法族である.

Lean code for Theorem5.2.2.24 theorems
  • theoremdefined in NoteKsk/«05lebesgue-measure».lean
    complete
    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».lean
    complete
    theorem NoteKsk.Chapter05.lebesgueMeasurableSet_empty {d : } :
      NoteKsk.Chapter05.LebesgueMeasurableSet 
    theorem NoteKsk.Chapter05.lebesgueMeasurableSet_empty
      {d : } :
      NoteKsk.Chapter05.LebesgueMeasurableSet
        
  • theoremdefined in NoteKsk/«05lebesgue-measure».lean
    complete
    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».lean
    complete
    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)
Proof for Theorem 5.2.2.2
uses 0

まず \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

である.

Corollary5.2.2.3
uses 1
Used by 2
Reverse dependency previews
Preview
Theorem 5.3.7
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
L∃∀N

集合演算. 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.34 theorems
  • theoremdefined in NoteKsk/«05lebesgue-measure».lean
    complete
    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».lean
    complete
    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».lean
    complete
    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».lean
    complete
    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)
Proof for Corollary 5.2.2.3
uses 0

Lebesgue可測集合族の \sigma-加法性 (Theorem 5.2.2.2)から,補集合と可算和に関する閉性が従う. あとはDe Morganの法則と

A\setminus B=A\cap(\RR^d\setminus B)

を用いればよい.

Theorem5.2.2.4
Statement uses 2
Statement dependency previews
Preview
Proposition 4.2.2
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
Used by 3
Reverse dependency previews
L∃∀N

開集合と閉集合. \RR^d の開集合と閉集合はLebesgue可測である.

Lean code for Theorem5.2.2.42 theorems
  • theoremdefined in NoteKsk/«05lebesgue-measure».lean
    complete
    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».lean
    complete
    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
Proof for Theorem 5.2.2.4
uses 0

まず閉集合 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可測である.