11.2. Tonelliの定理🔗

Tonelliの定理は，非負関数なら積分可能性を先に確認しなくても反復積分に直せる，という定理である．両辺が +\infty になることも許す．

Theorem11.2.1

uses 1

Used by 3

Reverse dependency previews

Preview

Proposition 11.2.3

Loading preview

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

✓L∃∀N

Tagsleanok

Tonelliの定理. f\in M^+(X\times Y) とする．このとき x\mapsto \int_Y f(x,y)\,d\nu(y) は M^+(X) に属し， y\mapsto \int_X f(x,y)\,d\mu(x) は M^+(Y) に属する．さらに

\int_{X\times Y} f\,d(\mu\otimes\nu)=\int_X\!\int_Y f(x,y)\,d\nu(y)\,d\mu(x)=\int_Y\!\int_X f(x,y)\,d\mu(x)\,d\nu(y)

が成り立つ．

Lean code for Theorem11.2.1●3 theorems

theoremdefined in NoteKsk/«11fubini».lean

complete

theorem NoteKsk.Chapter11.tonelli_lintegral.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite ν] (f : α × β → ENNReal)
  (hf : AEMeasurable f (μ.prod ν)) :
  ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ

theorem NoteKsk.Chapter11.tonelli_lintegral.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite ν]
  (f : α × β → ENNReal)
  (hf : AEMeasurable f (μ.prod ν)) :
  ∫⁻ (z : α × β), f z ∂μ.prod ν =
    ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ

Tonelli's theorem for nonnegative functions.

theoremdefined in NoteKsk/«11fubini».lean

complete

theorem NoteKsk.Chapter11.tonelli_lintegral_symm.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν]
  (f : α × β → ENNReal) (hf : AEMeasurable f (μ.prod ν)) :
  ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (y : β), ∫⁻ (x : α), f (x, y) ∂μ ∂ν

theorem NoteKsk.Chapter11.tonelli_lintegral_symm.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν]
  (f : α × β → ENNReal)
  (hf : AEMeasurable f (μ.prod ν)) :
  ∫⁻ (z : α × β), f z ∂μ.prod ν =
    ∫⁻ (y : β), ∫⁻ (x : α), f (x, y) ∂μ ∂ν

Tonelli's theorem with the order of integration reversed.

theoremdefined in NoteKsk/«11fubini».lean

complete

theorem NoteKsk.Chapter11.measurable_lintegral_section_right.{u_1, u_2}
  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β]
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν]
  {f : α × β → ENNReal} (hf : Measurable f) :
  Measurable fun x ↦ ∫⁻ (y : β), f (x, y) ∂ν

theorem NoteKsk.Chapter11.measurable_lintegral_section_right.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β]
  {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite ν]
  {f : α × β → ENNReal}
  (hf : Measurable f) :
  Measurable fun x ↦
    ∫⁻ (y : β), f (x, y) ∂ν

The inner integral in Tonelli is measurable.

Proof for Theorem 11.2.1

uses 0

Tonelliの証明は，積測度の存在とCavalieriの原理から始める．まず 1_E についてはCavalieriの原理そのものであり，有限線形結合により非負単関数の場合が従う．一般の非負可測関数は，非負単関数の単調増加極限で近似し，単調収束定理によって極限を積分の外へ出す．この手順により，集合に関するFubiniから非負関数に対するTonelliが得られる．

Remark (使い方). 被積分関数が非負なら，まずTonelliを使ってよい．例えば f\ge0 のときは，\int_{X\times Y}f を直接計算しても， \int_X\int_Y f または \int_Y\int_X f として計算してもよい．収束性を先に調べる必要はないが，答えが +\infty になる可能性は残る．

Proposition11.2.2

uses 0used by 0XL∃∀N

Tagsexample

三角形の面積. E:=\{(x,y)\in[0,1]^2\mid x+y\le1\} とする．指示関数 1_E は非負可測なのでTonelliを使える．各 x\in[0,1] について E_x=[0,1-x] だから (\lambda_1\otimes\lambda_1)(E)=\int_0^1 \lambda_1(E_x)\,d\lambda_1(x)=\int_0^1(1-x)\,dx=\frac12 である．

Proposition11.2.3

uses 1used by 0✓L∃∀N

Tagsleanokexample

直積形の関数. f\in M^+(X)，g\in M^+(Y) とする．このとき h(x,y):=f(x)g(y) は M^+(X\times Y) に属し，Tonelliより \int_{X\times Y}h\,d(\mu\otimes\nu)=\left(\int_X f\,d\mu\right)\left(\int_Y g\,d\nu\right) である．これは，長方形の測度公式 (\mu\otimes\nu)(A\times B)=\mu(A)\nu(B) の関数版である．

Lean code for Proposition11.2.3●1 theorem

theoremdefined in NoteKsk/«11fubini».lean

complete

theorem NoteKsk.Chapter11.lintegral_prod_mul.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite ν] {f : α → ENNReal} {g : β → ENNReal}
  (hf : AEMeasurable f μ) (hg : AEMeasurable g ν) :
  ∫⁻ (z : α × β), f z.1 * g z.2 ∂μ.prod ν =
    (∫⁻ (x : α), f x ∂μ) * ∫⁻ (y : β), g y ∂ν

theorem NoteKsk.Chapter11.lintegral_prod_mul.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite ν]
  {f : α → ENNReal} {g : β → ENNReal}
  (hf : AEMeasurable f μ)
  (hg : AEMeasurable g ν) :
  ∫⁻ (z : α × β),
      f z.1 * g z.2 ∂μ.prod ν =
    (∫⁻ (x : α), f x ∂μ) *
      ∫⁻ (y : β), g y ∂ν

Product form of Tonelli.