6.4. 半加法族と前測度🔗

Definition6.4.1

uses 0

Used by 4

Reverse dependency previews

Preview

Proposition 6.4.2

Loading preview

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

✓L∃∀N

Tagsmathlibok

半加法族. 集合 X の部分集合族 \calE\subset\calP(X) が半加法族（半環）であるとは，次を満たすことをいう．

\emptyset\in\calE．
A,B\in\calE ならば A\cap B\in\calE．
A,B\in\calE ならば A\setminus B が有限個の互いに素な \calE の元の合併として書ける．

ここで有限個は 0 個でもよい．

Lean code for Definition6.4.1●1 definition

structure(3 fields)defined in Mathlib/MeasureTheory/SetSemiring.lean

complete

structure MeasureTheory.IsSetSemiring.{u_1} {α : Type u_1} (C : Set (Set α)) :
  Prop

structure MeasureTheory.IsSetSemiring.{u_1}
  {α : Type u_1} (C : Set (Set α)) : Prop

A semi-ring of sets `C` is a family of sets containing `∅`, stable by intersection and such that
for all `s, t ∈ C`, `s \ t` is equal to a disjoint union of finitely many sets in `C`.

Fields

empty_mem : ∅ ∈ C

inter_mem : ∀ s ∈ C, ∀ t ∈ C, s ∩ t ∈ C

diff_eq_sUnion' : ∀ s ∈ C, ∀ t ∈ C, ∃ I, ↑I ⊆ C ∧ (↑I).PairwiseDisjoint id ∧ s \ t = ⋃₀ ↑I

Remark. X\in\calE であっても，半加法族 \calE は一般には有限加法族ではない．半加法族の定義で要求するのは，差集合が有限個の \calE の元の合併に分解できることまでであり，その有限合併自体が再び \calE に属するとは限らないからである．

Proposition6.4.2

uses 1used by 1✓L∃∀N

Tagsleanokexample

左半開区間の半加法族. \RR^d では

\calE_d := \left\{ \prod_{i=1}^{d}(a_i,b_i] \;\middle|\; -\infty\le a_i<b_i\le\infty \right\} \cup\{\emptyset\}

を用いる．端点が \pm\infty のときは自然な意味で解釈する．共通部分は再び左半開区間であり，差集合は有限個の互いに素な左半開区間に分割できるので， \calE_d は半加法族である．これまで基本集合と呼んできた族は \calA(\calE_d) である．

Lean code for Proposition6.4.2●1 theorem

theoremdefined in NoteKsk/«06caratheodory».lean

complete

theorem NoteKsk.Chapter06.leftHalfOpenBox_isSetSemiring {d : ℕ} :
  MeasureTheory.IsSetSemiring {S | NoteKsk.IsLeftHalfOpenBox S}

theorem NoteKsk.Chapter06.leftHalfOpenBox_isSetSemiring
  {d : ℕ} :
  MeasureTheory.IsSetSemiring
    {S | NoteKsk.IsLeftHalfOpenBox S}

The left half-open boxes from the earlier chapters form a semiring.

Proposition6.4.3

uses 0used by 0XL∃∀N

Tagsexample

有限分割の半加法族. X の有限分割

X=P_1\sqcup\cdots\sqcup P_m

を固定する．このとき

\calE_{\Pi}:=\{\emptyset,P_1,\ldots,P_m\}

は半加法族である．実際，異なるブロックは互いに素であり，各ブロック同士の共通部分や差集合はブロックそのものか空集合になる．ただし，m\ge 2 なら P_1\cup P_2 はふつう \calE_{\Pi} に入らないので， \calE_{\Pi} は一般には有限加法族ではない．生成される有限加法族 \calA(\calE_{\Pi}) は，分割のブロックの合併全体である．

Proposition6.4.4

uses 1used by 1✓L∃∀N

Tagsleanokexample

離散的な半加法族. 任意の集合 X に対し，冪集合 \calP(X) は半加法族である．また，有限集合全体

\calF(X):=\{F\subset X\mid F\text{ は有限集合}\}

も半加法族である．特に，X が有限集合なら \calF(X)=\calP(X) である．これらは数え上げ測度，有限集合上の確率測度，Dirac測度を構成するときの自然な出発点になる．

Lean code for Proposition6.4.4●1 theorem

theoremdefined in NoteKsk/«06caratheodory».lean

complete

theorem NoteKsk.Chapter06.powerset_isSetSemiring.{u_1} {α : Type u_1} :
  MeasureTheory.IsSetSemiring Set.univ

theorem NoteKsk.Chapter06.powerset_isSetSemiring.{u_1}
  {α : Type u_1} :
  MeasureTheory.IsSetSemiring Set.univ

The whole powerset is a semiring of sets.

Definition6.4.5

uses 0

Used by 2

Reverse dependency previews

Preview

Definition 6.4.6

Loading preview

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

✓L∃∀N

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

\emptyset\in\calA．
A,B\in\calA ならば A\cup B\in\calA．
A\in\calA ならば A^c\in\calA．

Lean code for Definition6.4.5●2 definitions

defdefined in NoteKsk/Defs.lean

complete

def NoteKsk.FiniteAdditiveFamily.{u_1} {α : Type u_1} (𝓕 : Set (Set α)) :
  Prop

def NoteKsk.FiniteAdditiveFamily.{u_1}
  {α : Type u_1} (𝓕 : Set (Set α)) : Prop

Definition body

def FiniteAdditiveFamily {α : Type*} (𝓕 : Set (Set α)) : Prop :=
  (∅ : Set α) ∈ 𝓕 ∧
    (∀ A, A ∈ 𝓕 → Aᶜ ∈ 𝓕) ∧
    (∀ A B, A ∈ 𝓕 → B ∈ 𝓕 → A ∪ B ∈ 𝓕)

/-! ## Abstract measure-theory vocabulary -/

A finite additive family of subsets.

structure(3 fields)defined in Mathlib/MeasureTheory/SetSemiring.lean

complete

structure MeasureTheory.IsSetRing.{u_1} {α : Type u_1} (C : Set (Set α)) : Prop

structure MeasureTheory.IsSetRing.{u_1}
  {α : Type u_1} (C : Set (Set α)) : Prop

A ring of sets `C` is a family of sets containing `∅`, stable by union and set difference.
It is then also stable by intersection (see `IsSetRing.inter_mem`).

Fields

empty_mem : ∅ ∈ C

union_mem : ∀ ⦃s t : Set α⦄, s ∈ C → t ∈ C → s ∪ t ∈ C

diff_mem : ∀ ⦃s t : Set α⦄, s ∈ C → t ∈ C → s \ t ∈ C

Definition6.4.6

Statement uses 2

Statement dependency previews

Preview

Definition 6.4.1

Loading preview

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

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

半加法族が生成する有限加法族. 半加法族 \calE に対して

\calA(\calE) := \left\{ \bigsqcup_{j=1}^{N}E_j \;\middle|\; N\in\NN,\ E_j\in\calE \right\}

と定める．半加法族は \emptyset を含むので，\calA(\calE) も \emptyset を含んでいる．

Lean code for Definition6.4.6●1 definition

abbrevdefined in NoteKsk/Defs.lean

complete

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

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

Definition body

abbrev algebraGeneratedBySemiring {α : Type*} (C : Set (Set α)) : Set (Set α) :=
  supClosure C

The finite additive family generated by a semiring of sets.

Mathlib represents this as `supClosure C`, the family of finite unions of
members of `C`.

Theorem6.4.7

Statement uses 2

Statement dependency previews

Preview

Definition 6.2.2

Loading preview

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

used by 0✓L∃∀N

Tagsleanok

\calA(\calE) は X 上の有限加法族である．

Lean code for Theorem6.4.7●2 theorems

theoremdefined in NoteKsk/«06caratheodory».lean

complete

theorem NoteKsk.Chapter06.algebraGeneratedBySemiring_isSetRing.{u_1}
  {α : Type u_1} {C : Set (Set α)}
  (hC : MeasureTheory.IsSetSemiring C) :
  MeasureTheory.IsSetRing (NoteKsk.algebraGeneratedBySemiring C)

theorem NoteKsk.Chapter06.algebraGeneratedBySemiring_isSetRing.{u_1}
  {α : Type u_1} {C : Set (Set α)}
  (hC : MeasureTheory.IsSetSemiring C) :
  MeasureTheory.IsSetRing
    (NoteKsk.algebraGeneratedBySemiring C)

A semiring generates a ring of sets by finite unions.

theoremdefined in NoteKsk/«06caratheodory».lean

complete

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

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

Finite unions of generators are measurable in the generated σ-algebra.

Proof for Theorem 6.4.7

uses 0

まず C\in\calE と F\in\calA(\calE) に対して， C\setminus F は有限個の互いに素な \calE の元の合併になる．これは F の表示に現れる項数に関する帰納法と，半加法族の差集合条件から従う．したがって E=\bigsqcup_i E_i と F\in\calA(\calE) なら E\setminus F=\bigsqcup_i(E_i\setminus F) も \calA(\calE) に属する．また E\cup F=E\sqcup(F\setminus E) だから有限和でも閉じており， \emptyset は \calE に属するので \calA(\calE) にも属する．

Definition6.4.8

uses 1

Used by 4

Reverse dependency previews

Preview

Proposition 6.4.9

Loading preview

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

✓L∃∀N

Tagsmathlibok

半加法族上の前測度. 半加法族 \calE 上の写像 \mu_0:\calE\to[0,\infty] が前測度であるとは，次を満たすことをいう．

\mu_0(\emptyset)=0．
互いに素な列 \{E_n\}_{n=1}^{\infty}\subset\calE が E=\bigsqcup_{n=1}^{\infty}E_n\in\calE を満たすとき \mu_0(E)=\sum_{n=1}^{\infty}\mu_0(E_n) となる．

半加法族上の前測度を体積と呼ぶこともある．有限個の分割については，残りを空集合とすれば同じ等式が成り立つ．

Lean code for Definition6.4.8●2 definitions

structure(3 fields)defined in Mathlib/MeasureTheory/Measure/AddContent.lean

complete

structure MeasureTheory.AddContent.{u_1, u_2} {α : Type u_1} (G : Type u_2)
  [AddCommMonoid G] (C : Set (Set α)) : Type (max u_1 u_2)

structure MeasureTheory.AddContent.{u_1, u_2}
  {α : Type u_1} (G : Type u_2)
  [AddCommMonoid G] (C : Set (Set α)) :
  Type (max u_1 u_2)

An additive content is a set function with value 0 at the empty set which is finitely additive
on a given set of sets.

Fields

toFun : Set α → G

The value of the content on a set.

empty' : self.toFun ∅ = 0

sUnion' : ∀ (I : Finset (Set α)), ↑I ⊆ C → (↑I).PairwiseDisjoint id → ⋃₀ ↑I ∈ C → self.toFun (⋃₀ ↑I) = ∑ u ∈ I, self.toFun u

defdefined in NoteKsk/Defs.lean

complete

def NoteKsk.IsPremeasureOnSemiring.{u_1} {α : Type u_1} {C : Set (Set α)}
  (m : MeasureTheory.AddContent ENNReal C) : Prop

def NoteKsk.IsPremeasureOnSemiring.{u_1}
  {α : Type u_1} {C : Set (Set α)}
  (m :
    MeasureTheory.AddContent ENNReal C) :
  Prop

Definition body

def IsPremeasureOnSemiring {α : Type*} {C : Set (Set α)}
    (m : AddContent ENNReal C) : Prop :=
  m.IsSigmaSubadditive

A premeasure on a semiring, in the sense needed for the Carathéodory--Hahn
extension theorem: an additive content with countable subadditivity.

Remark. 可算加法性は後の拡張定理において本質的な条件であるため，有限加法性だけでなく，前測度の定義の時点で含めておくことが多い．

Remark (用語の使い分け). 本章では，前測度を半加法族 \calE から有限加法族 \calA(\calE) へ移すことを延長と呼ぶ．また，前測度から外測度を誘導することを誘導と呼び，得られた測度をより大きな \sigma-加法族上で考えることを拡張と呼ぶ．

Proposition6.4.9

Statement uses 2

Statement dependency previews

Preview

Proposition 6.4.4

Loading preview

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

used by 0XL∃∀N

Tagsexample

離散的な前測度. Proposition 6.4.4の \calP(X) 上では，次はいずれも半加法族上の前測度である．

\mu_0(A)=\#A と定めると，数え上げ測度の出発点になる．
X が有限集合で，p_x\ge 0，\sum_{x\in X}p_x=1 を満たす重みを固定し， \mu_0(A)=\sum_{x\in A}p_x と定めると，有限集合上の確率測度の出発点になる．
a\in X を固定し，\mu_0(A)=1（a\in A のとき）， \mu_0(A)=0（a\notin A のとき）と定めると，Dirac測度の出発点になる．

いずれも \sigma(\calP(X))=\calP(X) なので，拡張後の測度は同じ式で \calP(X) 上に定まる．

Definition6.4.10

Statement uses 2

Statement dependency previews

Preview

Definition 6.4.5

Loading preview

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

used by 1✓L∃∀N

Tagsmathlibok

有限加法族上の前測度. 有限加法族 \calA 上の写像 \mu_0:\calA\to[0,\infty] が前測度であるとは，次を満たすことをいう．

\mu_0(\emptyset)=0．
互いに素な列 \{A_n\}_{n=1}^{\infty}\subset\calA が \bigsqcup_{n=1}^{\infty} A_n\in\calA を満たすとき \mu_0(\bigsqcup_{n=1}^{\infty} A_n)=\sum_{n=1}^{\infty}\mu_0(A_n) となる．

Lean code for Definition6.4.10●2 definitions

structure(3 fields)defined in Mathlib/MeasureTheory/Measure/AddContent.lean

complete

structure MeasureTheory.AddContent.{u_1, u_2} {α : Type u_1} (G : Type u_2)
  [AddCommMonoid G] (C : Set (Set α)) : Type (max u_1 u_2)

structure MeasureTheory.AddContent.{u_1, u_2}
  {α : Type u_1} (G : Type u_2)
  [AddCommMonoid G] (C : Set (Set α)) :
  Type (max u_1 u_2)

An additive content is a set function with value 0 at the empty set which is finitely additive
on a given set of sets.

Fields

toFun : Set α → G

The value of the content on a set.

empty' : self.toFun ∅ = 0

sUnion' : ∀ (I : Finset (Set α)), ↑I ⊆ C → (↑I).PairwiseDisjoint id → ⋃₀ ↑I ∈ C → self.toFun (⋃₀ ↑I) = ∑ u ∈ I, self.toFun u

defdefined in NoteKsk/Defs.lean

complete

def NoteKsk.IsPremeasureOnSemiring.{u_1} {α : Type u_1} {C : Set (Set α)}
  (m : MeasureTheory.AddContent ENNReal C) : Prop

def NoteKsk.IsPremeasureOnSemiring.{u_1}
  {α : Type u_1} {C : Set (Set α)}
  (m :
    MeasureTheory.AddContent ENNReal C) :
  Prop

Definition body

def IsPremeasureOnSemiring {α : Type*} {C : Set (Set α)}
    (m : AddContent ENNReal C) : Prop :=
  m.IsSigmaSubadditive

A premeasure on a semiring, in the sense needed for the Carathéodory--Hahn
extension theorem: an additive content with countable subadditivity.

Remark. 有限加法性はこの定義から従う．実際，互いに素な有限列の後ろに空集合を並べれば，上の可算加法性を適用できる．したがって，A\subset B なら \mu_0(B)=\mu_0(A)+\mu_0(B\setminus A) となり，単調性も従う．

Theorem6.4.11

Statement uses 3

Statement dependency previews

Preview

Definition 6.4.6

Loading preview

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

Used by 2

Reverse dependency previews

Preview

Theorem 6.5.2

Loading preview

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

✓L∃∀N

Tagsleanok

有限加法族への延長. \mu_0 を半加法族 \calE 上の前測度とする． A=\bigsqcup_{j=1}^{N}E_j\in\calA(\calE) に対して \overline\mu_0(A):=\sum_{j=1}^{N}\mu_0(E_j) と定める．このとき次が成り立つ．

\overline\mu_0 は表示の取り方によらず定まる．
\overline\mu_0 は \calA(\calE) 上の前測度である．

Lean code for Theorem6.4.11●3 declarations

defdefined in NoteKsk/«06caratheodory».lean

complete

def NoteKsk.Chapter06.premeasureExtensionToAlgebra.{u_1} {α : Type u_1}
  {C : Set (Set α)} (hC : MeasureTheory.IsSetSemiring C)
  (m : MeasureTheory.AddContent ENNReal C) :
  MeasureTheory.AddContent ENNReal
    (NoteKsk.algebraGeneratedBySemiring C)

def NoteKsk.Chapter06.premeasureExtensionToAlgebra.{u_1}
  {α : Type u_1} {C : Set (Set α)}
  (hC : MeasureTheory.IsSetSemiring C)
  (m :
    MeasureTheory.AddContent ENNReal C) :
  MeasureTheory.AddContent ENNReal
    (NoteKsk.algebraGeneratedBySemiring C)

Definition body

noncomputable def premeasureExtensionToAlgebra (hC : IsSetSemiring C)
    (m : AddContent ENNReal C) :
    AddContent ENNReal (algebraGeneratedBySemiring C) :=
  m.supClosure hC

Extension of an additive content from a semiring to its finite-union algebra.

This is the theorem `thm:premeasure-extension-to-algebra` in mathlib's form:
`AddContent.supClosure`.

theoremdefined in NoteKsk/«06caratheodory».lean

complete

theorem NoteKsk.Chapter06.premeasureExtensionToAlgebra_eq_on_semiring.{u_1}
  {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.IsSetSemiring C)
  (m : MeasureTheory.AddContent ENNReal C) {s : Set α} (hs : s ∈ C) :
  (NoteKsk.Chapter06.premeasureExtensionToAlgebra hC m) s = m s

theorem NoteKsk.Chapter06.premeasureExtensionToAlgebra_eq_on_semiring.{u_1}
  {α : Type u_1} {C : Set (Set α)}
  (hC : MeasureTheory.IsSetSemiring C)
  (m : MeasureTheory.AddContent ENNReal C)
  {s : Set α} (hs : s ∈ C) :
  (NoteKsk.Chapter06.premeasureExtensionToAlgebra
        hC m)
      s =
    m s

theoremdefined in NoteKsk/«06caratheodory».lean

complete

theorem NoteKsk.Chapter06.premeasureExtensionToAlgebra_isPremeasure.{u_1}
  {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.IsSetSemiring C)
  (m : MeasureTheory.AddContent ENNReal C)
  (hm : NoteKsk.IsPremeasureOnSemiring m) :
  NoteKsk.IsPremeasureOnSemiring
    (NoteKsk.Chapter06.premeasureExtensionToAlgebra hC m)

theorem NoteKsk.Chapter06.premeasureExtensionToAlgebra_isPremeasure.{u_1}
  {α : Type u_1} {C : Set (Set α)}
  (hC : MeasureTheory.IsSetSemiring C)
  (m : MeasureTheory.AddContent ENNReal C)
  (hm :
    NoteKsk.IsPremeasureOnSemiring m) :
  NoteKsk.IsPremeasureOnSemiring
    (NoteKsk.Chapter06.premeasureExtensionToAlgebra
      hC m)

If the original content is a premeasure, then its finite-algebra extension is a
premeasure.

The proof compares `AddContent.supClosure` with the measure generated by `m`
on `generatedSigmaAlgebra C`; countable subadditivity then follows from the
outer-measure subadditivity of that generated measure.

Proof for Theorem 6.4.11

uses 0

A=\bigsqcup_i E_i=\bigsqcup_j F_j と2通りに表す．各 E_i は互いに素な有限和 E_i=\bigsqcup_j(E_i\cap F_j) に分割され，各 F_j も F_j=\bigsqcup_i(E_i\cap F_j) に分割される．半加法族上の前測度の有限加法性を使えば， \sum_i\mu_0(E_i)=\sum_{i,j}\mu_0(E_i\cap F_j)=\sum_j\mu_0(F_j) となる．よって表示によらず定まる．有限加法性は表示を並べればよい．可算加法性は，A=\bigsqcup_n A_n\in\calA(\calE) をさらに A=\bigsqcup_i E_i と書き，各 E_i を A_n\cap E_i で分割して半加法族上の前測度の可算加法性を適用すれば従う．