Lebesgue積分講義ノート

6.3. 外測度とCarathéodory可測性🔗

Definition6.3.1
uses 1
Used by 2
Reverse dependency previews
Preview
Definition 6.3.2
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N
Tagsmathlibok

外測度. 集合 X 上の写像 \mu^*:\calP(X)\to[0,\infty] が外測度であるとは， 次を満たすことをいう．

  • \mu^*(\emptyset)=0．

  • A\subset B ならば \mu^*(A)\le\mu^*(B)．

  • 任意の集合列 \{A_n\}_{n=1}^{\infty}\subset\calP(X) に対して \mu^*(\bigcup_{n=1}^{\infty}A_n)\le\sum_{n=1}^{\infty}\mu^*(A_n)．

Lean code for Definition6.3.1●4 declarations
  • structure(4 fields)defined in Mathlib/MeasureTheory/OuterMeasure/Defs.lean
    complete
    structure MeasureTheory.OuterMeasure.{u_2} (α : Type u_2) : Type u_2
    structure MeasureTheory.OuterMeasure.{u_2}
  (α : Type u_2) : Type u_2
    An outer measure is a countably subadditive monotone function that sends `∅` to `0`.

    Fields

    measureOf : Set α → ENNReal
    Outer measure function. Use automatic coercion instead. 
    empty : self.measureOf ∅ = 0
    mono : ∀ {s₁ s₂ : Set α}, s₁ ⊆ s₂ → self.measureOf s₁ ≤ self.measureOf s₂
    iUnion_nat : ∀ (s : ℕ → Set α), Pairwise (Function.onFun Disjoint s) → self.measureOf (⋃ i, s i) ≤ ∑' (i : ℕ), self.measureOf (s i)
  • theoremdefined in NoteKsk/«06caratheodory».lean
    complete
    theorem NoteKsk.Chapter06.outerMeasure_empty.{u_1} {α : Type u_1}
  (μ : MeasureTheory.OuterMeasure α) : μ ∅ = 0
    theorem NoteKsk.Chapter06.outerMeasure_empty.{u_1}
  {α : Type u_1}
  (μ : MeasureTheory.OuterMeasure α) :
  μ ∅ = 0
  • theoremdefined in NoteKsk/«06caratheodory».lean
    complete
    theorem NoteKsk.Chapter06.outerMeasure_mono.{u_1} {α : Type u_1}
  (μ : MeasureTheory.OuterMeasure α) {A B : Set α} (hAB : A ⊆ B) :
  μ A ≤ μ B
    theorem NoteKsk.Chapter06.outerMeasure_mono.{u_1}
  {α : Type u_1}
  (μ : MeasureTheory.OuterMeasure α)
  {A B : Set α} (hAB : A ⊆ B) : μ A ≤ μ B
  • theoremdefined in NoteKsk/«06caratheodory».lean
    complete
    theorem NoteKsk.Chapter06.outerMeasure_iUnion_le.{u_1} {α : Type u_1}
  (μ : MeasureTheory.OuterMeasure α) (A : ℕ → Set α) :
  μ (⋃ n, A n) ≤ ∑' (n : ℕ), μ (A n)
    theorem NoteKsk.Chapter06.outerMeasure_iUnion_le.{u_1}
  {α : Type u_1}
  (μ : MeasureTheory.OuterMeasure α)
  (A : ℕ → Set α) :
  μ (⋃ n, A n) ≤ ∑' (n : ℕ), μ (A n)
Definition6.3.2
uses 1
Used by 2
Reverse dependency previews
Preview
Theorem 6.3.3
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N
Tagsleanok

Carathéodory条件. 外測度 \mu^* に対し，集合 A\subset X がCarathéodory条件を満たすとは， 任意の E\subset X に対して

\mu^*(E)=\mu^*(E\cap A)+\mu^*(E\setminus A)

が成り立つことをいう． この条件を満たす集合を \mu^*-可測集合ともいう．

Lean code for Definition6.3.2●3 declarations
  • defdefined in NoteKsk/Defs.lean
    complete
    def NoteKsk.CaratheodoryMeasurableSet.{u_1} {α : Type u_1}
  (μ : MeasureTheory.OuterMeasure α) (A : Set α) : Prop
    def NoteKsk.CaratheodoryMeasurableSet.{u_1}
  {α : Type u_1}
  (μ : MeasureTheory.OuterMeasure α)
  (A : Set α) : Prop

    Definition body

    def CaratheodoryMeasurableSet {α : Type*} (μ : OuterMeasure α) (A : Set α) : Prop :=
  μ.IsCaratheodory A
    Carathéodory measurability for an outer measure.
  • abbrevdefined in NoteKsk/Defs.lean
    complete
    abbrev NoteKsk.caratheodoryMeasurableSpace.{u_1} {α : Type u_1}
  (μ : MeasureTheory.OuterMeasure α) : MeasurableSpace α
    abbrev NoteKsk.caratheodoryMeasurableSpace.{u_1}
  {α : Type u_1}
  (μ : MeasureTheory.OuterMeasure α) :
  MeasurableSpace α

    Definition body

    abbrev caratheodoryMeasurableSpace {α : Type*} (μ : OuterMeasure α) : MeasurableSpace α :=
  μ.caratheodory
    The measurable structure consisting of the Carathéodory-measurable sets of an outer measure.
  • theoremdefined in NoteKsk/«06caratheodory».lean
    complete
    theorem NoteKsk.Chapter06.caratheodoryMeasurable_iff.{u_1} {α : Type u_1}
  {μ : MeasureTheory.OuterMeasure α} {A : Set α} :
  NoteKsk.CaratheodoryMeasurableSet μ A ↔
    ∀ (E : Set α), μ E = μ (E ∩ A) + μ (E \ A)
    theorem NoteKsk.Chapter06.caratheodoryMeasurable_iff.{u_1}
  {α : Type u_1}
  {μ : MeasureTheory.OuterMeasure α}
  {A : Set α} :
  NoteKsk.CaratheodoryMeasurableSet μ A ↔
    ∀ (E : Set α),
      μ E = μ (E ∩ A) + μ (E \ A)
Theorem6.3.3
uses 1used by 1✓L∃∀N
Tagsleanok

Carathéodoryの定理. 外測度 \mu^* に関する \mu^*-可測集合全体を \calM_{\mu^*} と書く． このとき次が成り立つ．

  • \calM_{\mu^*} は X 上の \sigma-加法族である．

  • \mu:=\mu^*|_{\calM_{\mu^*}} は (X,\calM_{\mu^*}) 上の測度である．

  • \mu(N)=0 である可測集合 N の任意の部分集合も可測で，測度 0 をもつ．

Lean code for Theorem6.3.3●8 theorems
  • theoremdefined in NoteKsk/«06caratheodory».lean
    complete
    theorem NoteKsk.Chapter06.caratheodory_empty.{u_1} {α : Type u_1}
  (μ : MeasureTheory.OuterMeasure α) :
  NoteKsk.CaratheodoryMeasurableSet μ ∅
    theorem NoteKsk.Chapter06.caratheodory_empty.{u_1}
  {α : Type u_1}
  (μ : MeasureTheory.OuterMeasure α) :
  NoteKsk.CaratheodoryMeasurableSet μ ∅
  • theoremdefined in NoteKsk/«06caratheodory».lean
    complete
    theorem NoteKsk.Chapter06.caratheodory_univ.{u_1} {α : Type u_1}
  (μ : MeasureTheory.OuterMeasure α) :
  NoteKsk.CaratheodoryMeasurableSet μ Set.univ
    theorem NoteKsk.Chapter06.caratheodory_univ.{u_1}
  {α : Type u_1}
  (μ : MeasureTheory.OuterMeasure α) :
  NoteKsk.CaratheodoryMeasurableSet μ
    Set.univ
  • theoremdefined in NoteKsk/«06caratheodory».lean
    complete
    theorem NoteKsk.Chapter06.caratheodory_compl.{u_1} {α : Type u_1}
  {μ : MeasureTheory.OuterMeasure α} {A : Set α}
  (hA : NoteKsk.CaratheodoryMeasurableSet μ A) :
  NoteKsk.CaratheodoryMeasurableSet μ Aᶜ
    theorem NoteKsk.Chapter06.caratheodory_compl.{u_1}
  {α : Type u_1}
  {μ : MeasureTheory.OuterMeasure α}
  {A : Set α}
  (hA :
    NoteKsk.CaratheodoryMeasurableSet μ
      A) :
  NoteKsk.CaratheodoryMeasurableSet μ Aᶜ
  • theoremdefined in NoteKsk/«06caratheodory».lean
    complete
    theorem NoteKsk.Chapter06.caratheodory_union.{u_1} {α : Type u_1}
  {μ : MeasureTheory.OuterMeasure α} {A B : Set α}
  (hA : NoteKsk.CaratheodoryMeasurableSet μ A)
  (hB : NoteKsk.CaratheodoryMeasurableSet μ B) :
  NoteKsk.CaratheodoryMeasurableSet μ (A ∪ B)
    theorem NoteKsk.Chapter06.caratheodory_union.{u_1}
  {α : Type u_1}
  {μ : MeasureTheory.OuterMeasure α}
  {A B : Set α}
  (hA :
    NoteKsk.CaratheodoryMeasurableSet μ A)
  (hB :
    NoteKsk.CaratheodoryMeasurableSet μ
      B) :
  NoteKsk.CaratheodoryMeasurableSet μ
    (A ∪ B)
  • theoremdefined in NoteKsk/«06caratheodory».lean
    complete
    theorem NoteKsk.Chapter06.caratheodory_inter.{u_1} {α : Type u_1}
  {μ : MeasureTheory.OuterMeasure α} {A B : Set α}
  (hA : NoteKsk.CaratheodoryMeasurableSet μ A)
  (hB : NoteKsk.CaratheodoryMeasurableSet μ B) :
  NoteKsk.CaratheodoryMeasurableSet μ (A ∩ B)
    theorem NoteKsk.Chapter06.caratheodory_inter.{u_1}
  {α : Type u_1}
  {μ : MeasureTheory.OuterMeasure α}
  {A B : Set α}
  (hA :
    NoteKsk.CaratheodoryMeasurableSet μ A)
  (hB :
    NoteKsk.CaratheodoryMeasurableSet μ
      B) :
  NoteKsk.CaratheodoryMeasurableSet μ
    (A ∩ B)
  • theoremdefined in NoteKsk/«06caratheodory».lean
    complete
    theorem NoteKsk.Chapter06.caratheodory_iUnion.{u_1} {α : Type u_1}
  {μ : MeasureTheory.OuterMeasure α} (A : ℕ → Set α)
  (hA : ∀ (n : ℕ), NoteKsk.CaratheodoryMeasurableSet μ (A n)) :
  NoteKsk.CaratheodoryMeasurableSet μ (⋃ n, A n)
    theorem NoteKsk.Chapter06.caratheodory_iUnion.{u_1}
  {α : Type u_1}
  {μ : MeasureTheory.OuterMeasure α}
  (A : ℕ → Set α)
  (hA :
    ∀ (n : ℕ),
      NoteKsk.CaratheodoryMeasurableSet μ
        (A n)) :
  NoteKsk.CaratheodoryMeasurableSet μ
    (⋃ n, A n)
  • theoremdefined in NoteKsk/«06caratheodory».lean
    complete
    theorem NoteKsk.Chapter06.caratheodoryMeasurableSpace_iff.{u_1} {α : Type u_1}
  {μ : MeasureTheory.OuterMeasure α} {A : Set α} :
  MeasurableSet A ↔ NoteKsk.CaratheodoryMeasurableSet μ A
    theorem NoteKsk.Chapter06.caratheodoryMeasurableSpace_iff.{u_1}
  {α : Type u_1}
  {μ : MeasureTheory.OuterMeasure α}
  {A : Set α} :
  MeasurableSet A ↔
    NoteKsk.CaratheodoryMeasurableSet μ A
    The σ-algebra of Carathéodory-measurable sets.
  • theoremdefined in NoteKsk/«06caratheodory».lean
    complete
    theorem NoteKsk.Chapter06.caratheodory_outerMeasure_iUnion_eq_tsum.{u_1}
  {α : Type u_1} {μ : MeasureTheory.OuterMeasure α} (A : ℕ → Set α)
  (hA : ∀ (n : ℕ), MeasurableSet (A n))
  (hdisj : Pairwise (Function.onFun Disjoint A)) :
  μ (⋃ n, A n) = ∑' (n : ℕ), μ (A n)
    theorem NoteKsk.Chapter06.caratheodory_outerMeasure_iUnion_eq_tsum.{u_1}
  {α : Type u_1}
  {μ : MeasureTheory.OuterMeasure α}
  (A : ℕ → Set α)
  (hA : ∀ (n : ℕ), MeasurableSet (A n))
  (hdisj :
    Pairwise
      (Function.onFun Disjoint A)) :
  μ (⋃ n, A n) = ∑' (n : ℕ), μ (A n)
Proof for Theorem 6.3.3
uses 0

外測度の劣加法性より，Carathéodory条件では \mu^*(E)\ge\mu^*(E\cap A)+\mu^*(E\setminus A) だけを示せばよい． \emptyset と X が可測であること，および補集合で閉じていることは定義から直ちに従う．

まず有限和で閉じていることを示す． A,B を可測集合とし，任意の E\subset X を取る． A の可測性より

\mu^*(E) = \mu^*(E\cap A)+\mu^*(E\setminus A)

である． さらに B の可測性を E\setminus A に適用すると

\mu^*(E\setminus A) = \mu^*((E\setminus A)\cap B) + \mu^*((E\setminus A)\setminus B)

である． ここで (E\setminus A)\setminus B=E\setminus(A\cup B) だから

\mu^*(E) = \mu^*(E\cap A) + \mu^*((E\setminus A)\cap B) + \mu^*(E\setminus(A\cup B)).

一方，

E\cap(A\cup B) = (E\cap A)\cup((E\setminus A)\cap B)

なので，外測度の劣加法性より

\mu^*(E\cap(A\cup B)) \le \mu^*(E\cap A)+\mu^*((E\setminus A)\cap B)

である． したがって

\mu^*(E) \ge \mu^*(E\cap(A\cup B))+\mu^*(E\setminus(A\cup B)).

よって A\cup B は可測である． 帰納法により有限和で閉じており，補集合で閉じているので差集合でも閉じている．

次に可算和で閉じていることを示す． 可測集合列 \{A_n\}_{n=1}^{\infty} に対し，

B_1:=A_1,\qquad B_n:=A_n\setminus\bigcup_{k<n}A_k\quad(n\ge2)

とおく． 有限和と差集合で閉じていることから各 B_n は可測であり， B_n は互いに素で，

\bigcup_{n=1}^{\infty}A_n=\bigsqcup_{n=1}^{\infty}B_n

である． B:=\bigcup_{n=1}^{\infty}B_n，C_N:=\bigcup_{n=1}^{N}B_n とおく． 有限和で閉じているので C_N は可測である． また，互いに素な可測集合で順に切ると，任意の E\subset X について

\mu^*(E) = \sum_{n=1}^{N}\mu^*(E\cap B_n) + \mu^*(E\setminus C_N)

が成り立つ． 実際，N=1 では B_1 の可測性そのものであり， N で成り立つときは B_{N+1} の可測性を E\setminus C_N に適用すればよい． E\setminus B\subset E\setminus C_N だから単調性より

\mu^*(E) \ge \sum_{n=1}^{N}\mu^*(E\cap B_n) + \mu^*(E\setminus B)

である． N\to\infty として

\mu^*(E) \ge \sum_{n=1}^{\infty}\mu^*(E\cap B_n) + \mu^*(E\setminus B)

を得る． さらに外測度の可算劣加法性より

\mu^*(E\cap B) = \mu^*\left(\bigcup_{n=1}^{\infty}(E\cap B_n)\right) \le \sum_{n=1}^{\infty}\mu^*(E\cap B_n)

であるから，

\mu^*(E) \ge \mu^*(E\cap B)+\mu^*(E\setminus B)

となる． よって B は可測であり，可測集合の可算和も可測である． よって \calM_{\mu^*} は \sigma-加法族である．

互いに素な可測列 A_n と A=\bigsqcup_n A_n に対し， 上の有限段階の分解式を E=A，B_n=A_n に適用すると

\mu^*(A) = \sum_{n=1}^{N}\mu^*(A_n) + \mu^*\left(A\setminus\bigcup_{n=1}^{N}A_n\right) \ge \sum_{n=1}^{N}\mu^*(A_n)

がすべての N で成り立つ． よって \mu^*(A)\ge\sum_{n=1}^{\infty}\mu^*(A_n) である． 逆向きは外測度の可算劣加法性であるから， \mu(A)=\sum_n\mu(A_n) であり，\mu は測度である． 最後に N が可測で \mu(N)=0，A\subset N とする． 任意の E で \mu^*(E\cap A)=0 かつ \mu^*(E\setminus A)\le\mu^*(E) なので， A もCarathéodory条件を満たし，測度は 0 である．

Definition6.3.4
uses 1used by 1✓L∃∀N
Tagsleanok

完備測度と完備化.

  • 測度空間 (X,\calS,\mu) が完備であるとは， N\in\calS，\mu(N)=0，A\subset N ならば A\in\calS であることをいう．

  • 測度（空間）の完備化とは， 零集合の部分集合をすべて可測集合として加えた測度空間であり， たとえば \overline{\calS}:=\{A\triangle Z\mid A\in\calS,\ Z\subset N,\ N\in\calS,\ \mu(N)=0\} 上に \overline\mu(A\triangle Z):=\mu(A) と定めて得られる．

ここで A\triangle Z:=(A\setminus Z)\cup(Z\setminus A) は対称差を表す．

Lean code for Definition6.3.4●3 declarations
  • defdefined in NoteKsk/Defs.lean
    complete
    def NoteKsk.CompletedMeasurableSet.{u_1} {α : Type u_1} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α) (A : Set α) : Prop
    def NoteKsk.CompletedMeasurableSet.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  (A : Set α) : Prop

    Definition body

    def CompletedMeasurableSet {α : Type*} [MeasurableSpace α]
    (μ : Measure α) (A : Set α) : Prop :=
  NullMeasurableSet A μ
    The measurable sets in the completion of a measure.  Mathlib calls these
`NullMeasurableSet`s.
  • theoremdefined in NoteKsk/«06caratheodory».lean
    complete
    theorem NoteKsk.Chapter06.null_subset_completedMeasurableSet.{u_2}
  {α : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α}
  {N A : Set α} (hN : μ N = 0) (hA : A ⊆ N) :
  NoteKsk.CompletedMeasurableSet μ A
    theorem NoteKsk.Chapter06.null_subset_completedMeasurableSet.{u_2}
  {α : Type u_2} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {N A : Set α} (hN : μ N = 0)
  (hA : A ⊆ N) :
  NoteKsk.CompletedMeasurableSet μ A
    Null subsets are measurable in the completed measurable structure.
  • theoremdefined in NoteKsk/«06caratheodory».lean
    complete
    theorem NoteKsk.Chapter06.measure_completion_isComplete.{u_2} {α : Type u_2}
  [MeasurableSpace α] (μ : MeasureTheory.Measure α) :
  μ.completion.IsComplete
    theorem NoteKsk.Chapter06.measure_completion_isComplete.{u_2}
  {α : Type u_2} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α) :
  μ.completion.IsComplete