2.4. Jordan零集合🔗

Definition2.4.1

uses 1

Used by 4

Reverse dependency previews

Preview

Proposition 2.4.2

Loading preview

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

✓L∃∀N

Tagsleanok

Jordan零集合. m_J^*(N)=0 を満たす集合 N をJordan零集合という．

Lean code for Definition2.4.1●2 declarations

defdefined in NoteKsk/Defs.lean

complete

def NoteKsk.JordanNullSet {d : ℕ} (A : Set (NoteKsk.Space d)) : Prop

def NoteKsk.JordanNullSet {d : ℕ}
  (A : Set (NoteKsk.Space d)) : Prop

Definition body

def JordanNullSet {d : ℕ} (A : Set (Space d)) : Prop :=
  jordanOuterMeasure A = 0

/-! ## Finite additive families -/

Jordan null sets.

theoremdefined in NoteKsk/«02jordan».lean

complete

theorem NoteKsk.Chapter02.jordanMeasure_eq_zero_of_null {d : ℕ}
  {N : Set (NoteKsk.Space d)} (hN : NoteKsk.JordanNullSet N) :
  NoteKsk.jordanMeasure N = 0

theorem NoteKsk.Chapter02.jordanMeasure_eq_zero_of_null
  {d : ℕ} {N : Set (NoteKsk.Space d)}
  (hN : NoteKsk.JordanNullSet N) :
  NoteKsk.jordanMeasure N = 0

Proposition2.4.2

Statement uses 2

Statement dependency previews

Preview

Definition 2.3.3

Loading preview

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

used by 0!L∃∀N

Tagsnotready

Jordan零集合はJordan可測である．

Lean code for Proposition2.4.2●1 declaration, 1 missing

NoteKsk.Chapter02.jordanNullSet_jordanMeasurablemissing declaration

declaration not found (name was not present during directive/code-block registration)

Proof for Proposition 2.4.2

uses 0

実際，

0 \le m_{J,*}(N) \le m_J^*(N)=0

だから m_{J,*}(N)=m_J^*(N)=0 である．

Proposition2.4.3

uses 1used by 1!L∃∀N

Tagsnotreadyexample

1点集合はJordan零集合である．

Lean code for Proposition2.4.3●1 declaration, 1 missing

NoteKsk.Chapter02.jordanNullSet_singletonmissing declaration

declaration not found (name was not present during directive/code-block registration)

Proof for Proposition 2.4.3

uses 0

x \in \RR^d を固定する． \eps > 0に対し， 1点集合 \{ x \} は，x を中心とする幅 2 \eps の区間 Q_\eps で覆える：

\{ x \} \subset Q_\eps := \prod_{i=1}^d (x_i - \eps, x_i+\eps].

よって

m_J^*(\{x\}) \le |Q_\eps| = (2 \eps)^d

\eps>0 は任意なので \eps \to 0 として m_J^*(\{x\}) = 0.

Proposition2.4.4

uses 1used by 0!L∃∀N

Tagsnotreadyexample

有限集合はJordan零集合である

Lean code for Proposition2.4.4●1 declaration, 1 missing

NoteKsk.Chapter02.jordanNullSet_finitemissing declaration

declaration not found (name was not present during directive/code-block registration)

Proof for Proposition 2.4.4

uses 0

有限集合は1点集合の有限合併なので， 1点集合の場合と同様にして，十分小さい区間で覆えるのでJordan零である．

Proposition2.4.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 1!L∃∀N

Tagsnotreadyexample

有界基本集合 E \subset \RR^d の境界 \partial E はJordan零集合である．

Lean code for Proposition2.4.5●1 declaration, 1 missing

NoteKsk.Chapter02.jordanNullSet_boundary_elementarymissing declaration

declaration not found (name was not present during directive/code-block registration)

Proof for Proposition 2.4.5

uses 0

有界基本集合 E を

E=\bigsqcup_{j=1}^m Q_j, \qquad Q_j=\prod_{k=1}^d (a_{j,k},b_{j,k}]

と書く．各 Q_j の境界 \partial Q_j は，各座標について端点を1つ固定して得られる有限個の超平面片の合併であるからJordan零集合である．したがって

\partial E \subset \bigcup_{j=1}^m \partial Q_j

より，\partial E もJordan零集合である．

Proposition2.4.6

uses 0used by 0XL∃∀N

Tagsexample

線分や超平面片など，\RR^d の中で厚みをもたない典型的な図形はJordan零集合である

Proof for Proposition 2.4.6

uses 0

例えば超平面片 \{x_d=0\} \cap [-M,M]^d は厚さ \delta の板

[-M,M]^{d-1} \times [-\delta,\delta]

で覆えるのでJordan零である．線分も同様に細い区間で覆える