Lebesgue積分講義ノート

11.2. Tonelliの定理🔗

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

Theorem11.2.1
uses 1
Used by 5
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 0⚠L∃∀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 である．

Lean code for Proposition11.2.2●1 theorem, incomplete
  • theoremdefined in NoteKsk/«11fubini».lean
    contains sorry
    theorem NoteKsk.Chapter11.triangle_area_tonelli :
  MeasureTheory.volume
      {p | p.1 ∈ Set.Icc 0 1 ∧ p.2 ∈ Set.Icc 0 1 ∧ p.1 + p.2 ≤ 1} =
    ENNReal.ofReal (1 / 2)
    theorem NoteKsk.Chapter11.triangle_area_tonelli :
  MeasureTheory.volume
      {p |
        p.1 ∈ Set.Icc 0 1 ∧
          p.2 ∈ Set.Icc 0 1 ∧
            p.1 + p.2 ≤ 1} =
    ENNReal.ofReal (1 / 2)
    The unit right triangle in `[0, 1]²` has area `1 / 2`.
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.
Proposition11.2.4
Statement uses 2
Statement dependency previews
Preview
Theorem 11.1.3
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
used by 0⚠L∃∀N
Tagsexample

分布公式. f\in M^+(X) とする． このとき

\int_X f\,d\mu = \int_0^\infty \mu(\{x\in X\mid f(x)\ge t\})\,dt

が成り立つ． これは分布公式（tail-integral formula），または層化表示（layer-cake representation）と呼ばれる．

実際，X\times(0,\infty) の部分集合 E:=\{(x,t)\mid 0<t\le f(x)\} を考える． 各 x に対する切片は E_x=(0,f(x)]（f(x)=\infty のときは (0,\infty)）なので，\lambda_1(E_x)=f(x) である． 一方，各 t>0 に対する切片は E^t=\{x\in X\mid f(x)\ge t\} である． したがってCavalieriの原理，または指示関数 1_E へのTonelliの適用により，

\int_X f\,d\mu = \int_X \lambda_1(E_x)\,d\mu(x) = \int_0^\infty \mu(E^t)\,dt = \int_0^\infty \mu(\{x\in X\mid f(x)\ge t\})\,dt

を得る． 非負関数の積分は，その上側集合の測度を高さ方向に積分したものと見なせる．

Lean code for Proposition11.2.4●1 theorem, incomplete
  • theoremdefined in NoteKsk/«11fubini».lean
    contains sorry
    theorem NoteKsk.Chapter11.layerCake_lintegral.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ENNReal}
  (hf : AEMeasurable f μ) :
  ∫⁻ (x : α), f x ∂μ =
    ∫⁻ (t : ℝ) in Set.Ioi 0, μ {x | ENNReal.ofReal t ≤ f x}
    theorem NoteKsk.Chapter11.layerCake_lintegral.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {f : α → ENNReal}
  (hf : AEMeasurable f μ) :
  ∫⁻ (x : α), f x ∂μ =
    ∫⁻ (t : ℝ) in Set.Ioi 0,
      μ {x | ENNReal.ofReal t ≤ f x}
    Layer-cake / tail-integral formula for an `ℝ≥0∞`-valued function.

The notes state the same principle for nonnegative measurable functions.  This
extended-nonnegative version is the natural Tonelli form in mathlib.