6.2. 可測空間と測度🔗

Definition6.2.1

uses 0

Used by 2

Reverse dependency previews

Preview

Definition 6.2.2

Loading preview

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

✓L∃∀N

Tagsmathlibok

\sigma-加法族. 集合 X の部分集合族 \calS\subset\calP(X) が X 上の \sigma-加法族であるとは，次を満たすことをいう．

X\in\calS．
A\in\calS ならば X\setminus A\in\calS．
\{A_n\}_{n=1}^{\infty}\subset\calS ならば \bigcup_{n=1}^{\infty}A_n\in\calS．

Lean code for Definition6.2.1●6 declarations

class(4 methods)defined in Mathlib/MeasureTheory/MeasurableSpace/Defs.lean

complete

class MeasurableSpace.{u_7} (α : Type u_7) : Type u_7

class MeasurableSpace.{u_7} (α : Type u_7) :
  Type u_7

A measurable space is a space equipped with a σ-algebra.

Methods

MeasurableSet' : Set α → Prop

Predicate saying that a given set is measurable. Use `MeasurableSet` in the root namespace
instead.

measurableSet_empty : MeasurableSpace.MeasurableSet' self ∅

The empty set is a measurable set. Use `MeasurableSet.empty` instead.

measurableSet_compl : ∀ (s : Set α), MeasurableSpace.MeasurableSet' self s → MeasurableSpace.MeasurableSet' self sᶜ

The complement of a measurable set is a measurable set. Use `MeasurableSet.compl` instead.

measurableSet_iUnion : ∀ (f : ℕ → Set α),
  (∀ (i : ℕ), MeasurableSpace.MeasurableSet' self (f i)) → MeasurableSpace.MeasurableSet' self (⋃ i, f i)

The union of a sequence of measurable sets is a measurable set. Use a more general
`MeasurableSet.iUnion` instead.

abbrevdefined in NoteKsk/Defs.lean

complete

abbrev NoteKsk.SigmaAlgebra.{u_1} (α : Type u_1) : Type u_1

abbrev NoteKsk.SigmaAlgebra.{u_1}
  (α : Type u_1) : Type u_1

Definition body

abbrev SigmaAlgebra (α : Type*) : Type _ :=
  MeasurableSpace α

A σ-algebra on a type.  This is only a lecture-note synonym for mathlib's
`MeasurableSpace`.

theoremdefined in NoteKsk/«06caratheodory».lean

complete

theorem NoteKsk.Chapter06.sigmaAlgebra_empty_mem.{u_1} {α : Type u_1}
  [MeasurableSpace α] : MeasurableSet ∅

theorem NoteKsk.Chapter06.sigmaAlgebra_empty_mem.{u_1}
  {α : Type u_1} [MeasurableSpace α] :
  MeasurableSet ∅

theoremdefined in NoteKsk/«06caratheodory».lean

complete

theorem NoteKsk.Chapter06.sigmaAlgebra_univ_mem.{u_1} {α : Type u_1}
  [MeasurableSpace α] : MeasurableSet Set.univ

theorem NoteKsk.Chapter06.sigmaAlgebra_univ_mem.{u_1}
  {α : Type u_1} [MeasurableSpace α] :
  MeasurableSet Set.univ

theoremdefined in NoteKsk/«06caratheodory».lean

complete

theorem NoteKsk.Chapter06.sigmaAlgebra_compl_mem.{u_1} {α : Type u_1}
  [MeasurableSpace α] {A : Set α} (hA : MeasurableSet A) :
  MeasurableSet Aᶜ

theorem NoteKsk.Chapter06.sigmaAlgebra_compl_mem.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {A : Set α} (hA : MeasurableSet A) :
  MeasurableSet Aᶜ

theoremdefined in NoteKsk/«06caratheodory».lean

complete

theorem NoteKsk.Chapter06.sigmaAlgebra_iUnion_mem.{u_1} {α : Type u_1}
  [MeasurableSpace α] (A : ℕ → Set α)
  (hA : ∀ (n : ℕ), MeasurableSet (A n)) : MeasurableSet (⋃ n, A n)

theorem NoteKsk.Chapter06.sigmaAlgebra_iUnion_mem.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  (A : ℕ → Set α)
  (hA : ∀ (n : ℕ), MeasurableSet (A n)) :
  MeasurableSet (⋃ n, A n)

Remark. \sigma-加法族は，補集合と可算和を取っても外へ出ない集合族である．したがって可算共通部分や差集合についても閉じている．

Definition6.2.2

uses 1

Used by 2

Reverse dependency previews

Preview

Theorem 6.4.7

Loading preview

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

✓L∃∀N

Tagsleanok

集合系が生成する \sigma-加法族. 任意の集合族 \calC\subset\calP(X) に対し， \calC を含む最小の \sigma-加法族を \sigma(\calC) と書き， \calC が生成する \sigma-加法族という．具体的には，\calC を含むすべての \sigma-加法族の共通部分である．

Lean code for Definition6.2.2●3 declarations

abbrevdefined in NoteKsk/Defs.lean

complete

abbrev NoteKsk.generatedSigmaAlgebra.{u_1} {α : Type u_1} (C : Set (Set α)) :
  MeasurableSpace α

abbrev NoteKsk.generatedSigmaAlgebra.{u_1}
  {α : Type u_1} (C : Set (Set α)) :
  MeasurableSpace α

Definition body

abbrev generatedSigmaAlgebra {α : Type*} (C : Set (Set α)) : MeasurableSpace α :=
  MeasurableSpace.generateFrom C

/-! ## Measurable maps and measurable functions -/

The σ-algebra generated by a family of subsets.

theoremdefined in NoteKsk/«06caratheodory».lean

complete

theorem NoteKsk.Chapter06.generatedSigmaAlgebra_contains.{u_1} {α : Type u_1}
  {C : Set (Set α)} {s : Set α} (hs : s ∈ C) : MeasurableSet s

theorem NoteKsk.Chapter06.generatedSigmaAlgebra_contains.{u_1}
  {α : Type u_1} {C : Set (Set α)}
  {s : Set α} (hs : s ∈ C) :
  MeasurableSet s

Members of the generated σ-algebra contain the original generating family.

theoremdefined in NoteKsk/«06caratheodory».lean

complete

theorem NoteKsk.Chapter06.generatedSigmaAlgebra_minimal.{u_1} {α : Type u_1}
  {C : Set (Set α)} {m : MeasurableSpace α}
  (hC : ∀ s ∈ C, MeasurableSet s) : NoteKsk.generatedSigmaAlgebra C ≤ m

theorem NoteKsk.Chapter06.generatedSigmaAlgebra_minimal.{u_1}
  {α : Type u_1} {C : Set (Set α)}
  {m : MeasurableSpace α}
  (hC : ∀ s ∈ C, MeasurableSet s) :
  NoteKsk.generatedSigmaAlgebra C ≤ m

The generated σ-algebra is the smallest σ-algebra containing the given family.

Definition6.2.3

uses 0used by 0XL∃∀N

可測空間. X 上の \sigma-加法族 \calS を1つ固定した組 (X,\calS) を可測空間という．

Definition6.2.4

uses 1

Used by 6

Reverse dependency previews

Preview

Definition 6.2.6

Loading preview

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

✓L∃∀N

Tagsmathlibok

測度. 可測空間 (X,\calS) 上の写像 \mu:\calS\to[0,\infty] が測度であるとは，次を満たすことをいう．

\mu(\emptyset)=0．
互いに素な列 \{A_n\}_{n=1}^{\infty}\subset\calS に対して \mu(\bigsqcup_{n=1}^{\infty}A_n)=\sum_{n=1}^{\infty}\mu(A_n) が成り立つ．

Lean code for Definition6.2.4●3 declarations

structure(extends 1, 6 fields)defined in Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

complete

structure MeasureTheory.Measure.{u_6} (α : Type u_6) [MeasurableSpace α] :
  Type u_6

structure MeasureTheory.Measure.{u_6} (α : Type u_6)
  [MeasurableSpace α] : Type u_6

A measure is defined to be an outer measure that is countably additive on
measurable sets, with the additional assumption that the outer measure is the canonical
extension of the restricted measure.

The measure of a set `s`, denoted `μ s`, is an extended nonnegative real. The real-valued version
is written `μ.real s`.

Extends

MeasureTheory.OuterMeasure α

Fields

measureOf : Set α → ENNReal

Inherited from

MeasureTheory.OuterMeasure

empty : self.measureOf ∅ = 0

Inherited from

MeasureTheory.OuterMeasure

mono : ∀ {s₁ s₂ : Set α}, s₁ ⊆ s₂ → self.measureOf s₁ ≤ self.measureOf s₂

Inherited from

MeasureTheory.OuterMeasure

iUnion_nat : ∀ (s : ℕ → Set α), Pairwise (Function.onFun Disjoint s) → self.measureOf (⋃ i, s i) ≤ ∑' (i : ℕ), self.measureOf (s i)

Inherited from

MeasureTheory.OuterMeasure

m_iUnion : ∀ ⦃f : ℕ → Set α⦄,
  (∀ (i : ℕ), MeasurableSet (f i)) →
    Pairwise (Function.onFun Disjoint f) → self.toOuterMeasure (⋃ i, f i) = ∑' (i : ℕ), self.toOuterMeasure (f i)

trim_le : self.trim ≤ self.toOuterMeasure

theoremdefined in NoteKsk/«06caratheodory».lean

complete

theorem NoteKsk.Chapter06.measure_empty.{u_1} {α : Type u_1} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α) : μ ∅ = 0

theorem NoteKsk.Chapter06.measure_empty.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α) : μ ∅ = 0

theoremdefined in NoteKsk/«06caratheodory».lean

complete

theorem NoteKsk.Chapter06.measure_iUnion_disjoint.{u_1} {α : Type u_1}
  [MeasurableSpace α] (μ : MeasureTheory.Measure α) (A : ℕ → Set α)
  (hA : ∀ (n : ℕ), MeasurableSet (A n))
  (hdisj : Pairwise (Function.onFun Disjoint A)) :
  μ (⋃ n, A n) = ∑' (n : ℕ), μ (A n)

theorem NoteKsk.Chapter06.measure_iUnion_disjoint.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  (A : ℕ → Set α)
  (hA : ∀ (n : ℕ), MeasurableSet (A n))
  (hdisj :
    Pairwise
      (Function.onFun Disjoint A)) :
  μ (⋃ n, A n) = ∑' (n : ℕ), μ (A n)

Definition6.2.5

uses 0used by 0XL∃∀N

測度空間. 可測空間 (X,\calS) とその上の測度 \mu の組 (X,\calS,\mu) を測度空間という．

Definition6.2.6

uses 1used by 1✓L∃∀N

Tagsmathlibok

\sigma-有限測度. 測度 \mu が \sigma-有限であるとは，ある列 \{X_n\}_{n=1}^{\infty}\subset\calS が存在して，次を満たすことをいう．

X=\bigcup_{n=1}^{\infty}X_n．
すべての n について \mu(X_n)<\infty．

同じ言葉を有限加法族上の前測度に対して使うときも，被覆集合 X_n はその有限加法族の元とする．

Lean code for Definition6.2.6●3 declarations

class(1 method)defined in Mathlib/MeasureTheory/Measure/Typeclasses/SFinite.lean

complete

class MeasureTheory.SigmaFinite.{u_1} {α : Type u_1} {m0 : MeasurableSpace α}
  (μ : MeasureTheory.Measure α) : Prop

class MeasureTheory.SigmaFinite.{u_1}
  {α : Type u_1} {m0 : MeasurableSpace α}
  (μ : MeasureTheory.Measure α) : Prop

A measure `μ` is called σ-finite if there is a countable collection of sets
`{ A i | i ∈ ℕ }` such that `μ (A i) < ∞` and `⋃ i, A i = s`.

Methods

out' : Nonempty (μ.FiniteSpanningSetsIn Set.univ)

class(1 method)defined in Mathlib/MeasureTheory/Measure/Typeclasses/SFinite.lean

complete

class MeasureTheory.SFinite.{u_1} {α : Type u_1} {m0 : MeasurableSpace α}
  (μ : MeasureTheory.Measure α) : Prop

class MeasureTheory.SFinite.{u_1} {α : Type u_1}
  {m0 : MeasurableSpace α}
  (μ : MeasureTheory.Measure α) : Prop

A measure is called s-finite if it is a countable sum of finite measures.

Methods

out' : ∃ m, (∀ (n : ℕ), MeasureTheory.IsFiniteMeasure (m n)) ∧ μ = MeasureTheory.Measure.sum m

theoremdefined in NoteKsk/«06caratheodory».lean

complete

theorem NoteKsk.Chapter06.sigmaFinite_iff_exists_measurable_finite_spanning.{u_1}
  {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) :
  MeasureTheory.SigmaFinite μ ↔
    ∃ S,
      (∀ (n : ℕ), MeasurableSet (S n)) ∧
        (∀ (n : ℕ), μ (S n) < ⊤) ∧ ⋃ n, S n = Set.univ

theorem NoteKsk.Chapter06.sigmaFinite_iff_exists_measurable_finite_spanning.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α) :
  MeasureTheory.SigmaFinite μ ↔
    ∃ S,
      (∀ (n : ℕ), MeasurableSet (S n)) ∧
        (∀ (n : ℕ), μ (S n) < ⊤) ∧
          ⋃ n, S n = Set.univ

σ-finiteness, stated as the usual measurable countable exhaustion.

Proposition6.2.7

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 0✓L∃∀N

Tagsleanokexample

数え上げ測度. 任意の集合 X について \calP(X) 上で \#A を A の元の個数，ただし無限集合なら \#A=\infty，と定めると測度になる．これを数え上げ測度（計数測度，個数測度）という． X が可算集合なら一点集合の可算和で覆えるので \sigma-有限であり， X が非可算集合なら \sigma-有限ではない．

Lean code for Proposition6.2.7●1 theorem

theoremdefined in NoteKsk/«06caratheodory».lean

complete

theorem NoteKsk.Chapter06.countingMeasure_apply.{u_1} {α : Type u_1}
  [MeasurableSpace α] {A : Set α} (hA : MeasurableSet A) :
  MeasureTheory.Measure.count A = ↑A.encard

theorem NoteKsk.Chapter06.countingMeasure_apply.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {A : Set α} (hA : MeasurableSet A) :
  MeasureTheory.Measure.count A =
    ↑A.encard

Counting measure assigns the cardinality to a measurable set.

Proposition6.2.8

uses 1used by 0✓L∃∀N

Tagsleanokexample

Dirac測度. 可測空間 (X,\calS) と点 a\in X に対し， \delta_a(A)=1（a\in A のとき），\delta_a(A)=0（a\notin A のとき）と定める．これは (X,\calS) 上の測度であり，点 a に質量が集中したDirac測度という．

Lean code for Proposition6.2.8●1 theorem

theoremdefined in NoteKsk/«06caratheodory».lean

complete

theorem NoteKsk.Chapter06.diracMeasure_apply.{u_1} {α : Type u_1}
  [MeasurableSpace α] [MeasurableSingletonClass α] (a : α) (A : Set α) :
  (MeasureTheory.Measure.dirac a) A = A.indicator (fun x ↦ 1) a

theorem NoteKsk.Chapter06.diracMeasure_apply.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  [MeasurableSingletonClass α] (a : α)
  (A : Set α) :
  (MeasureTheory.Measure.dirac a) A =
    A.indicator (fun x ↦ 1) a

Dirac measure, in the mathlib form using `indicator`.