Lebesgue積分講義ノート

2.3. Jordan測度・Jordan可測🔗

Definition2.3.1
uses 1
Used by 4
Reverse dependency previews
Preview
Proposition 2.3.2
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N
Tagsleanok

Jordan外測度とJordan内測度. 集合 A \subset \RR^d に対し，

m_J^*(A) := \inf\{m_J(E) \mid E \text{ は基本集合},\ A \subset E\}

をJordan外測度，

m_{J,*}(A) := \sup\{m_J(E) \mid E \text{ は基本集合},\ E \subset A\}

をJordan内測度という．

Lean code for Definition2.3.1●2 definitions
  • defdefined in NoteKsk/Defs.lean
    complete
    def NoteKsk.jordanOuterMeasure {d : ℕ} (A : Set (NoteKsk.Space d)) : ENNReal
    def NoteKsk.jordanOuterMeasure {d : ℕ}
  (A : Set (NoteKsk.Space d)) : ENNReal

    Definition body

    def jordanOuterMeasure {d : ℕ} (A : Set (Space d)) : ENNReal :=
  ⨅ E : Set (Space d), ⨅ _hE : IsElementarySet E, ⨅ _hAE : A ⊆ E, elementaryVolume E
    Jordan outer measure: infimum of elementary volumes over elementary supersets.
  • defdefined in NoteKsk/Defs.lean
    complete
    def NoteKsk.jordanInnerMeasure {d : ℕ} (A : Set (NoteKsk.Space d)) : ENNReal
    def NoteKsk.jordanInnerMeasure {d : ℕ}
  (A : Set (NoteKsk.Space d)) : ENNReal

    Definition body

    def jordanInnerMeasure {d : ℕ} (A : Set (Space d)) : ENNReal :=
  ⨆ E : Set (Space d), ⨆ _hE : IsElementarySet E, ⨆ _hEA : E ⊆ A, elementaryVolume E
    Jordan inner measure: supremum of elementary volumes over elementary subsets.

Remark. Jordan理論は本質的に有界集合の理論である． 実際，A が有界でなければ，有限個の区間で A 全体を覆えないので m_J^*(A)=\infty となる． 後のLebesgue測度では，可算個の区間を使えるため， この有界性の制約が大きく緩和される．

Proposition2.3.2
uses 1used by 0!L∃∀N
Tagsnotready

任意の集合 A \subset \RR^d に対して

m_{J,*}(A) \le m_J^*(A)

が成り立つ．

Lean code for Proposition2.3.2●1 declaration, 1 missing
Proof for Proposition 2.3.2
uses 0

A を含む基本集合が存在しなければ m_J^*(A)=\infty であり自明である． そうでないとき，E \subset A \subset F を満たす基本集合 E,F に対して 基本集合の単調性より m_J(E) \le m_J(F) である． 左辺で上限を，右辺で下限を取ればよい．

Definition2.3.3
uses 1
Used by 4
Reverse dependency previews
Preview
Proposition 2.3.4
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N
Tagsleanok

Jordan可測・Jordan測度. 有界集合 A \subset \RR^d がJordan可測であるとは

m_{J,*}(A) = m_J^*(A)

が成り立つことをいう． その共通値を A のJordan測度と書き，m_J(A) で表す． \RR^dのJordan可測集合の全体を\calA_Jと書く． この定義により，m_Jは集合族\calA_J上の非負値関数に拡張された．

Lean code for Definition2.3.3●4 declarations
  • defdefined in NoteKsk/Defs.lean
    complete
    def NoteKsk.JordanMeasurable {d : ℕ} (A : Set (NoteKsk.Space d)) : Prop
    def NoteKsk.JordanMeasurable {d : ℕ}
  (A : Set (NoteKsk.Space d)) : Prop

    Definition body

    def JordanMeasurable {d : ℕ} (A : Set (Space d)) : Prop :=
  Bornology.IsBounded A ∧ MeasurableSet A ∧ jordanOuterMeasure A = jordanInnerMeasure A
    Jordan measurability, restricted to bounded sets as in the notes.

The `MeasurableSet` field records the later theorem that Jordan-measurable sets
are Lebesgue measurable; this lets Chapter 03 use mathlib's countable additivity
of `volume` without adding another placeholder.
  • defdefined in NoteKsk/Defs.lean
    complete
    def NoteKsk.jordanMeasure {d : ℕ} (A : Set (NoteKsk.Space d)) : ENNReal
    def NoteKsk.jordanMeasure {d : ℕ}
  (A : Set (NoteKsk.Space d)) : ENNReal

    Definition body

    def jordanMeasure {d : ℕ} (A : Set (Space d)) : ENNReal :=
  jordanOuterMeasure A
    Jordan measure of a Jordan-measurable set, represented by the outer value.
  • theoremdefined in NoteKsk/«02jordan».lean
    complete
    theorem NoteKsk.Chapter02.jordanMeasurable_iff {d : ℕ}
  {A : Set (NoteKsk.Space d)} :
  NoteKsk.JordanMeasurable A ↔
    Bornology.IsBounded A ∧
      MeasurableSet A ∧
        NoteKsk.jordanOuterMeasure A = NoteKsk.jordanInnerMeasure A
    theorem NoteKsk.Chapter02.jordanMeasurable_iff
  {d : ℕ} {A : Set (NoteKsk.Space d)} :
  NoteKsk.JordanMeasurable A ↔
    Bornology.IsBounded A ∧
      MeasurableSet A ∧
        NoteKsk.jordanOuterMeasure A =
          NoteKsk.jordanInnerMeasure A
  • theoremdefined in NoteKsk/«02jordan».lean
    complete
    theorem NoteKsk.Chapter02.jordanMeasure_eq_outer {d : ℕ}
  (A : Set (NoteKsk.Space d)) :
  NoteKsk.jordanMeasure A = NoteKsk.jordanOuterMeasure A
    theorem NoteKsk.Chapter02.jordanMeasure_eq_outer
  {d : ℕ} (A : Set (NoteKsk.Space d)) :
  NoteKsk.jordanMeasure A =
    NoteKsk.jordanOuterMeasure A
Proposition2.3.4
Statement uses 2
Statement dependency previews
Preview
Definition 2.1.3
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
used by 0!L∃∀N
Tagsnotreadyexample

基本集合はJordan可測であり，そのJordan測度は最初に定めた m_J に一致する

Lean code for Proposition2.3.4●2 declarations, 2 missing
Proof for Proposition 2.3.4
uses 0

基本集合 E 自身を内側近似と外側近似に取れば m_{J,*}(E)=m_J^*(E)=m_J(E) である．