Lebesgue積分講義ノート

11.1. 積測度と切片🔗

本章の前半では，\sigma-有限な測度空間 (X,\calM,\mu) と (Y,\calN,\nu) を固定する． 積空間には積 \sigma-加法族 \calM\otimes\calN と積測度 \mu\otimes\nu を入れる． ここで \calM\otimes\calN とは，基本図形 A\times B（A\in\calM，B\in\calN）全体が生成する X\times Y 上の \sigma-加法族である． 積測度は基本図形について (\mu\otimes\nu)(A\times B)=\mu(A)\nu(B) を満たす測度である． 以下では積測度空間 (X\times Y,\calM\otimes\calN,\mu\otimes\nu) 上の可測関数全体を M(X\times Y;\eRR) と表す．

Remark. \sigma-有限性は，積測度の一意性やTonelli--Fubiniの標準形を使うための仮定である． Lebesgue測度空間は \sigma-有限なので，本章の定理は \RR^m\times\RR^n 上の積分にもそのまま適用できる．

Remark (積測度の構成). 積測度の存在は自明ではない． 証明ではまず基本図形 A\times B に \mu(A)\nu(B) を対応させ，有限個の互いに素な基本図形の和でできる集合上に前測度を作る． その後，Carathéodory--Hahnの拡張定理を用いて，この前測度を積 \sigma-加法族 \calM\otimes\calN 上の測度へ拡張する． \sigma-有限性のもとでは，この測度は基本図形上の値によって一意に決まる．

ただし，もとの測度空間が完備であっても，積測度空間が自動的に完備になるとは限らない． Lebesgue測度の場合，\RR^m\times\RR^n は自然に \RR^{m+n} と同一視される． この同一視のもとで，\lambda_m\otimes\lambda_n は \lambda_{m+n} と同じものとして扱ってよい． 厳密には積 \sigma-加法族の完備化を考えるが，通常の計算ではこの違いは問題にならない． 今後は \int_{\RR^m\times\RR^n} f(x,y)\,d(\lambda_m\otimes\lambda_n) を \int_{\RR^m}\int_{\RR^n} f(x,y)\,dy\,dx のように略記する． これは記法の省略であり，正当化はTonelliまたはFubiniによって行う．

Definition11.1.1
uses 0
Used by 3
Reverse dependency previews
Preview
Theorem 11.1.2
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N
Tagsleanok

切片. E\subset X\times Y と f:X\times Y\to\eRR に対して，各 x\in X，y\in Y について E_x:=\{y\in Y\mid (x,y)\in E\}，E^y:=\{x\in X\mid (x,y)\in E\} と書く． また f_x(y):=f(x,y)，f^y(x):=f(x,y) と書き，これらを切片という．

Lean code for Definition11.1.1●4 definitions
  • defdefined in NoteKsk/«11fubini».lean
    complete
    def NoteKsk.Chapter11.xSection.{u_1, u_2} {α : Type u_1} {β : Type u_2}
  (E : Set (α × β)) (x : α) : Set β
    def NoteKsk.Chapter11.xSection.{u_1, u_2}
  {α : Type u_1} {β : Type u_2}
  (E : Set (α × β)) (x : α) : Set β

    Definition body

    def xSection (E : Set (α × β)) (x : α) : Set β :=
  Prod.mk x ⁻¹' E
    The `x`-section of a subset of a product.
  • defdefined in NoteKsk/«11fubini».lean
    complete
    def NoteKsk.Chapter11.ySection.{u_1, u_2} {α : Type u_1} {β : Type u_2}
  (E : Set (α × β)) (y : β) : Set α
    def NoteKsk.Chapter11.ySection.{u_1, u_2}
  {α : Type u_1} {β : Type u_2}
  (E : Set (α × β)) (y : β) : Set α

    Definition body

    def ySection (E : Set (α × β)) (y : β) : Set α :=
  (fun x : α => (x, y)) ⁻¹' E
    The `y`-section of a subset of a product.
  • defdefined in NoteKsk/«11fubini».lean
    complete
    def NoteKsk.Chapter11.functionXSection.{u_1, u_2, u_3} {α : Type u_1}
  {β : Type u_2} {γ : Type u_3} (f : α × β → γ) (x : α) : β → γ
    def NoteKsk.Chapter11.functionXSection.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {γ : Type u_3} (f : α × β → γ) (x : α) :
  β → γ

    Definition body

    def functionXSection (f : α × β → γ) (x : α) : β → γ :=
  fun y => f (x, y)
    The `x`-section of a function on a product.
  • defdefined in NoteKsk/«11fubini».lean
    complete
    def NoteKsk.Chapter11.functionYSection.{u_1, u_2, u_3} {α : Type u_1}
  {β : Type u_2} {γ : Type u_3} (f : α × β → γ) (y : β) : α → γ
    def NoteKsk.Chapter11.functionYSection.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {γ : Type u_3} (f : α × β → γ) (y : β) :
  α → γ

    Definition body

    def functionYSection (f : α × β → γ) (y : β) : α → γ :=
  fun x => f (x, y)
    The `y`-section of a function on a product.
Theorem11.1.2
uses 1used by 1✓L∃∀N
Tagsleanok

切片の可測性. E\in\calM\otimes\calN なら，すべての x\in X と y\in Y に対して E_x\in\calN，E^y\in\calM である． また f\in M(X\times Y;\eRR) なら，すべての x\in X と y\in Y に対して f_x\in M(Y;\eRR)，f^y\in M(X;\eRR) である．

Lean code for Theorem11.1.2●4 theorems
  • theoremdefined in NoteKsk/«11fubini».lean
    complete
    theorem NoteKsk.Chapter11.measurableSet_xSection.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β]
  {E : Set (α × β)} (hE : MeasurableSet E) (x : α) :
  MeasurableSet (NoteKsk.Chapter11.xSection E x)
    theorem NoteKsk.Chapter11.measurableSet_xSection.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β]
  {E : Set (α × β)} (hE : MeasurableSet E)
  (x : α) :
  MeasurableSet
    (NoteKsk.Chapter11.xSection E x)
  • theoremdefined in NoteKsk/«11fubini».lean
    complete
    theorem NoteKsk.Chapter11.measurableSet_ySection.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β]
  {E : Set (α × β)} (hE : MeasurableSet E) (y : β) :
  MeasurableSet (NoteKsk.Chapter11.ySection E y)
    theorem NoteKsk.Chapter11.measurableSet_ySection.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β]
  {E : Set (α × β)} (hE : MeasurableSet E)
  (y : β) :
  MeasurableSet
    (NoteKsk.Chapter11.ySection E y)
  • theoremdefined in NoteKsk/«11fubini».lean
    complete
    theorem NoteKsk.Chapter11.measurable_functionXSection.{u_1, u_2, u_3}
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α]
  [MeasurableSpace β] [MeasurableSpace γ] {f : α × β → γ}
  (hf : Measurable f) (x : α) :
  Measurable (NoteKsk.Chapter11.functionXSection f x)
    theorem NoteKsk.Chapter11.measurable_functionXSection.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {γ : Type u_3} [MeasurableSpace α]
  [MeasurableSpace β] [MeasurableSpace γ]
  {f : α × β → γ} (hf : Measurable f)
  (x : α) :
  Measurable
    (NoteKsk.Chapter11.functionXSection f
      x)
  • theoremdefined in NoteKsk/«11fubini».lean
    complete
    theorem NoteKsk.Chapter11.measurable_functionYSection.{u_1, u_2, u_3}
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α]
  [MeasurableSpace β] [MeasurableSpace γ] {f : α × β → γ}
  (hf : Measurable f) (y : β) :
  Measurable (NoteKsk.Chapter11.functionYSection f y)
    theorem NoteKsk.Chapter11.measurable_functionYSection.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {γ : Type u_3} [MeasurableSpace α]
  [MeasurableSpace β] [MeasurableSpace γ]
  {f : α × β → γ} (hf : Measurable f)
  (y : β) :
  Measurable
    (NoteKsk.Chapter11.functionYSection f
      y)
Proof for Theorem 11.1.2
uses 0

集合の切片については，x\in X を固定し， \mathcal C_x:=\{E\in\calM\otimes\calN\mid E_x\in\calN\} とおく． 空集合，補集合，可算和について切片を取る操作はそれぞれ空集合，補集合，可算和と両立するので，\mathcal C_x は \sigma-加法族である． また可測矩形 A\times B の x-切片は，x\in A なら B，x\notin A なら \emptyset であるから可測である． したがって \mathcal C_x は可測矩形が生成する \calM\otimes\calN 全体を含む． E^y についても同様である．

関数の切片については，例えば \{y\in Y\mid f_x(y)>a\}=\{(u,v)\in X\times Y\mid f(u,v)>a\}_x と書ける． 右辺は可測集合の切片なので可測であり，したがって f_x は可測である． f^y についても同様である．

Theorem11.1.3
Statement uses 2
Statement dependency previews
Preview
Definition 11.1.1
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
used by 0✓L∃∀N
Tagsleanok

Cavalieriの原理. E\in\calM\otimes\calN とする． このとき x\mapsto \nu(E_x) は X 上可測であり，

(\mu\otimes\nu)(E)=\int_X \nu(E_x)\,d\mu(x)

が成り立つ． 同様に y\mapsto \mu(E^y) は Y 上可測であり，

(\mu\otimes\nu)(E)=\int_Y \mu(E^y)\,d\nu(y)

が成り立つ．

Lean code for Theorem11.1.3●4 theorems
  • theoremdefined in NoteKsk/«11fubini».lean
    complete
    theorem NoteKsk.Chapter11.productMeasure_apply.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite ν] {E : Set (α × β)} (hE : MeasurableSet E) :
  (μ.prod ν) E = ∫⁻ (x : α), ν (NoteKsk.Chapter11.xSection E x) ∂μ
    theorem NoteKsk.Chapter11.productMeasure_apply.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite ν]
  {E : Set (α × β)}
  (hE : MeasurableSet E) :
  (μ.prod ν) E =
    ∫⁻ (x : α),
      ν
        (NoteKsk.Chapter11.xSection E
          x) ∂μ
    Product measure on measurable sets, written using sections.
  • theoremdefined in NoteKsk/«11fubini».lean
    complete
    theorem NoteKsk.Chapter11.productMeasure_apply_symm.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] {E : Set (α × β)}
  (hE : MeasurableSet E) :
  (μ.prod ν) E = ∫⁻ (y : β), μ (NoteKsk.Chapter11.ySection E y) ∂ν
    theorem NoteKsk.Chapter11.productMeasure_apply_symm.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν]
  {E : Set (α × β)}
  (hE : MeasurableSet E) :
  (μ.prod ν) E =
    ∫⁻ (y : β),
      μ
        (NoteKsk.Chapter11.ySection E
          y) ∂ν
    Product measure on measurable sets, written using the other family of sections.
  • theoremdefined in NoteKsk/«11fubini».lean
    complete
    theorem NoteKsk.Chapter11.measurable_measure_xSection.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β]
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν]
  {E : Set (α × β)} (hE : MeasurableSet E) :
  Measurable fun x ↦ ν (NoteKsk.Chapter11.xSection E x)
    theorem NoteKsk.Chapter11.measurable_measure_xSection.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β]
  {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite ν]
  {E : Set (α × β)}
  (hE : MeasurableSet E) :
  Measurable fun x ↦
    ν (NoteKsk.Chapter11.xSection E x)
    Measurability of the section-measure function.
  • theoremdefined in NoteKsk/«11fubini».lean
    complete
    theorem NoteKsk.Chapter11.measurable_measure_ySection.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ]
  {E : Set (α × β)} (hE : MeasurableSet E) :
  Measurable fun y ↦ μ (NoteKsk.Chapter11.ySection E y)
    theorem NoteKsk.Chapter11.measurable_measure_ySection.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  [MeasureTheory.SFinite μ]
  {E : Set (α × β)}
  (hE : MeasurableSet E) :
  Measurable fun y ↦
    μ (NoteKsk.Chapter11.ySection E y)
    Measurability of the other section-measure function.
Proof for Theorem 11.1.3
uses 0

まず可測矩形 E=A\times B について確認する． このとき \nu(E_x)=\nu(B)1_A(x) だから， \int_X\nu(E_x)\,d\mu(x)=\mu(A)\nu(B)=(\mu\otimes\nu)(A\times B) である．

次に，この公式と可測性が成り立つ集合 E 全体を集める． 有限測度空間の場合，この集合族は空集合を含み，補集合と互いに素な可算和に対して閉じている． 閉じていることは，切片が補集合・和・極限と両立すること，測度の可算加法性，単調収束定理から従う． したがって，可測矩形を含む \sigma-加法族になり，\calM\otimes\calN 全体で公式が成り立つ．

\sigma-有限な場合は，X と Y を有限測度の可測集合列で増大近似し，有限測度部分で得た公式を単調収束定理で極限に送る． y に関する式も同じ議論で得られる．

Remark. Cavalieriの原理は「集合に関するFubiniの定理」とも呼ばれる． これは指示関数 1_E に対する積分公式と同じ内容であり，後で関数に対するTonelli--Fubiniを導く出発点になる．