Lebesgue積分講義ノート

6.5. 誘導外測度と拡張定理🔗

Definition6.5.1
Statement uses 2
Statement dependency previews
Preview
Definition 6.3.1
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
used by 1✓L∃∀N
Tagsleanok

誘導外測度. 有限加法族 \calA 上の前測度 \mu_0 から，任意の B\subset X に対して

\mu^*(B) := \inf\left\{ \sum_{n=1}^{\infty}\mu_0(A_n) \;\middle|\; B\subset\bigcup_{n=1}^{\infty}A_n,\ A_n\in\calA\ (n=1,2,\ldots) \right\}

と定める． つまり，下限は B を覆う \calA の可算列すべてにわたって取る． そのような被覆が存在しないときは，この下限を \infty と約束する．

Lean code for Definition6.5.1●1 definition
  • defdefined in NoteKsk/«06caratheodory».lean
    complete
    def NoteKsk.Chapter06.inducedOuterMeasureFromPremeasure.{u_1} {α : Type u_1}
  {C : Set (Set α)} (hC : MeasureTheory.IsSetSemiring C)
  (m : MeasureTheory.AddContent ENNReal C) :
  MeasureTheory.OuterMeasure α
    def NoteKsk.Chapter06.inducedOuterMeasureFromPremeasure.{u_1}
  {α : Type u_1} {C : Set (Set α)}
  (hC : MeasureTheory.IsSetSemiring C)
  (m :
    MeasureTheory.AddContent ENNReal C) :
  MeasureTheory.OuterMeasure α

    Definition body

    noncomputable def inducedOuterMeasureFromPremeasure
    (hC : IsSetSemiring C) (m : AddContent ENNReal C) : OuterMeasure α :=
  inducedOuterMeasure (fun s (_hs : s ∈ C) => m s) hC.empty_mem (by simp)
    The outer measure induced by a semiring premeasure via countable covers.

Remark (半加法族から直接作る流儀). 半加法族 \calE 上の前測度 \mu_0 から直接

\mu^*_{\calE}(B) := \inf\left\{ \sum_{n=1}^{\infty}\mu_0(E_n) \;\middle|\; B\subset\bigcup_{n=1}^{\infty}E_n,\ E_n\in\calE\ (n=1,2,\ldots) \right\}

と定める流儀もある． 一方，本章ではまず \mu_0 を有限加法族 \calA(\calE) 上の前測度 \overline\mu_0 に延長し，その後で可算被覆による誘導外測度を作る． 両者は同じ外測度を与える． 実際，\calE\subset\calA(\calE) なので \calE による被覆は \calA(\calE) による被覆でもある． 逆に，\calA(\calE) の各元は有限個の互いに素な \calE の元の合併として書け， そのとき \overline\mu_0 は各項の \mu_0 の和であるから， \calA(\calE) による可算被覆は同じ総和をもつ \calE による可算被覆に細分できる． したがって，下限は一致する．

Theorem6.5.2
Statement uses 3
Statement dependency previews
Preview
Definition 6.3.2
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
used by 1✓L∃∀N
Tagsleanok

誘導外測度. Definition 6.5.1で定めた \mu^* について， 次が成り立つ．

  • \mu^* は X 上の外測度である．

  • 任意の A\in\calA に対して \mu^*(A)=\mu_0(A) である．

  • 任意の A\in\calA は \mu^*-可測である．

Lean code for Theorem6.5.2●4 declarations
  • defdefined in NoteKsk/«06caratheodory».lean
    complete
    def NoteKsk.Chapter06.inducedOuterMeasureFromPremeasure.{u_1} {α : Type u_1}
  {C : Set (Set α)} (hC : MeasureTheory.IsSetSemiring C)
  (m : MeasureTheory.AddContent ENNReal C) :
  MeasureTheory.OuterMeasure α
    def NoteKsk.Chapter06.inducedOuterMeasureFromPremeasure.{u_1}
  {α : Type u_1} {C : Set (Set α)}
  (hC : MeasureTheory.IsSetSemiring C)
  (m :
    MeasureTheory.AddContent ENNReal C) :
  MeasureTheory.OuterMeasure α

    Definition body

    noncomputable def inducedOuterMeasureFromPremeasure
    (hC : IsSetSemiring C) (m : AddContent ENNReal C) : OuterMeasure α :=
  inducedOuterMeasure (fun s (_hs : s ∈ C) => m s) hC.empty_mem (by simp)
    The outer measure induced by a semiring premeasure via countable covers.
  • theoremdefined in NoteKsk/«06caratheodory».lean
    complete
    theorem NoteKsk.Chapter06.inducedOuterMeasureFromPremeasure_eq_on_semiring.{u_1}
  {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.IsSetSemiring C)
  (m : MeasureTheory.AddContent ENNReal C)
  (hm : NoteKsk.IsPremeasureOnSemiring m) {s : Set α} (hs : s ∈ C) :
  (NoteKsk.Chapter06.inducedOuterMeasureFromPremeasure hC m) s = m s
    theorem NoteKsk.Chapter06.inducedOuterMeasureFromPremeasure_eq_on_semiring.{u_1}
  {α : Type u_1} {C : Set (Set α)}
  (hC : MeasureTheory.IsSetSemiring C)
  (m : MeasureTheory.AddContent ENNReal C)
  (hm : NoteKsk.IsPremeasureOnSemiring m)
  {s : Set α} (hs : s ∈ C) :
  (NoteKsk.Chapter06.inducedOuterMeasureFromPremeasure
        hC m)
      s =
    m s
  • theoremdefined in NoteKsk/«06caratheodory».lean
    complete
    theorem NoteKsk.Chapter06.inducedOuterMeasureFromPremeasure_caratheodory_of_mem.{u_1}
  {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.IsSetSemiring C)
  (m : MeasureTheory.AddContent ENNReal C) {s : Set α} (hs : s ∈ C) :
  NoteKsk.CaratheodoryMeasurableSet
    (NoteKsk.Chapter06.inducedOuterMeasureFromPremeasure hC m) s
    theorem NoteKsk.Chapter06.inducedOuterMeasureFromPremeasure_caratheodory_of_mem.{u_1}
  {α : Type u_1} {C : Set (Set α)}
  (hC : MeasureTheory.IsSetSemiring C)
  (m : MeasureTheory.AddContent ENNReal C)
  {s : Set α} (hs : s ∈ C) :
  NoteKsk.CaratheodoryMeasurableSet
    (NoteKsk.Chapter06.inducedOuterMeasureFromPremeasure
      hC m)
    s
  • theoremdefined in NoteKsk/«06caratheodory».lean
    complete
    theorem NoteKsk.Chapter06.inducedOuterMeasureFromPremeasure_caratheodory_generated.{u_1}
  {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.IsSetSemiring C)
  (m : MeasureTheory.AddContent ENNReal C) {s : Set α}
  (hs : MeasurableSet s) :
  NoteKsk.CaratheodoryMeasurableSet
    (NoteKsk.Chapter06.inducedOuterMeasureFromPremeasure hC m) s
    theorem NoteKsk.Chapter06.inducedOuterMeasureFromPremeasure_caratheodory_generated.{u_1}
  {α : Type u_1} {C : Set (Set α)}
  (hC : MeasureTheory.IsSetSemiring C)
  (m : MeasureTheory.AddContent ENNReal C)
  {s : Set α} (hs : MeasurableSet s) :
  NoteKsk.CaratheodoryMeasurableSet
    (NoteKsk.Chapter06.inducedOuterMeasureFromPremeasure
      hC m)
    s
Proof for Theorem 6.5.2
uses 0

\mu^*(\emptyset)=0 は空集合による被覆から従い，単調性は被覆の範囲が広がるだけである． 可算劣加法性を示す． \sum_n\mu^*(E_n)=\infty なら自明なので，右辺は有限とする． \eps>0 を任意に取る． 各 n について，\mu^*(E_n) は下限であり最小値とは限らないので，

E_n\subset\bigcup_{k=1}^{\infty}A_{n,k}, \qquad \sum_{k=1}^{\infty}\mu_0(A_{n,k}) < \mu^*(E_n)+\eps 2^{-n}

となる A_{n,k}\in\calA を取る． この \eps は，最後に任意に小さくする全体の誤差を各 n に配分するためのものである． これらを全部並べると \bigcup_n E_n の \calA-被覆になるから，

\mu^*\left(\bigcup_{n=1}^{\infty}E_n\right) \le \sum_{n=1}^{\infty}\sum_{k=1}^{\infty}\mu_0(A_{n,k}) < \sum_{n=1}^{\infty}\mu^*(E_n)+\eps .

\eps>0 は任意なので可算劣加法性が従う． 次に A\in\calA なら1項被覆で \mu^*(A)\le\mu_0(A) である． 逆に A\subset\bigcup_n A_n を \calA の被覆とし， B_1=A\cap A_1，B_n=A\cap(A_n\setminus\bigcup_{k<n}A_k) とおくと， A=\bigsqcup_n B_n，B_n\in\calA，B_n\subset A_n である． 前測度性と単調性より \mu_0(A)=\sum_n\mu_0(B_n)\le\sum_n\mu_0(A_n) なので， 下限を取って \mu_0(A)\le\mu^*(A) を得る． 最後に A\in\calA と任意の E\subset X を取る． E\subset\bigcup_n A_n という任意の \calA-被覆を A_n\cap A と A_n\setminus A に分けると， \mu^*(E\cap A)+\mu^*(E\setminus A)\le\sum_n\mu_0(A_n) である． 下限を取ればCarathéodory条件の逆向きが従い，劣加法性と合わせて A は可測である．

Theorem6.5.3
Statement uses 3
Statement dependency previews
Preview
Theorem 6.3.3
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
used by 1✓L∃∀N
Tagsleanok

Carathéodory--Hahnの拡張定理. \calE を集合 X 上の半加法族， \mu_0 をその上の前測度とする． \overline\mu_0 を \calA(\calE) 上に延長した前測度， \mu^* を \overline\mu_0 から誘導した外測度， \calM_{\mu^*} を \mu^*-可測集合全体， \mu:=\mu^*|_{\calM_{\mu^*}} とする． このとき次が成り立つ．

  • \calE\subset\calS\subset\calM_{\mu^*} を満たす任意の \sigma-加法族 \calS に対し，\mu_{\calS}:=\mu|_{\calS} は (X,\calS) 上の測度であり，すべての E\in\calE に対して \mu_{\calS}(E)=\mu_0(E) を満たす．

  • とくに \sigma(\calE)=\sigma(\calA(\calE))\subset\calM_{\mu^*} であり， \calS=\sigma(\calE) と取れば通常の生成 \sigma-加法族上の拡張が得られる． また，\calS=\calM_{\mu^*} と取れば Theorem 6.3.3で得られる測度空間 (X,\calM_{\mu^*},\mu) そのものである．

  • \overline\mu_0 が \calA(\calE) 上で \sigma-有限ならば， 上の各 \calS 上でこの拡張は一意的である．

Lean code for Theorem6.5.3●5 declarations
  • defdefined in NoteKsk/«06caratheodory».lean
    complete
    def NoteKsk.Chapter06.measureFromPremeasure.{u_1} {α : Type u_1}
  {C : Set (Set α)} [MeasurableSpace α]
  (hC : MeasureTheory.IsSetSemiring C)
  (hgen : inst✝ ≤ NoteKsk.generatedSigmaAlgebra C)
  (m : MeasureTheory.AddContent ENNReal C)
  (hm : NoteKsk.IsPremeasureOnSemiring m) : MeasureTheory.Measure α
    def NoteKsk.Chapter06.measureFromPremeasure.{u_1}
  {α : Type u_1} {C : Set (Set α)}
  [MeasurableSpace α]
  (hC : MeasureTheory.IsSetSemiring C)
  (hgen :
    inst✝ ≤
      NoteKsk.generatedSigmaAlgebra C)
  (m : MeasureTheory.AddContent ENNReal C)
  (hm :
    NoteKsk.IsPremeasureOnSemiring m) :
  MeasureTheory.Measure α

    Definition body

    noncomputable def measureFromPremeasure [MeasurableSpace α]
    (hC : IsSetSemiring C)
    (hgen : ‹MeasurableSpace α› ≤ generatedSigmaAlgebra C)
    (m : AddContent ENNReal C) (hm : IsPremeasureOnSemiring m) :
    Measure α :=
  m.measure hC hgen hm
    A measure generated from a semiring premeasure on the current measurable space.
  • theoremdefined in NoteKsk/«06caratheodory».lean
    complete
    theorem NoteKsk.Chapter06.measureFromPremeasure_eq_on_semiring.{u_1}
  {α : Type u_1} {C : Set (Set α)} [MeasurableSpace α]
  (hC : MeasureTheory.IsSetSemiring C)
  (hgen : inst✝ = NoteKsk.generatedSigmaAlgebra C)
  (m : MeasureTheory.AddContent ENNReal C)
  (hm : NoteKsk.IsPremeasureOnSemiring m) {s : Set α} (hs : s ∈ C) :
  (NoteKsk.Chapter06.measureFromPremeasure hC ⋯ m hm) s = m s
    theorem NoteKsk.Chapter06.measureFromPremeasure_eq_on_semiring.{u_1}
  {α : Type u_1} {C : Set (Set α)}
  [MeasurableSpace α]
  (hC : MeasureTheory.IsSetSemiring C)
  (hgen :
    inst✝ =
      NoteKsk.generatedSigmaAlgebra C)
  (m : MeasureTheory.AddContent ENNReal C)
  (hm : NoteKsk.IsPremeasureOnSemiring m)
  {s : Set α} (hs : s ∈ C) :
  (NoteKsk.Chapter06.measureFromPremeasure
        hC ⋯ m hm)
      s =
    m s
  • theoremdefined in NoteKsk/«06caratheodory».lean
    complete
    theorem NoteKsk.Chapter06.caratheodoryHahn_extension_exists.{u_1} {α : Type u_1}
  {C : Set (Set α)} (hC : MeasureTheory.IsSetSemiring C)
  (m : MeasureTheory.AddContent ENNReal C)
  (hm : NoteKsk.IsPremeasureOnSemiring m) : ∃ μ, ∀ s ∈ C, μ s = m s
    theorem NoteKsk.Chapter06.caratheodoryHahn_extension_exists.{u_1}
  {α : Type u_1} {C : Set (Set α)}
  (hC : MeasureTheory.IsSetSemiring C)
  (m : MeasureTheory.AddContent ENNReal C)
  (hm :
    NoteKsk.IsPremeasureOnSemiring m) :
  ∃ μ, ∀ s ∈ C, μ s = m s
    Existence part of the Carathéodory--Hahn extension theorem.

Compared with the lecture statement, the generated measurable space is made
explicit in the type of the resulting measure.
  • theoremdefined in NoteKsk/«06caratheodory».lean
    complete
    theorem NoteKsk.Chapter06.caratheodoryHahn_extension_unique.{u_1} {α : Type u_1}
  {C : Set (Set α)} [MeasurableSpace α]
  (hgen : inst✝ = NoteKsk.generatedSigmaAlgebra C) (hπ : IsPiSystem C)
  {μ ν : MeasureTheory.Measure α} (hspan : μ.FiniteSpanningSetsIn C)
  (hμν : ∀ s ∈ C, μ s = ν s) : μ = ν
    theorem NoteKsk.Chapter06.caratheodoryHahn_extension_unique.{u_1}
  {α : Type u_1} {C : Set (Set α)}
  [MeasurableSpace α]
  (hgen :
    inst✝ =
      NoteKsk.generatedSigmaAlgebra C)
  (hπ : IsPiSystem C)
  {μ ν : MeasureTheory.Measure α}
  (hspan : μ.FiniteSpanningSetsIn C)
  (hμν : ∀ s ∈ C, μ s = ν s) : μ = ν
    Uniqueness part in mathlib's standard form.

The lecture notes state uniqueness under σ-finiteness on the generating
semiring.  Mathlib uses the more concrete hypothesis
`μ.FiniteSpanningSetsIn C`: a countable cover by members of the generator, each
with finite `μ`-measure.  This implies σ-finiteness and is the version used by
`Measure.FiniteSpanningSetsIn.ext`.
  • theoremdefined in NoteKsk/«06caratheodory».lean
    complete
    theorem NoteKsk.Chapter06.caratheodoryHahn_extension_unique_of_semiring.{u_1}
  {α : Type u_1} {C : Set (Set α)} [MeasurableSpace α]
  (hgen : inst✝ = NoteKsk.generatedSigmaAlgebra C)
  (hC : MeasureTheory.IsSetSemiring C) {μ ν : MeasureTheory.Measure α}
  (hspan : μ.FiniteSpanningSetsIn C) (hμν : ∀ s ∈ C, μ s = ν s) : μ = ν
    theorem NoteKsk.Chapter06.caratheodoryHahn_extension_unique_of_semiring.{u_1}
  {α : Type u_1} {C : Set (Set α)}
  [MeasurableSpace α]
  (hgen :
    inst✝ =
      NoteKsk.generatedSigmaAlgebra C)
  (hC : MeasureTheory.IsSetSemiring C)
  {μ ν : MeasureTheory.Measure α}
  (hspan : μ.FiniteSpanningSetsIn C)
  (hμν : ∀ s ∈ C, μ s = ν s) : μ = ν
Proof for Theorem 6.5.3
uses 0

Theorem 6.4.11により \overline\mu_0 は \calA(\calE) 上の前測度である． Theorem 6.5.2で外測度 \mu^* を作ると， \calA(\calE) の元はすべて \mu^*-可測で，\mu^* はその上で \overline\mu_0 と一致する． Theorem 6.3.3より \mu=\mu^*|_{\calM_{\mu^*}} は測度であり， \sigma(\calE)=\sigma(\calA(\calE))\subset\calM_{\mu^*} である． したがって \calE\subset\calS\subset\calM_{\mu^*} を満たす任意の \calS について， \mu_{\calS}:=\mu|_{\calS} は (X,\calS) 上の測度である． また E\in\calE なら \mu_{\calS}(E)=\mu^*(E)=\overline\mu_0(E)=\mu_0(E) であるから，これは求める拡張である．

一意性を示す． (X,\calS) 上の別の拡張を \nu とする． \calA(\calE)\subset\calS であり，有限加法性により \nu と \mu_{\calS} は \calA(\calE) 上で一致する． \sigma-有限性により X_n\in\calA(\calE)，X_n\uparrow X， \overline\mu_0(X_n)<\infty と取る． 任意の F\in\calS に対し F_n:=F\cap X_n とおく． 任意の \calA(\calE)-被覆 F_n\subset\bigcup_k A_k について \nu(F_n)\le\sum_k\overline\mu_0(A_k) だから \nu(F_n)\le\mu^*(F_n)． 逆向きは，X_n\setminus F の任意の \calA(\calE)-被覆を用いて \overline\mu_0(X_n)-\nu(F_n)\le\mu^*(X_n\setminus F) とし， X_n と F の \mu^*-可測性から \mu^*(F_n)=\overline\mu_0(X_n)-\mu^*(X_n\setminus F)\le\nu(F_n) を得る． よって \nu(F_n)=\mu_{\calS}(F_n) であり，F_n\uparrow F と測度の下からの連続性により \nu(F)=\mu_{\calS}(F) である．

Remark (Hopfの拡張定理との関係). 用語には揺れがあるが，ここでは前測度から測度が存在する部分を Carathéodory--Hahnの拡張定理と呼んだ． \sigma-有限性の仮定のもとで一意性まで述べる形をHopfの拡張定理と呼ぶ文献もある． 要点は，半加法族 \calE から有限加法族 \calA(\calE) へ延長し， そこから外測度を誘導し，Carathéodory可測集合へ制限するという流れである．

Proposition6.5.4
Statement uses 3
Statement dependency previews
Preview
Corollary 5.4.5
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
used by 0✓L∃∀N
Tagsleanokexample

Lebesgue測度. Proposition 6.4.2の \calE_d 上で \mu_0(\prod_{i=1}^d(a_i,b_i])=\prod_{i=1}^d(b_i-a_i)， \mu_0(\emptyset)=0 と定める． これは半加法族上の前測度である． この前測度から誘導される外測度はLebesgue外測度の定義そのものであり， Corollary 5.4.5により Carathéodory可測集合全体はLebesgue可測集合族 \calL_d と一致する． したがって Theorem 6.5.3 を \calS=\calL_d に適用すると，\calL_d 上に得られる測度 \mu^*|_{\calL_d} はLebesgue測度そのものである．

Lean code for Proposition6.5.4●1 theorem
  • theoremdefined in NoteKsk/«06caratheodory».lean
    complete
    theorem NoteKsk.Chapter06.lambdaStar_eq_inducedOuterMeasureFromBoxes {d : ℕ} :
  ∃ m,
    NoteKsk.IsPremeasureOnSemiring m ∧
      ∀ (A : Set (NoteKsk.Space d)),
        NoteKsk.Chapter03.lambdaStar A =
          (NoteKsk.Chapter06.inducedOuterMeasureFromPremeasure ⋯ m) A
    theorem NoteKsk.Chapter06.lambdaStar_eq_inducedOuterMeasureFromBoxes
  {d : ℕ} :
  ∃ m,
    NoteKsk.IsPremeasureOnSemiring m ∧
      ∀ (A : Set (NoteKsk.Space d)),
        NoteKsk.Chapter03.lambdaStar A =
          (NoteKsk.Chapter06.inducedOuterMeasureFromPremeasure
              ⋯ m)
            A
    The Lebesgue outer measure is the outer measure induced by the premeasure on
left half-open boxes.

The exact construction depends on reconciling the Chapter 03 box content with
mathlib's `AddContent` API, so this is left as a named bridge theorem.

Remark (Jordan測度). 有界区間（または有界矩形）I に含まれる左半開区間全体に空集合を加えた半加法族を \calE(I) とする． 区間の長さ・体積は \calE(I) 上の前測度を定める． さらに，これを有限加法的に \calA(\calE(I)) へ延長するところまでは， Lebesgue測度の構成とJordan測度の構成に共通する．

分岐点は，この有限加法族から任意の集合を外側近似する段階にある． Carathéodory流では \calA(\calE(I)) の元による可算被覆を許して誘導外測度を作る． 一方，Jordan流では有限被覆だけを許す． 有限個の基本集合の合併は再び \calA(\calE(I)) に属するので， Jordan外容量は

\inf\{\overline\mu_0(G)\mid G\in\calA(\calE(I)),\ A\subset G\}

という外側近似になる． この有限被覆に留める点が，可算被覆から測度を作るCarathéodory流との違いである．