Lebesgue積分講義ノート

3.5. Lebesgue外測度の性質🔗

Definition3.5.1
uses 0used by 0✓L∃∀N

Carathéodory外測度. 集合 X 上の集合関数

\mu^* : \mathcal P(X) \to [0,\infty]

が（Carathéodory）外測度であるとは，次の3条件を満たすことをいう．

  • \mu^*(\emptyset)=0

  • （単調性）A \subset B ならば \mu^*(A) \le \mu^*(B)

  • （可算劣加法性）任意の集合列 \{A_n\}_{n=1}^{\infty} に対して

\mu^*\left(\bigcup_{n=1}^{\infty} A_n\right) \le \sum_{n=1}^{\infty} \mu^*(A_n)

が成り立つ

Lean code for Definition3.5.1●2 definitions
  • defdefined in NoteKsk/«03lebesgue-outer».lean
    complete
    def NoteKsk.Chapter03.IsOuterMeasureFunction.{u_1} {α : Type u_1}
  (μ : Set α → ENNReal) : Prop
    def NoteKsk.Chapter03.IsOuterMeasureFunction.{u_1}
  {α : Type u_1} (μ : Set α → ENNReal) :
  Prop

    Definition body

    def IsOuterMeasureFunction {α : Type*} (μ : Set α → ENNReal) : Prop :=
  μ ∅ = 0 ∧
    (∀ ⦃A B : Set α⦄, A ⊆ B → μ A ≤ μ B) ∧
    (∀ A : ℕ → Set α, μ (⋃ n, A n) ≤ ∑' n, μ (A n))
    Unbundled outer-measure axioms for comparison with the text.
  • 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)
Theorem3.5.2
uses 1
Used by 3
Reverse dependency previews
Preview
Theorem 3.7.1
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N
Tagsleanok

Lebesgue外測度は外測度. \lambda^* は \RR^d 上のCarathéodory外測度である．

Lean code for Theorem3.5.2●5 theorems
  • theoremdefined in NoteKsk/«03lebesgue-outer».lean
    complete
    theorem NoteKsk.Chapter03.lambdaStar_empty {d : ℕ} :
  NoteKsk.Chapter03.lambdaStar ∅ = 0
    theorem NoteKsk.Chapter03.lambdaStar_empty
  {d : ℕ} :
  NoteKsk.Chapter03.lambdaStar ∅ = 0
  • theoremdefined in NoteKsk/«03lebesgue-outer».lean
    complete
    theorem NoteKsk.Chapter03.lambdaStar_mono {d : ℕ} {A B : Set (NoteKsk.Space d)}
  (hAB : A ⊆ B) :
  NoteKsk.Chapter03.lambdaStar A ≤ NoteKsk.Chapter03.lambdaStar B
    theorem NoteKsk.Chapter03.lambdaStar_mono {d : ℕ}
  {A B : Set (NoteKsk.Space d)}
  (hAB : A ⊆ B) :
  NoteKsk.Chapter03.lambdaStar A ≤
    NoteKsk.Chapter03.lambdaStar B
  • theoremdefined in NoteKsk/«03lebesgue-outer».lean
    complete
    theorem NoteKsk.Chapter03.lambdaStar_iUnion_le {d : ℕ}
  (A : ℕ → Set (NoteKsk.Space d)) :
  NoteKsk.Chapter03.lambdaStar (⋃ n, A n) ≤
    ∑' (n : ℕ), NoteKsk.Chapter03.lambdaStar (A n)
    theorem NoteKsk.Chapter03.lambdaStar_iUnion_le
  {d : ℕ}
  (A : ℕ → Set (NoteKsk.Space d)) :
  NoteKsk.Chapter03.lambdaStar
      (⋃ n, A n) ≤
    ∑' (n : ℕ),
      NoteKsk.Chapter03.lambdaStar (A n)
  • theoremdefined in NoteKsk/«03lebesgue-outer».lean
    complete
    theorem NoteKsk.Chapter03.lambdaStar_union_le {d : ℕ}
  (A B : Set (NoteKsk.Space d)) :
  NoteKsk.Chapter03.lambdaStar (A ∪ B) ≤
    NoteKsk.Chapter03.lambdaStar A + NoteKsk.Chapter03.lambdaStar B
    theorem NoteKsk.Chapter03.lambdaStar_union_le
  {d : ℕ} (A B : Set (NoteKsk.Space d)) :
  NoteKsk.Chapter03.lambdaStar (A ∪ B) ≤
    NoteKsk.Chapter03.lambdaStar A +
      NoteKsk.Chapter03.lambdaStar B
  • theoremdefined in NoteKsk/«03lebesgue-outer».lean
    complete
    theorem NoteKsk.Chapter03.lambdaStar_isOuterMeasureFunction (d : ℕ) :
  NoteKsk.Chapter03.IsOuterMeasureFunction fun A ↦
    NoteKsk.Chapter03.lambdaStar A
    theorem NoteKsk.Chapter03.lambdaStar_isOuterMeasureFunction
  (d : ℕ) :
  NoteKsk.Chapter03.IsOuterMeasureFunction
    fun A ↦ NoteKsk.Chapter03.lambdaStar A
    `λ*` is a Carathéodory outer measure in the unbundled sense of the notes.
Proof for Theorem 3.5.2
uses 0

  • \lambda^*(\emptyset)=0： まず定義から \lambda^*(\emptyset)\ge 0 である． 一方，

\emptyset \subset \bigcup_{n=1}^{\infty}\emptyset

であるから

\lambda^*(\emptyset) \le \sum_{n=1}^{\infty} |\emptyset| = 0.

よって \lambda^*(\emptyset)=0 である．

  • 単調性： A \subset B とする． B の任意の可算被覆

B \subset \bigcup_{n=1}^{\infty} R_n

はそのまま A の可算被覆でもある． したがって，A に対する下限は B に対する下限以下であり，

\lambda^*(A) \le \lambda^*(B)

を得る．

  • 可算劣加法性： 集合列 \{A_n\}_{n=1}^{\infty} を取る． もし

\sum_{n=1}^{\infty}\lambda^*(A_n)=\infty

なら不等式は自明である． したがって右辺が有限であるとし，\eps > 0 を任意に取る． 各 n に対して，\lambda^*(A_n) の定義より A_n を覆う可算個の区間 \{R_{n,k}\}_{k=1}^{\infty} を

A_n \subset \bigcup_{k=1}^{\infty} R_{n,k}, \qquad \sum_{k=1}^{\infty} |R_{n,k}| < \lambda^*(A_n) + \frac{\eps}{2^n}

となるように取れる． すると二重列 \{R_{n,k}\}_{n,k} は可算個の区間からなり，

\bigcup_{n=1}^{\infty} A_n \subset \bigcup_{n=1}^{\infty}\bigcup_{k=1}^{\infty} R_{n,k}

であるから，

\begin{aligned} \lambda^*\left(\bigcup_{n=1}^{\infty} A_n\right) &\le \sum_{n=1}^{\infty}\sum_{k=1}^{\infty} |R_{n,k}| \\ &< \sum_{n=1}^{\infty} \left( \lambda^*(A_n)+\frac{\eps}{2^n} \right) \\ &= \sum_{n=1}^{\infty}\lambda^*(A_n)+\eps. \end{aligned}

\eps > 0 は任意だから

\lambda^*\left(\bigcup_{n=1}^{\infty} A_n\right) \le \sum_{n=1}^{\infty}\lambda^*(A_n)

が従う．

Proposition3.5.3
uses 1used by 1✓L∃∀N
Tagsleanok

平行移動不変性. 任意の A \subset \RR^d と c \in \RR^d に対して

\lambda^*(A+c)=\lambda^*(A)

が成り立つ．

Lean code for Proposition3.5.3●1 theorem
  • theoremdefined in NoteKsk/«03lebesgue-outer».lean
    complete
    theorem NoteKsk.Chapter03.lambdaStar_translate {d : ℕ}
  (A : Set (NoteKsk.Space d)) (c : NoteKsk.Space d) :
  NoteKsk.Chapter03.lambdaStar (NoteKsk.translate A c) =
    NoteKsk.Chapter03.lambdaStar A
    theorem NoteKsk.Chapter03.lambdaStar_translate
  {d : ℕ} (A : Set (NoteKsk.Space d))
  (c : NoteKsk.Space d) :
  NoteKsk.Chapter03.lambdaStar
      (NoteKsk.translate A c) =
    NoteKsk.Chapter03.lambdaStar A
    Lebesgue outer measure is invariant under translations.
Proof for Proposition 3.5.3
uses 0

A \subset \bigcup_{n=1}^{\infty} R_n ならば

A+c \subset \bigcup_{n=1}^{\infty} (R_n+c)

であり，平行移動は各辺の長さを変えないので

|R_n+c| = |R_n|

である． したがって

\lambda^*(A+c) \le \sum_{n=1}^{\infty} |R_n|

となるから，A の被覆について下限を取って

\lambda^*(A+c) \le \lambda^*(A)

を得る． 逆向きの不等式は -c だけ平行移動すれば従う．