Lebesgue積分講義ノート

3.3. Lebesgue外測度の定義🔗

以後，次元 d \in \NN を固定する． 第2章の記法に拡大実数を含めるため，以下のように約束する

  • \eRR の区間とは，-\infty \le a < b \le \infty に対し，I = (a,b), (a,b], [a,b), [a,b], \text{or } \emptyset である．便宜的に，空集合 \emptyset も区間に含める．

  • \eRR^d の区間 R = \prod_{i=1}^d I_i の体積を |R| = \prod_{i=1}^d (b_i - a_i) で表す．また空集合の体積を |\emptyset|:=0 と約束する．区間に一つでも\pm \inftyが含まれるときは |R|=\inftyとする．

  • \eRR^d の左半開区間の全体に空集合を加えたものを \calE_d := \left\{ \prod_{i=1}^d (a_i,b_i] \;\middle|\; a_i < b_i \right\} \cup \{ \emptyset\}

    と書く

  • \eRR^d の基本集合（互いに素な左半開区間の有限合併）の全体を \calA_d := \bigcup_{n \in \NN} \left\{ \bigsqcup_{j=1}^n Q_j \;\middle|\; Q_j \in \calE_d\right\} と書く．区間の定義に拡大実数を含めたことにより，\calA_dは有限加法族である．

Definition3.3.1
uses 0
Used by 8
Reverse dependency previews
Preview
Proposition 3.3.2
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N
Tagsleanok

Lebesgue外測度. 集合 A \subset \RR^d に対し，A のLebesgue外測度 \lambda^*(A) を

\lambda^*(A) := \inf\left\{ \sum_{i=1}^{\infty} |R_i| \;\middle|\; A \subset \bigcup_{i=1}^{\infty} R_i,\ R_i \in \calE_d \right\}

で定める．

Lean code for Definition3.3.1●9 declarations
  • abbrevdefined in NoteKsk/«03lebesgue-outer».lean
    complete
    abbrev NoteKsk.Chapter03.lebesgueOuterMeasure (d : ℕ) :
  MeasureTheory.OuterMeasure (NoteKsk.Space d)
    abbrev NoteKsk.Chapter03.lebesgueOuterMeasure
  (d : ℕ) :
  MeasureTheory.OuterMeasure
    (NoteKsk.Space d)

    Definition body

    abbrev lebesgueOuterMeasure (d : ℕ) : OuterMeasure (Space d) :=
  (volume : Measure (Space d)).toOuterMeasure
    Bundled Lebesgue outer measure on `ℝ^d`.
  • abbrevdefined in NoteKsk/«03lebesgue-outer».lean
    complete
    abbrev NoteKsk.Chapter03.lambdaStar {d : ℕ} (A : Set (NoteKsk.Space d)) :
  ENNReal
    abbrev NoteKsk.Chapter03.lambdaStar {d : ℕ}
  (A : Set (NoteKsk.Space d)) : ENNReal

    Definition body

    abbrev lambdaStar {d : ℕ} (A : Set (Space d)) : ENNReal :=
  (volume : Measure (Space d)) A
    Lebesgue outer measure `λ*`.

In mathlib this is simply Lebesgue measure `volume` evaluated on an arbitrary set.
For measurable sets it is the usual measure; for nonmeasurable sets it is the
corresponding outer-measure value.
  • inductive(2 constructors, 1 parameter)defined in NoteKsk/«03lebesgue-outer».lean
    complete
    inductive NoteKsk.Chapter03.CoverBox (d : ℕ) : Type
    inductive NoteKsk.Chapter03.CoverBox (d : ℕ) : Type
    A covering piece is either a left half-open box or the explicitly allowed empty set.

    Constructors

    NoteKsk.Chapter03.CoverBox.empty {d : ℕ} :
  NoteKsk.Chapter03.CoverBox d
    NoteKsk.Chapter03.CoverBox.box {d : ℕ} :
  NoteKsk.Box d → NoteKsk.Chapter03.CoverBox d
  • defdefined in NoteKsk/«03lebesgue-outer».lean
    complete
    def NoteKsk.Chapter03.CoverBox.carrier {d : ℕ} :
  NoteKsk.Chapter03.CoverBox d → Set (NoteKsk.Space d)
    def NoteKsk.Chapter03.CoverBox.carrier
  {d : ℕ} :
  NoteKsk.Chapter03.CoverBox d →
    Set (NoteKsk.Space d)

    Definition body

    def carrier : CoverBox d → Set (Space d)
  | empty => ∅
  | box Q => Q.Ioc
    The set carried by a covering piece.
  • defdefined in NoteKsk/«03lebesgue-outer».lean
    complete
    def NoteKsk.Chapter03.CoverBox.volume {d : ℕ} :
  NoteKsk.Chapter03.CoverBox d → ENNReal
    def NoteKsk.Chapter03.CoverBox.volume
  {d : ℕ} :
  NoteKsk.Chapter03.CoverBox d → ENNReal

    Definition body

    def volume : CoverBox d → ENNReal
  | empty => 0
  | box Q => Q.volume
    The volume of a covering piece.
  • defdefined in NoteKsk/«03lebesgue-outer».lean
    complete
    def NoteKsk.Chapter03.IsBoxCover {d : ℕ} (A : Set (NoteKsk.Space d))
  (Q : ℕ → NoteKsk.Chapter03.CoverBox d) : Prop
    def NoteKsk.Chapter03.IsBoxCover {d : ℕ}
  (A : Set (NoteKsk.Space d))
  (Q : ℕ → NoteKsk.Chapter03.CoverBox d) :
  Prop

    Definition body

    def IsBoxCover {d : ℕ} (A : Set (Space d)) (Q : ℕ → CoverBox d) : Prop :=
  A ⊆ ⋃ n, (Q n).carrier
    A sequence of boxes covers `A`.
  • defdefined in NoteKsk/«03lebesgue-outer».lean
    complete
    def NoteKsk.Chapter03.boxCoverCost {d : ℕ}
  (Q : ℕ → NoteKsk.Chapter03.CoverBox d) : ENNReal
    def NoteKsk.Chapter03.boxCoverCost {d : ℕ}
  (Q : ℕ → NoteKsk.Chapter03.CoverBox d) :
  ENNReal

    Definition body

    def boxCoverCost {d : ℕ} (Q : ℕ → CoverBox d) : ENNReal :=
  ∑' n, (Q n).volume
    Cost of a countable box cover, `∑ n |Q_n|`.
  • defdefined in NoteKsk/«03lebesgue-outer».lean
    complete
    def NoteKsk.Chapter03.lambdaStarByBoxes {d : ℕ}
  (A : Set (NoteKsk.Space d)) : ENNReal
    def NoteKsk.Chapter03.lambdaStarByBoxes
  {d : ℕ} (A : Set (NoteKsk.Space d)) :
  ENNReal

    Definition body

    def lambdaStarByBoxes {d : ℕ} (A : Set (Space d)) : ENNReal :=
  ⨅ Q : ℕ → CoverBox d, ⨅ _hQ : IsBoxCover A Q, boxCoverCost Q
    The blueprint definition: infimum of costs over all countable covers by left
half-open boxes.
  • theoremdefined in NoteKsk/«03lebesgue-outer».lean
    complete
    theorem NoteKsk.Chapter03.lambdaStar_eq_iInf_boxCovers {d : ℕ}
  (A : Set (NoteKsk.Space d)) :
  NoteKsk.Chapter03.lambdaStar A = NoteKsk.Chapter03.lambdaStarByBoxes A
    theorem NoteKsk.Chapter03.lambdaStar_eq_iInf_boxCovers
  {d : ℕ} (A : Set (NoteKsk.Space d)) :
  NoteKsk.Chapter03.lambdaStar A =
    NoteKsk.Chapter03.lambdaStarByBoxes A
    The box-cover definition agrees with mathlib's Lebesgue outer measure.

This is the formal version of the definition in the lecture notes.  The
nontrivial construction direction is isolated in
`lambdaStarByBoxes_le_lambdaStar`.

Remark. 可算被覆の基本単位 R_i として区間（\calE_d）ではなく基本集合（\calA_d）を採用しても同じ量を定める．

Remark. 有限被覆 A \subset \bigcup_{i=1}^n Q_i は可算被覆の特別な場合

A \subset \bigcup_{i=1}^\infty R_i, \qquad R_i := \begin{cases} Q_i, & i \le n,\\ \emptyset, & i > n \end{cases}

である． したがって，Lebesgue外測度はJordan外測度よりも精密に近似できる．

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

Jordan外測度との比較. 有界集合 A \subset \RR^d に対して

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

が成り立つ．

Lean code for Proposition3.3.2●1 theorem
  • theoremdefined in NoteKsk/«03lebesgue-outer».lean
    complete
    theorem NoteKsk.Chapter03.lambdaStar_le_jordanOuterMeasure {d : ℕ}
  {A : Set (NoteKsk.Space d)} (_hA : Bornology.IsBounded A) :
  NoteKsk.Chapter03.lambdaStar A ≤ NoteKsk.jordanOuterMeasure A
    theorem NoteKsk.Chapter03.lambdaStar_le_jordanOuterMeasure
  {d : ℕ} {A : Set (NoteKsk.Space d)}
  (_hA : Bornology.IsBounded A) :
  NoteKsk.Chapter03.lambdaStar A ≤
    NoteKsk.jordanOuterMeasure A
    Lebesgue outer measure is bounded above by Jordan outer measure on bounded sets.
This is a Chapter 2 compatibility statement.
Proof for Proposition 3.3.2
uses 0

A \subset E を満たす基本集合 E を取る． E は互いに素な左半開区間の有限合併

E = \bigsqcup_{j=1}^N Q_j

と書け，

m_J(E) = \sum_{j=1}^N |Q_j|

であった． この有限個の区間の族は A の可算被覆でもあるから，

\lambda^*(A) \le \sum_{j=1}^N |Q_j| = m_J(E)

を得る． E の取り方について下限を取ればよい．