7.5. ベクトル値可測写像と合成🔗

Proposition7.5.1

uses 1used by 1✓L∃∀N

Tagsleanok

有限個の可測関数をまとめた写像. (X,\calM) を可測空間とし， f_1,\dots,f_n\in M(X;\RR) とする．このとき F:X\to\RR^n,\ F(x):=(f_1(x),\dots,f_n(x)) は可測である．

Lean code for Proposition7.5.1●1 theorem

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

complete

theorem NoteKsk.Chapter07.measurable_vector_map.{u_1} {α : Type u_1}
  [MeasurableSpace α] {n : ℕ} (f : Fin n → α → ℝ)
  (hf : ∀ (i : Fin n), Measurable (f i)) : Measurable fun x i ↦ f i x

theorem NoteKsk.Chapter07.measurable_vector_map.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {n : ℕ} (f : Fin n → α → ℝ)
  (hf : ∀ (i : Fin n), Measurable (f i)) :
  Measurable fun x i ↦ f i x

Proof for Proposition 7.5.1

uses 0

\mathcal C:=\{B\in\mathcal B(\RR^n)\mid F^{-1}(B)\in \calM\}

とおく．

\mathcal C は \sigma-加法族である．

任意の a_1,\dots,a_n\in\RR に対して

\begin{aligned} F^{-1}\bigl((-\infty,a_1]\times\cdots\times(-\infty,a_n]\bigr) = \bigcap_{k=1}^n \{x\in X\mid f_k(x)\le a_k\} \end{aligned}

であり，右辺は可測である．したがって

(-\infty,a_1]\times\cdots\times(-\infty,a_n]\in\mathcal C.

ところが，このような直方体は \mathcal B(\RR^n) を生成するから

\mathcal B(\RR^n)\subset \mathcal C

である．よって F は可測である．

Theorem7.5.2

uses 1used by 1✓L∃∀N

Tagsleanok

可測写像の合成. (X,\calM)，(Y,\calN)，(Z,\calP) を可測空間とする． F:(X,\calM)\to(Y,\calN) と G:(Y,\calN)\to(Z,\calP) が可測写像なら， G\circ F:(X,\calM)\to(Z,\calP) も可測写像である．

Lean code for Theorem7.5.2●1 theorem

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

complete

theorem NoteKsk.Chapter07.measurable_comp.{u_1, u_2, u_3} {α : Type u_1}
  {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β]
  [MeasurableSpace γ] {f : α → β} {g : β → γ}
  (hg : NoteKsk.MeasurableMap g) (hf : NoteKsk.MeasurableMap f) :
  NoteKsk.MeasurableMap (g ∘ f)

theorem NoteKsk.Chapter07.measurable_comp.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {γ : Type u_3} [MeasurableSpace α]
  [MeasurableSpace β] [MeasurableSpace γ]
  {f : α → β} {g : β → γ}
  (hg : NoteKsk.MeasurableMap g)
  (hf : NoteKsk.MeasurableMap f) :
  NoteKsk.MeasurableMap (g ∘ f)

Proof for Theorem 7.5.2

uses 0

任意の B\in\calP を取る． G は可測だから G^{-1}(B)\in\calN であり，さらに F は可測だから

(G\circ F)^{-1}(B)=F^{-1}(G^{-1}(B))\in\calM

である．したがって G\circ F は可測である．

Corollary7.5.3

Statement uses 2

Statement dependency previews

Preview

Proposition 7.4.1

Loading preview

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

used by 1✓L∃∀N

Tagsleanok

連続写像との合成. (X,\calM) を可測空間とする． F:(X,\calM)\to(\RR^n,\calB(\RR^n)) を可測写像， \Phi:\RR^n\to\RR を連続関数とする．このとき \Phi\circ F:X\to\RR は \calM-可測である．

Lean code for Corollary7.5.3●2 theorems

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

complete

theorem NoteKsk.Chapter07.measurable_continuous_comp.{u_1} {α : Type u_1}
  [MeasurableSpace α] {n : ℕ} {F : α → Fin n → ℝ} {φ : (Fin n → ℝ) → ℝ}
  (hF : Measurable F) (hφ : Continuous φ) : Measurable (φ ∘ F)

theorem NoteKsk.Chapter07.measurable_continuous_comp.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {n : ℕ} {F : α → Fin n → ℝ}
  {φ : (Fin n → ℝ) → ℝ}
  (hF : Measurable F)
  (hφ : Continuous φ) : Measurable (φ ∘ F)

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

complete

theorem NoteKsk.Chapter07.measurable_continuous_real_comp.{u_1} {α : Type u_1}
  [MeasurableSpace α] {f : α → ℝ} {φ : ℝ → ℝ} (hf : Measurable f)
  (hφ : Continuous φ) : Measurable (φ ∘ f)

theorem NoteKsk.Chapter07.measurable_continuous_real_comp.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {f : α → ℝ} {φ : ℝ → ℝ}
  (hf : Measurable f)
  (hφ : Continuous φ) : Measurable (φ ∘ f)

Proof for Corollary 7.5.3

uses 0

\Phi は連続だから，Proposition 7.4.1より \Phi:(\RR^n,\calB(\RR^n))\to(\RR,\calB(\RR)) は可測写像である．したがってTheorem 7.5.2より \Phi\circ F は可測である．

Corollary7.5.4

Statement uses 2

Statement dependency previews

Preview

Proposition 7.5.1

Loading preview

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

used by 1✓L∃∀N

Tagsleanok

代数演算と合成. (X,\calM) を可測空間とし， f,g\in M(X;\RR) とする．このとき次が成り立つ．

任意の c\in\RR に対して cf は可測である
f+g と fg は可測である
\max(f,g) と \min(f,g) は可測である
p>0 に対して |f|^p は可測である
\phi:\RR\to\RR が連続なら \phi\circ f は可測である

Lean code for Corollary7.5.4●7 theorems

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

complete

theorem NoteKsk.Chapter07.measurable_const_mul.{u_1} {α : Type u_1}
  [MeasurableSpace α] {f : α → ℝ} (hf : Measurable f) (c : ℝ) :
  Measurable fun x ↦ c * f x

theorem NoteKsk.Chapter07.measurable_const_mul.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {f : α → ℝ} (hf : Measurable f)
  (c : ℝ) : Measurable fun x ↦ c * f x

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

complete

theorem NoteKsk.Chapter07.measurable_add.{u_1} {α : Type u_1}
  [MeasurableSpace α] {f g : α → ℝ} (hf : Measurable f)
  (hg : Measurable g) : Measurable fun x ↦ f x + g x

theorem NoteKsk.Chapter07.measurable_add.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {f g : α → ℝ} (hf : Measurable f)
  (hg : Measurable g) :
  Measurable fun x ↦ f x + g x

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

complete

theorem NoteKsk.Chapter07.measurable_mul.{u_1} {α : Type u_1}
  [MeasurableSpace α] {f g : α → ℝ} (hf : Measurable f)
  (hg : Measurable g) : Measurable fun x ↦ f x * g x

theorem NoteKsk.Chapter07.measurable_mul.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {f g : α → ℝ} (hf : Measurable f)
  (hg : Measurable g) :
  Measurable fun x ↦ f x * g x

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

complete

theorem NoteKsk.Chapter07.measurable_max.{u_1} {α : Type u_1}
  [MeasurableSpace α] {f g : α → ℝ} (hf : Measurable f)
  (hg : Measurable g) : Measurable fun x ↦ max (f x) (g x)

theorem NoteKsk.Chapter07.measurable_max.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {f g : α → ℝ} (hf : Measurable f)
  (hg : Measurable g) :
  Measurable fun x ↦ max (f x) (g x)

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

complete

theorem NoteKsk.Chapter07.measurable_min.{u_1} {α : Type u_1}
  [MeasurableSpace α] {f g : α → ℝ} (hf : Measurable f)
  (hg : Measurable g) : Measurable fun x ↦ min (f x) (g x)

theorem NoteKsk.Chapter07.measurable_min.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {f g : α → ℝ} (hf : Measurable f)
  (hg : Measurable g) :
  Measurable fun x ↦ min (f x) (g x)

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

complete

theorem NoteKsk.Chapter07.measurable_abs_rpow.{u_1} {α : Type u_1}
  [MeasurableSpace α] {f : α → ℝ} (hf : Measurable f) (p : ℝ)
  (_hp : 0 < p) : Measurable fun x ↦ |f x| ^ p

theorem NoteKsk.Chapter07.measurable_abs_rpow.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {f : α → ℝ} (hf : Measurable f) (p : ℝ)
  (_hp : 0 < p) :
  Measurable fun x ↦ |f x| ^ p

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

complete

theorem NoteKsk.Chapter07.measurable_continuous_real_comp.{u_1} {α : Type u_1}
  [MeasurableSpace α] {f : α → ℝ} {φ : ℝ → ℝ} (hf : Measurable f)
  (hφ : Continuous φ) : Measurable (φ ∘ f)

theorem NoteKsk.Chapter07.measurable_continuous_real_comp.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {f : α → ℝ} {φ : ℝ → ℝ}
  (hf : Measurable f)
  (hφ : Continuous φ) : Measurable (φ ∘ f)

Proof for Corollary 7.5.4

uses 0

\Phi(t):=ct は連続だから，Corollary 7.5.3を n=1 に適用すればよい．
\Phi(u,v):=u+v と \Psi(u,v):=uv は \RR^2 上連続である．また (f,g):X\to\RR^2 はProposition 7.5.1より可測である．よって f+g=\Phi\circ(f,g) と fg=\Psi\circ(f,g) は可測である．
\Phi(u,v):=\max(u,v) と \Psi(u,v):=\min(u,v) は連続だから，同様に従う．
\phi(t):=|t|^p は連続だから従う．
Corollary 7.5.3そのものである．

Proposition7.5.5

Statement uses 2

Statement dependency previews

Preview

Theorem 7.3.4

Loading preview

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

used by 0✓L∃∀N

Tagsleanok

逆数. (X,\calM) を可測空間とし，f\in M(X;\RR) とする．このとき E_0:=\{x\in X\mid f(x)\ne 0\} は \calM に属し， 1/f:E_0\to\RR は \calM(E_0)-可測である．特に f(x)\ne 0 がすべての x\in X で成り立つなら，1/f は X 上可測である．

Lean code for Proposition7.5.5●3 theorems

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

complete

theorem NoteKsk.Chapter07.measurable_nonzero_set.{u_1} {α : Type u_1}
  [MeasurableSpace α] {f : α → ℝ} (hf : Measurable f) :
  MeasurableSet {x | f x ≠ 0}

theorem NoteKsk.Chapter07.measurable_nonzero_set.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {f : α → ℝ} (hf : Measurable f) :
  MeasurableSet {x | f x ≠ 0}

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

complete

theorem NoteKsk.Chapter07.measurable_reciprocal_on_nonzero.{u_1} {α : Type u_1}
  [MeasurableSpace α] {f : α → ℝ} (hf : Measurable f) :
  Measurable fun x ↦ (f ↑x)⁻¹

theorem NoteKsk.Chapter07.measurable_reciprocal_on_nonzero.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {f : α → ℝ} (hf : Measurable f) :
  Measurable fun x ↦ (f ↑x)⁻¹

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

complete

theorem NoteKsk.Chapter07.measurable_reciprocal_global.{u_1} {α : Type u_1}
  [MeasurableSpace α] {f : α → ℝ} (hf : Measurable f) :
  Measurable fun x ↦ (f x)⁻¹

theorem NoteKsk.Chapter07.measurable_reciprocal_global.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {f : α → ℝ} (hf : Measurable f) :
  Measurable fun x ↦ (f x)⁻¹

Mathlib also gives the total reciprocal on `ℝ`, with the convention `0⁻¹ = 0`.
This is stronger as a measurability statement than the restricted-domain form
used in the lecture notes.

Proof for Proposition 7.5.5

uses 0

まず

E_0=\{f>0\}\cup\{f<0\}

だから E_0\in\calM である．

h:=1/f:E_0\to\RR とおく．任意の a\in\RR に対して

\{h>a\} = \begin{cases} E_0\cap\{0<f<1/a\} & (a>0),\\ E_0\cap\{f>0\} & (a=0),\\ E_0\cap\bigl(\{f>0\}\cup\{f<1/a\}\bigr) & (a<0) \end{cases}

である．右辺はいずれも \calM(E_0) に属する．よってTheorem 7.3.4より h は \calM(E_0)-可測である．