Lebesgue積分講義ノート

2.1. \RR^dの基本集合🔗

Definition2.1.1
uses 0used by 1XL∃∀N

区間と長さ. 実数 a \le b に対し，

\begin{aligned} [a,b] &:= \{x \in \RR \mid a \le x \le b\}, & [a,b) &:= \{x \in \RR \mid a \le x < b\},\\ (a,b] &:= \{x \in \RR \mid a < x \le b\}, & (a,b) &:= \{x \in \RR \mid a < x < b\} \end{aligned}

を \RR の有界区間という． これらの長さは端点の開閉に依らず

|I| := b-a

で定める．

Definition2.1.2
uses 1used by 1✓L∃∀N
Tagsleanok

区間. \RR^d の有界区間とは， 各成分が有界区間である直積

R = I_1 \times \cdots \times I_d

のことである． その体積を

|R| := \prod_{k=1}^d |I_k|, \quad |\emptyset|=0

で定める． d=1,2,3 のときは，それぞれ長さ，面積，体積と呼ぶ．

Lean code for Definition2.1.2●9 definitions
  • abbrevdefined in NoteKsk/Defs.lean
    complete
    abbrev NoteKsk.Space (d : ℕ) : Type
    abbrev NoteKsk.Space (d : ℕ) : Type

    Definition body

    abbrev Space (d : ℕ) : Type := Fin d → ℝ

/-! ## Boxes and elementary sets -/
    The Lean model of `ℝ^d`.
  • structure(2 fields)defined in NoteKsk/Defs.lean
    complete
    structure NoteKsk.Box (d : ℕ) : Type
    structure NoteKsk.Box (d : ℕ) : Type
    A coordinate rectangle is recorded by lower and upper endpoints.

    Fields

    lower : NoteKsk.Space d
    upper : NoteKsk.Space d
  • defdefined in NoteKsk/Defs.lean
    complete
    def NoteKsk.Box.Ioo {d : ℕ} (Q : NoteKsk.Box d) : Set (NoteKsk.Space d)
    def NoteKsk.Box.Ioo {d : ℕ}
  (Q : NoteKsk.Box d) :
  Set (NoteKsk.Space d)

    Definition body

    def Ioo (Q : Box d) : Set (Space d) :=
  Set.pi Set.univ fun i => Set.Ioo (Q.lower i) (Q.upper i)
    Open rectangle `∏ i (a_i, b_i)`.
  • defdefined in NoteKsk/Defs.lean
    complete
    def NoteKsk.Box.Ioc {d : ℕ} (Q : NoteKsk.Box d) : Set (NoteKsk.Space d)
    def NoteKsk.Box.Ioc {d : ℕ}
  (Q : NoteKsk.Box d) :
  Set (NoteKsk.Space d)

    Definition body

    def Ioc (Q : Box d) : Set (Space d) :=
  Set.pi Set.univ fun i => Set.Ioc (Q.lower i) (Q.upper i)
    Left-open/right-closed rectangle `∏ i (a_i, b_i]`.
  • defdefined in NoteKsk/Defs.lean
    complete
    def NoteKsk.Box.Ico {d : ℕ} (Q : NoteKsk.Box d) : Set (NoteKsk.Space d)
    def NoteKsk.Box.Ico {d : ℕ}
  (Q : NoteKsk.Box d) :
  Set (NoteKsk.Space d)

    Definition body

    def Ico (Q : Box d) : Set (Space d) :=
  Set.pi Set.univ fun i => Set.Ico (Q.lower i) (Q.upper i)
    Left-closed/right-open rectangle `∏ i [a_i, b_i)`.
  • defdefined in NoteKsk/Defs.lean
    complete
    def NoteKsk.Box.Icc {d : ℕ} (Q : NoteKsk.Box d) : Set (NoteKsk.Space d)
    def NoteKsk.Box.Icc {d : ℕ}
  (Q : NoteKsk.Box d) :
  Set (NoteKsk.Space d)

    Definition body

    def Icc (Q : Box d) : Set (Space d) :=
  Set.Icc Q.lower Q.upper
    Closed rectangle `∏ i [a_i, b_i]`.
  • defdefined in NoteKsk/Defs.lean
    complete
    def NoteKsk.Box.volume {d : ℕ} (Q : NoteKsk.Box d) : ENNReal
    def NoteKsk.Box.volume {d : ℕ}
  (Q : NoteKsk.Box d) : ENNReal

    Definition body

    def volume (Q : Box d) : ENNReal :=
  ∏ i, ENNReal.ofReal (Q.upper i - Q.lower i)
    The formal volume of a rectangle, `∏ i (b_i - a_i)`, as an `ENNReal`.
  • defdefined in NoteKsk/Defs.lean
    complete
    def NoteKsk.Box.Nondegenerate {d : ℕ} (Q : NoteKsk.Box d) : Prop
    def NoteKsk.Box.Nondegenerate {d : ℕ}
  (Q : NoteKsk.Box d) : Prop

    Definition body

    def Nondegenerate (Q : Box d) : Prop :=
  ∀ i, Q.lower i < Q.upper i
    A nondegenerate finite rectangle.
  • defdefined in NoteKsk/Defs.lean
    complete
    def NoteKsk.IsLeftHalfOpenBox {d : ℕ} (S : Set (NoteKsk.Space d)) : Prop
    def NoteKsk.IsLeftHalfOpenBox {d : ℕ}
  (S : Set (NoteKsk.Space d)) : Prop

    Definition body

    def IsLeftHalfOpenBox {d : ℕ} (S : Set (Space d)) : Prop :=
  S = ∅ ∨ ∃ Q : Box d, Q.Nondegenerate ∧ Q.Ioc = S
    The family `𝓔_d`: left half-open rectangles together with the empty set.
Endpoints are finite real numbers at this stage of the development.

Remark. 端点の開閉は体積に影響しない． 後で見るように，境界は後でJordan零集合として無視できるので，閉区間・開区間・半開区間の違いは本質的でない． 以後，有限分割を扱う際には

Q = \prod_{k=1}^d (a_k,b_k]

という左半開区間を主に用いる． \RR^dの左半開区間の全体に空集合を加えた集合族を\calE_dと書く．

Definition2.1.3
uses 1
Used by 5
Reverse dependency previews
Preview
Lemma 2.1.4
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N
Tagsleanok

基本集合. \RR^d の基本集合とは， 有限個の互いに素な \calE_d の元の合併

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

のことである． このとき

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

と定める．\RR^dの基本集合の全体を\calA_dと書く．m_Jは集合族\calA_d上の非負値関数である．

Lean code for Definition2.1.3●2 definitions
  • defdefined in NoteKsk/Defs.lean
    complete
    def NoteKsk.IsElementarySet {d : ℕ} (S : Set (NoteKsk.Space d)) : Prop
    def NoteKsk.IsElementarySet {d : ℕ}
  (S : Set (NoteKsk.Space d)) : Prop

    Definition body

    def IsElementarySet {d : ℕ} (S : Set (Space d)) : Prop :=
  ∃ n : ℕ, ∃ Q : Fin n → Box d,
    (∀ j, (Q j).Nondegenerate) ∧
    (∀ ⦃i j : Fin n⦄, i ≠ j → Disjoint ((Q i).Ioc) ((Q j).Ioc)) ∧
    S = ⋃ j, (Q j).Ioc
    Elementary sets `𝓐_d`: finite disjoint unions of nondegenerate left half-open boxes.
  • defdefined in NoteKsk/Defs.lean
    complete
    def NoteKsk.elementaryVolume {d : ℕ} (E : Set (NoteKsk.Space d)) : ENNReal
    def NoteKsk.elementaryVolume {d : ℕ}
  (E : Set (NoteKsk.Space d)) : ENNReal

    Definition body

    def elementaryVolume {d : ℕ} (E : Set (Space d)) : ENNReal :=
  (volume : Measure (Space d)) E
    The volume assigned to an elementary set.  This is deliberately defined by
mathlib's `volume` for now; Chapter 2 later proves that this agrees with the
finite disjoint-box presentation.
Lemma2.1.4
uses 1used by 1!L∃∀N
Tagsnotready

格子分割. 有限個の \calE_d の元\{B_i\}_{i=1}^nの合併 A = \bigcup_{i=1}^n B_iは，ある互いに素な \calE_d の元\{Q_j\}_{j=1}^mからなる基本集合\bigsqcup_{j=1}^m Q_jとして書き直せる．

A = \bigcup_{i=1}^n B_i = \bigsqcup_{j=1}^m Q_j.

一般にこのような基本集合の取り方は一意ではないが，その体積\sum_{j=1}^m |Q_j|は基本集合の取り方に依らない．

Lean code for Lemma2.1.4●2 declarations, 2 missing
Proof for Lemma 2.1.4
uses 0

（考え方：各区間B_iを細分し，互いに素な小半開区間Q_jをつくる．）

Theorem2.1.5
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
Tagsnotready

基本集合の測度の性質. 基本集合 E,F \subset \RR^d に対して次が成り立つ．

  • （非負性）m_J(E) \ge 0，特に m_J(\emptyset)=0

  • （単調性）E \subset F ならば m_J(E) \le m_J(F)

  • （加法性）E \cap F = \emptyset ならば m_J(E \sqcup F) = m_J(E) + m_J(F)

  • （平行移動不変性）任意の c \in \RR^d に対して m_J(E+c) = m_J(E)

Lean code for Theorem2.1.5●5 declarations, 2 missing
  • theoremdefined in NoteKsk/«02jordan».lean
    complete
    theorem NoteKsk.Chapter02.elementaryVolume_empty {d : ℕ} :
  NoteKsk.elementaryVolume ∅ = 0
    theorem NoteKsk.Chapter02.elementaryVolume_empty
  {d : ℕ} : NoteKsk.elementaryVolume ∅ = 0
  • theoremdefined in NoteKsk/«02jordan».lean
    complete
    theorem NoteKsk.Chapter02.elementaryVolume_nonneg {d : ℕ}
  (E : Set (NoteKsk.Space d)) : 0 ≤ NoteKsk.elementaryVolume E
    theorem NoteKsk.Chapter02.elementaryVolume_nonneg
  {d : ℕ} (E : Set (NoteKsk.Space d)) :
  0 ≤ NoteKsk.elementaryVolume E
  • theoremdefined in NoteKsk/«02jordan».lean
    complete
    theorem NoteKsk.Chapter02.elementaryVolume_mono {d : ℕ}
  {E F : Set (NoteKsk.Space d)} (hEF : E ⊆ F) :
  NoteKsk.elementaryVolume E ≤ NoteKsk.elementaryVolume F
    theorem NoteKsk.Chapter02.elementaryVolume_mono
  {d : ℕ} {E F : Set (NoteKsk.Space d)}
  (hEF : E ⊆ F) :
  NoteKsk.elementaryVolume E ≤
    NoteKsk.elementaryVolume F
  • NoteKsk.Chapter02.elementaryVolume_union_of_disjointmissing declaration
    declaration not found (name was not present during directive/code-block registration)
  • NoteKsk.Chapter02.elementaryVolume_translatemissing declaration
    declaration not found (name was not present during directive/code-block registration)
Proof for Theorem 2.1.5
uses 0

補題より，E,F に現れる全ての端点を集めた共通の格子分割

\calP=\{R_1,\dots,R_N\}

を取れば，ある添字集合 I,J \subset \{1,\dots,N\} が存在して

E=\bigsqcup_{i\in I} R_i, \qquad F=\bigsqcup_{i\in J} R_i

と書ける． このとき

m_J(E)=\sum_{i\in I}|R_i|, \qquad m_J(F)=\sum_{i\in J}|R_i|

である．

  • 各 |R_i| \ge 0 であるから

m_J(E)=\sum_{i\in I}|R_i| \ge 0.

また \emptyset=\bigsqcup_{i\in\emptyset}R_i だから

m_J(\emptyset)=\sum_{i\in\emptyset}|R_i|=0.

  • E \subset F ならば，各 R_i は互いに素であるから I \subset J である． したがって

m_J(F)-m_J(E) =\sum_{i\in J}|R_i|-\sum_{i\in I}|R_i| =\sum_{i\in J\setminus I}|R_i| \ge 0,

よって m_J(E)\le m_J(F) である．

  • E \cap F=\emptyset ならば I\cap J=\emptyset であり，

E\sqcup F=\bigsqcup_{i\in I\cup J}R_i

だから

m_J(E\sqcup F) =\sum_{i\in I\cup J}|R_i| =\sum_{i\in I}|R_i|+\sum_{i\in J}|R_i| =m_J(E)+m_J(F).

  • c=(c_1,\dots,c_d)\in\RR^d とする． 各 R_i=\prod_{k=1}^d(a_{i,k},b_{i,k}] に対して

R_i+c=\prod_{k=1}^d(a_{i,k}+c_k,b_{i,k}+c_k]

であり，

|R_i+c| =\prod_{k=1}^d\bigl((b_{i,k}+c_k)-(a_{i,k}+c_k)\bigr) =\prod_{k=1}^d(b_{i,k}-a_{i,k}) =|R_i|.

ゆえに

E+c=\bigsqcup_{i\in I}(R_i+c)

かつ

m_J(E+c) =\sum_{i\in I}|R_i+c| =\sum_{i\in I}|R_i| =m_J(E).