6.6. Borel集合族🔗

Definition6.6.1

uses 1

Used by 2

Reverse dependency previews

Preview

Theorem 6.6.3

Loading preview

Reverse dependency preview content is loaded from the Blueprint HTML cache.

✓L∃∀N

Tagsleanok

Borel集合族. 位相空間 X に対し，X の開集合全体を \calO(X) と書く． \calB(X):=\sigma(\calO(X)) を X のBorel集合族といい， \calB(X) の元をBorel集合という．

Lean code for Definition6.6.1●1 definition

abbrevdefined in NoteKsk/«06caratheodory».lean

complete

abbrev NoteKsk.Chapter06.borelSigmaAlgebra.{u_1} (α : Type u_1)
  [TopologicalSpace α] : MeasurableSpace α

abbrev NoteKsk.Chapter06.borelSigmaAlgebra.{u_1}
  (α : Type u_1) [TopologicalSpace α] :
  MeasurableSpace α

Definition body

abbrev borelSigmaAlgebra (α : Type*) [TopologicalSpace α] : MeasurableSpace α :=
  borel α

The Borel σ-algebra of a topological space.

Proposition6.6.2

uses 0used by 0XL∃∀N

Tagsexample

\RR^d では，開集合，閉集合，開集合の可算共通部分，閉集合の可算和はいずれもBorel集合である．また，有理端点をもつ有界開区間 \prod_{i=1}^d(a_i,b_i)，a_i,b_i\in\QQ，の全体は可算基底をなすので， \calB(\RR^d) はこの可算な集合族から生成される．

Theorem6.6.3

Statement uses 3

Statement dependency previews

Preview

Theorem 5.2.2.2

Loading preview

Statement dependency preview content is loaded from the Blueprint HTML cache.

used by 0✓L∃∀N

Tagsleanok

Borel集合はLebesgue可測. すべてのBorel集合 B\subset\RR^d はLebesgue可測である．

Lean code for Theorem6.6.3●1 theorem

theoremdefined in NoteKsk/«06caratheodory».lean

complete

theorem NoteKsk.Chapter06.borelSet_lebesgueMeasurable {d : ℕ}
  {A : Set (NoteKsk.Space d)} (hA : MeasurableSet A) :
  NoteKsk.Chapter05.LebesgueMeasurableSet A

theorem NoteKsk.Chapter06.borelSet_lebesgueMeasurable
  {d : ℕ} {A : Set (NoteKsk.Space d)}
  (hA : MeasurableSet A) :
  NoteKsk.Chapter05.LebesgueMeasurableSet
    A

Borel sets in Euclidean space are Lebesgue measurable.

Proof for Theorem 6.6.3

uses 0

Theorem 5.2.2.4により開集合はLebesgue可測である．また Theorem 5.2.2.2 により Lebesgue可測集合全体 \calL_d は \sigma-加法族である．したがって開集合が生成する \calB(\RR^d) は \calL_d に含まれる．

Definition6.6.4

Statement uses 2

Statement dependency previews

Preview

Definition 6.2.4

Loading preview

Statement dependency preview content is loaded from the Blueprint HTML cache.

used by 1✓L∃∀N

Tagsleanok

Borel測度. 本章では，Lebesgue測度をBorel集合族に制限した測度 \lambda|_{\calB(\RR^d)} を \RR^d 上のBorel測度という．

Lean code for Definition6.6.4●1 definition

abbrevdefined in NoteKsk/«06caratheodory».lean

complete

abbrev NoteKsk.Chapter06.borelMeasure (d : ℕ) :
  MeasureTheory.Measure (NoteKsk.Space d)

abbrev NoteKsk.Chapter06.borelMeasure (d : ℕ) :
  MeasureTheory.Measure (NoteKsk.Space d)

Definition body

abbrev borelMeasure (d : ℕ) : Measure (Space d) :=
  volume

The Borel measure on `ℝ^d`.

Mathlib's `volume` is used here.  Lebesgue measurable sets are represented in
Chapter 05 by `NullMeasurableSet A volume`, i.e. by the completion of this
Borel measure.

Theorem6.6.5

Statement uses 3

Statement dependency previews

Preview

Theorem 5.3.10

Loading preview

Statement dependency preview content is loaded from the Blueprint HTML cache.

used by 0✓L∃∀N

Tagsleanok

Lebesgue測度の構造定理（Borel測度の完備化）. 次が成り立つ．

任意のLebesgue可測集合 A\subset\RR^d は，あるBorel集合 B とあるLebesgue零集合 N を用いて A=B\triangle N と書ける．
Lebesgue測度は，Borel測度の完備化である．

Lean code for Theorem6.6.5●3 theorems

theoremdefined in NoteKsk/«06caratheodory».lean

complete

theorem NoteKsk.Chapter06.lebesgueMeasure_completion_of_borel {d : ℕ}
  {A : Set (NoteKsk.Space d)} :
  NoteKsk.Chapter05.LebesgueMeasurableSet A ↔
    NoteKsk.CompletedMeasurableSet (NoteKsk.Chapter06.borelMeasure d) A

theorem NoteKsk.Chapter06.lebesgueMeasure_completion_of_borel
  {d : ℕ} {A : Set (NoteKsk.Space d)} :
  NoteKsk.Chapter05.LebesgueMeasurableSet
      A ↔
    NoteKsk.CompletedMeasurableSet
      (NoteKsk.Chapter06.borelMeasure d) A

theoremdefined in NoteKsk/«06caratheodory».lean

complete

theorem NoteKsk.Chapter06.lebesgueMeasurable_exists_borel_ae_eq {d : ℕ}
  {A : Set (NoteKsk.Space d)}
  (hA : NoteKsk.Chapter05.LebesgueMeasurableSet A) :
  ∃ B, MeasurableSet B ∧ B =ᵐ[MeasureTheory.volume] A

theorem NoteKsk.Chapter06.lebesgueMeasurable_exists_borel_ae_eq
  {d : ℕ} {A : Set (NoteKsk.Space d)}
  (hA :
    NoteKsk.Chapter05.LebesgueMeasurableSet
      A) :
  ∃ B,
    MeasurableSet B ∧
      B =ᵐ[MeasureTheory.volume] A

theoremdefined in NoteKsk/«06caratheodory».lean

complete

theorem NoteKsk.Chapter06.lebesgueMeasurable_exists_borel_symmDiff_null {d : ℕ}
  {A : Set (NoteKsk.Space d)}
  (hA : NoteKsk.Chapter05.LebesgueMeasurableSet A) :
  ∃ B, MeasurableSet B ∧ NoteKsk.Chapter03.lambdaStar (symmDiff A B) = 0

theorem NoteKsk.Chapter06.lebesgueMeasurable_exists_borel_symmDiff_null
  {d : ℕ} {A : Set (NoteKsk.Space d)}
  (hA :
    NoteKsk.Chapter05.LebesgueMeasurableSet
      A) :
  ∃ B,
    MeasurableSet B ∧
      NoteKsk.Chapter03.lambdaStar
          (symmDiff A B) =
        0

Proof for Theorem 6.6.5

uses 0

まず \lambda(A)<\infty の場合を示す． Theorem 5.3.10と有限加法性により，各 n で A\subset O_n かつ \lambda(O_n\setminus A)<1/n となる開集合 O_n が取れる． B:=\bigcap_n O_n とおくと B はBorel集合で，A\subset B，かつ B\setminus A\subset O_n\setminus A がすべての n で成り立つので \lambda(B\setminus A)=0 である．一般の場合は Q_m:=(-m,m]^d とし，有限測度集合 A\cap Q_m に上の議論を適用して， Borel集合 B_m で A\cap Q_m\subset B_m\subset Q_m かつ \lambda(B_m\setminus A)=0 となるものを取る． B:=\bigcup_m B_m とすれば B はBorel集合，A\subset B， B\setminus A は零集合である． N:=B\setminus A とおけば A=B\triangle N であり，これは Definition 6.3.4の意味でBorel測度を完備化している．なお任意のLebesgue零集合は，外正則性によりBorel零集合に含まれる．