7.2. 可測写像🔗

Definition7.2.1

uses 0used by 1✓L∃∀N

Tagsmathlibok

可測空間. 集合 X とその上の\sigma-加法族 \calM の組

(X,\calM)

を可測空間という．

Lean code for Definition7.2.1●2 definitions

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`.

Definition7.2.2

uses 1

Used by 3

Reverse dependency previews

Preview

Proposition 7.2.4

Loading preview

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

✓L∃∀N

Tagsleanok

可測写像. 可測空間 (X,\calM) と (Y,\calN) の間の写像 f:X\to Y が可測であるとは，任意の B \in \calN に対して f^{-1}(B)\in \calM が成り立つことをいう．

Lean code for Definition7.2.2●2 declarations

abbrevdefined in NoteKsk/Defs.lean

complete

abbrev NoteKsk.MeasurableMap.{u_1, u_2} {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β] (f : α → β) : Prop

abbrev NoteKsk.MeasurableMap.{u_1, u_2}
  {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β]
  (f : α → β) : Prop

Definition body

abbrev MeasurableMap {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
    (f : α → β) : Prop :=
  Measurable f

Lecture-note synonym for mathlib's measurable maps.

theoremdefined in NoteKsk/«07mble-funcs».lean

complete

theorem NoteKsk.Chapter07.measurableMap_iff_preimage.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} :
  NoteKsk.MeasurableMap f ↔
    ∀ ⦃B : Set β⦄, MeasurableSet B → MeasurableSet (f ⁻¹' B)

theorem NoteKsk.Chapter07.measurableMap_iff_preimage.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β]
  {f : α → β} :
  NoteKsk.MeasurableMap f ↔
    ∀ ⦃B : Set β⦄,
      MeasurableSet B →
        MeasurableSet (f ⁻¹' B)

以下では，写像f : X \to Y による集合族 \calE\subset\calP(Y) の逆像を

f^{-1}(\calE):=\{f^{-1}(E)\mid E\in\calE\}

と略記する．例えば，写像の可測性は f^{-1}(\calN) \subset \calM と書ける．

Proposition7.2.3

uses 0used by 1✓L∃∀N

Tagsleanok

逆像の基本性質. 任意の写像 f:X\to Y と部分集合族 \{B_s\}_{s\in S}\subset \mathcal P(Y) に対して次が成り立つ．

f^{-1}(Y\setminus B) =X\setminus f^{-1}(B),\quad f^{-1}\left(\bigcup_{s\in S}B_s\right) =\bigcup_{s\in S}f^{-1}(B_s),\quad f^{-1}\left(\bigcap_{s\in S}B_s\right) =\bigcap_{s\in S}f^{-1}(B_s).

ここで添え字集合Sは非可算無限集合でもよい．

Lean code for Proposition7.2.3●3 theorems

theoremdefined in NoteKsk/«07mble-funcs».lean

complete

theorem NoteKsk.Chapter07.preimage_compl.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} (f : α → β) (B : Set β) : f ⁻¹' Bᶜ = (f ⁻¹' B)ᶜ

theorem NoteKsk.Chapter07.preimage_compl.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  (f : α → β) (B : Set β) :
  f ⁻¹' Bᶜ = (f ⁻¹' B)ᶜ

theoremdefined in NoteKsk/«07mble-funcs».lean

complete

theorem NoteKsk.Chapter07.preimage_iUnion.{u_1, u_2, u_4} {α : Type u_1}
  {β : Type u_2} {ι : Type u_4} (f : α → β) (B : ι → Set β) :
  f ⁻¹' ⋃ i, B i = ⋃ i, f ⁻¹' B i

theorem NoteKsk.Chapter07.preimage_iUnion.{u_1,
    u_2, u_4}
  {α : Type u_1} {β : Type u_2}
  {ι : Type u_4} (f : α → β)
  (B : ι → Set β) :
  f ⁻¹' ⋃ i, B i = ⋃ i, f ⁻¹' B i

theoremdefined in NoteKsk/«07mble-funcs».lean

complete

theorem NoteKsk.Chapter07.preimage_iInter.{u_1, u_2, u_4} {α : Type u_1}
  {β : Type u_2} {ι : Type u_4} (f : α → β) (B : ι → Set β) :
  f ⁻¹' ⋂ i, B i = ⋂ i, f ⁻¹' B i

theorem NoteKsk.Chapter07.preimage_iInter.{u_1,
    u_2, u_4}
  {α : Type u_1} {β : Type u_2}
  {ι : Type u_4} (f : α → β)
  (B : ι → Set β) :
  f ⁻¹' ⋂ i, B i = ⋂ i, f ⁻¹' B i

Proof for Proposition 7.2.3

uses 0

補集合quad x\in f^{-1}(Y\setminus B) であることは f(x)\in Y\setminus B，すなわち f(x)\notin B と同値である．これは x\notin f^{-1}(B)，つまり x\in X\setminus f^{-1}(B) と同値だから， f^{-1}(Y\setminus B)=X\setminus f^{-1}(B) である．

和集合quad x\in f^{-1}(\bigcup_s B_s) であることは，ある s について f(x)\in B_s となること，すなわち x\in f^{-1}(B_s) となることと同値である．したがって x\in \bigcup_{s\in S}f^{-1}(B_s) である．

共通部分quad 補集合と和集合の場合，および De Morgan の法則から従う．

Proposition7.2.4

Statement uses 2

Statement dependency previews

Preview

Definition 7.2.2

Loading preview

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

used by 1✓L∃∀N

Tagsleanok

\sigma-加法族の誘導. 任意の写像 f: X \to Y と Y上の\sigma-加法族 \calN に対して，逆像 \calM := f^{-1}(\calN) はX上の\sigma-加法族である．

Lean code for Proposition7.2.4●2 declarations

abbrevdefined in NoteKsk/«07mble-funcs».lean

complete

abbrev NoteKsk.Chapter07.inducedMeasurableSpace.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} (f : α → β) [MeasurableSpace β] : MeasurableSpace α

abbrev NoteKsk.Chapter07.inducedMeasurableSpace.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  (f : α → β) [MeasurableSpace β] :
  MeasurableSpace α

Definition body

abbrev inducedMeasurableSpace (f : α → β) [MeasurableSpace β] : MeasurableSpace α :=
  MeasurableSpace.comap f inferInstance

The inverse-image σ-algebra induced by a map.

theoremdefined in NoteKsk/«07mble-funcs».lean

complete

theorem NoteKsk.Chapter07.inducedMeasurableSpace_measurable.{u_1, u_2}
  {α : Type u_1} {β : Type u_2} (f : α → β) [MeasurableSpace β] :
  Measurable f

theorem NoteKsk.Chapter07.inducedMeasurableSpace_measurable.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  (f : α → β) [MeasurableSpace β] :
  Measurable f

Proof for Proposition 7.2.4

uses 0

まず f^{-1}(\emptyset) = \emptyset より \emptyset \in \calM である．次に Proposition 7.2.3より f^{-1}(Y\setminus B)=X\setminus f^{-1}(B) および f^{-1}(\bigcup_n B_n)=\bigcup_n f^{-1}(B_n) が成り立つので， A \in \calM \implies A^c \in \calM および \{A_i\}_{i=1}^\infty \subset \calM \implies \cup_{i=1}^\infty A_i \in \calM が言える．

Lemma7.2.5

uses 1

Used by 2

Reverse dependency previews

Preview

Theorem 7.3.4

Loading preview

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

✓L∃∀N

Tagsleanok

逆像と生成 \sigma-加法族の可換性. 任意の写像 f: X \to Y と集合族 \calE \subset \calP(Y) に対して，

f^{-1}\left(\sigma(\calE)\right) = \sigma\left(f^{-1}(\calE)\right)

が成り立つ．特に f : (X,\sigma(f^{-1}(\calE))) \to (Y,\sigma(\calE)) は可測写像である．

Lean code for Lemma7.2.5●2 theorems

theoremdefined in NoteKsk/«07mble-funcs».lean

complete

theorem NoteKsk.Chapter07.comap_generatedSigmaAlgebra.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} (f : α → β) (C : Set (Set β)) :
  MeasurableSpace.comap f (NoteKsk.generatedSigmaAlgebra C) =
    NoteKsk.generatedSigmaAlgebra (NoteKsk.preimageFamily f C)

theorem NoteKsk.Chapter07.comap_generatedSigmaAlgebra.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  (f : α → β) (C : Set (Set β)) :
  MeasurableSpace.comap f
      (NoteKsk.generatedSigmaAlgebra C) =
    NoteKsk.generatedSigmaAlgebra
      (NoteKsk.preimageFamily f C)

theoremdefined in NoteKsk/«07mble-funcs».lean

complete

theorem NoteKsk.Chapter07.measurable_to_generatedSigmaAlgebra.{u_1, u_2}
  {α : Type u_1} {β : Type u_2} (f : α → β) (C : Set (Set β)) :
  Measurable f

theorem NoteKsk.Chapter07.measurable_to_generatedSigmaAlgebra.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  (f : α → β) (C : Set (Set β)) :
  Measurable f

Remark. したがって，Y 側の \sigma-加法族がある生成族で記述されていれば，X 側ではその生成族の逆像だけを調べればよい．可測集合の全体\calBはしばしば超越的なので，その素性はよく分からないが，生成系\calEの方はある程度分かりやすい構造を持っていることがある．例えば，開集合系\calOが生成するBorel集合系\calB(\calO)などが典型的である．そのような場合にこの補題は威力を発揮する．

Proof for Lemma 7.2.5

uses 0

\sigma(\calE) は Y 上の \sigma-加法族である．したがってProposition 7.2.4より f^{-1}(\sigma(\calE)) は X 上の \sigma-加法族である．また f^{-1}(\calE)\subset f^{-1}(\sigma(\calE)) だから，

\sigma(f^{-1}(\calE))\subset f^{-1}(\sigma(\calE))

である．

逆向きを示す．

\calC:=\{B\subset Y\mid f^{-1}(B)\in\sigma(f^{-1}(\calE))\}

とおく．

\calC は Y 上の \sigma-加法族である．しかも \calE\subset\calC であるから，

\sigma(\calE)\subset\calC

である．したがって任意の B\in\sigma(\calE) に対して f^{-1}(B)\in\sigma(f^{-1}(\calE)) となる．これは

f^{-1}(\sigma(\calE))\subset\sigma(f^{-1}(\calE))

を意味する．以上より等号が成り立つ．

最後に，B\in\sigma(\calE) ならば f^{-1}(B)\in\sigma(f^{-1}(\calE)) であるから，述べた写像は可測である．

Remark (可測写像の定義はなぜ逆像か). 可測写像や連続写像の定義は，像ではなく逆像で書かれる．その理由は，逆像が補集合，可算和，可算共通部分といった集合演算を保つからである．実際，Proposition 7.2.3より f^{-1}(Y\setminus B)=X\setminus f^{-1}(B) および f^{-1}(\bigcup_n B_n)=\bigcup_n f^{-1}(B_n) が成り立つ．さらにLemma 7.2.5より，生成族について

f^{-1}(\sigma(\calE))=\sigma(f^{-1}(\calE))

が成り立つ．

これに対して像 f(B) は，一般には f(X\setminus A)=Y\setminus f(A) も f(\bigcap_n A_n)=\bigcap_n f(A_n) も満たさない．したがって「\sigma-加法族の構造を保つ」という意味で自然なのは像ではなく逆像なのである．