Lebesgue積分講義ノート

11.3. Fubiniの定理🔗

Fubiniの定理は，符号がある関数でも絶対可積分なら積分順序を交換できる，という定理である． Tonelliが「非負ならよい」という定理であるのに対し，Fubiniは「絶対値が積分できるならよい」という定理である．

Theorem11.3.1
uses 1used by 1✓L∃∀N
Tagsleanok

Fubiniの定理. f\in\calL^1(X\times Y) とする． このとき，\mu-a.e. の x\in X に対して f_x\in\calL^1(Y) であり， \nu-a.e. の y\in Y に対して f^y\in\calL^1(X) である． さらに，g(x):=\int_Y f(x,y)\,d\nu(y) と h(y):=\int_X f(x,y)\,d\mu(x) は a.e. の値を適当に定めれば g\in\calL^1(X)，h\in\calL^1(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.3.1●5 theorems
  • theoremdefined in NoteKsk/«11fubini».lean
    complete
    theorem NoteKsk.Chapter11.ae_integrable_section_right.{u_1, u_2, u_3}
  {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α]
  [MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [NormedAddCommGroup E]
  [MeasureTheory.SFinite ν] {f : α × β → E}
  (hf : MeasureTheory.Integrable f (μ.prod ν)) :
  ∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun y ↦ f (x, y)) ν
    theorem NoteKsk.Chapter11.ae_integrable_section_right.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {E : Type u_3} [MeasurableSpace α]
  [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  [NormedAddCommGroup E]
  [MeasureTheory.SFinite ν]
  {f : α × β → E}
  (hf :
    MeasureTheory.Integrable f
      (μ.prod ν)) :
  ∀ᵐ (x : α) ∂μ,
    MeasureTheory.Integrable
      (fun y ↦ f (x, y)) ν
    Almost-everywhere integrability of sections.
  • theoremdefined in NoteKsk/«11fubini».lean
    complete
    theorem NoteKsk.Chapter11.fubini_integral_prod.{u_1, u_2, u_3} {α : Type u_1}
  {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν] (f : α × β → E)
  (hf : MeasureTheory.Integrable f (μ.prod ν)) :
  ∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
    theorem NoteKsk.Chapter11.fubini_integral_prod.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {E : Type u_3} [MeasurableSpace α]
  [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν]
  (f : α × β → E)
  (hf :
    MeasureTheory.Integrable f
      (μ.prod ν)) :
  ∫ (z : α × β), f z ∂μ.prod ν =
    ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
    Fubini's theorem for Bochner integrals.
  • theoremdefined in NoteKsk/«11fubini».lean
    complete
    theorem NoteKsk.Chapter11.fubini_integral_prod_symm.{u_1, u_2, u_3}
  {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α]
  [MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] (f : α × β → E)
  (hf : MeasureTheory.Integrable f (μ.prod ν)) :
  ∫ (z : α × β), f z ∂μ.prod ν = ∫ (y : β), ∫ (x : α), f (x, y) ∂μ ∂ν
    theorem NoteKsk.Chapter11.fubini_integral_prod_symm.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {E : Type u_3} [MeasurableSpace α]
  [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν]
  (f : α × β → E)
  (hf :
    MeasureTheory.Integrable f
      (μ.prod ν)) :
  ∫ (z : α × β), f z ∂μ.prod ν =
    ∫ (y : β), ∫ (x : α), f (x, y) ∂μ ∂ν
    Fubini's theorem with the order of integration reversed.
  • theoremdefined in NoteKsk/«11fubini».lean
    complete
    theorem NoteKsk.Chapter11.integrable_integral_section_right.{u_1, u_2, u_3}
  {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α]
  [MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [MeasureTheory.SFinite ν] {f : α × β → E}
  (hf : MeasureTheory.Integrable f (μ.prod ν)) :
  MeasureTheory.Integrable (fun x ↦ ∫ (y : β), f (x, y) ∂ν) μ
    theorem NoteKsk.Chapter11.integrable_integral_section_right.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {E : Type u_3} [MeasurableSpace α]
  [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  [MeasureTheory.SFinite ν]
  {f : α × β → E}
  (hf :
    MeasureTheory.Integrable f
      (μ.prod ν)) :
  MeasureTheory.Integrable
    (fun x ↦ ∫ (y : β), f (x, y) ∂ν) μ
    Integrability of the function obtained by integrating the right section.
  • theoremdefined in NoteKsk/«11fubini».lean
    complete
    theorem NoteKsk.Chapter11.integrable_integral_section_left.{u_1, u_2, u_3}
  {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α]
  [MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] {f : α × β → E}
  (hf : MeasureTheory.Integrable f (μ.prod ν)) :
  MeasureTheory.Integrable (fun y ↦ ∫ (x : α), f (x, y) ∂μ) ν
    theorem NoteKsk.Chapter11.integrable_integral_section_left.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {E : Type u_3} [MeasurableSpace α]
  [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν]
  {f : α × β → E}
  (hf :
    MeasureTheory.Integrable f
      (μ.prod ν)) :
  MeasureTheory.Integrable
    (fun y ↦ ∫ (x : α), f (x, y) ∂μ) ν
    Integrability of the function obtained by integrating the left section.
Proof for Theorem 11.3.1
uses 0

Fubiniの定理はTonelliの定理から導く． まず |f| にTonelliを適用し，f\in\calL^1(X\times Y) ならほとんどすべての切片で \int_Y |f(x,y)|\,d\nu(y)<\infty，\int_X |f(x,y)|\,d\mu(x)<\infty となることを得る． そのうえで f=f^+-f^- と分解し，f^+ と f^- にTonelliを適用して差を取る． つまり，証明の流れは「積測度の構成 \to 集合に関するFubini \to 非負関数のTonelli \to 可積分関数のFubini」である．

Remark (ベクトル値の場合). Fubiniの定理は，実数値関数だけでなく有限次元ベクトル値関数にも同じ形で成り立つ． その場合は，絶対値をノルムに置き換えて \int_{X\times Y}\|f(x,y)\|\,d(\mu\otimes\nu)<\infty を確認すればよい． この講義の範囲では，各成分に実数値のFubiniの定理を適用すると思えば十分である．

Corollary11.3.2
Statement uses 2
Statement dependency previews
Preview
Theorem 11.2.1
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
used by 0✓L∃∀N

積分順序の交換判定. f\in M(X\times Y) とする． このとき，|f|\ge0 にTonelliを適用すると

\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)

が [0,\infty] の値として成り立つ． したがって，この3つの量のどれか一つが有限なら f\in\calL^1(X\times Y) であり，

\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)

が成り立つ． 実際の計算では，直接の積分，x から先に積分する反復積分，y から先に積分する反復積分のうち，有限性を確かめやすいものを一つ調べればよい．

Lean code for Corollary11.3.2●1 theorem
  • theoremdefined in NoteKsk/«11fubini».lean
    complete
    theorem NoteKsk.Chapter11.integral_integral_swap.{u_1, u_2, u_3} {α : Type u_1}
  {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν] {f : α → β → E}
  (hf : MeasureTheory.Integrable (Function.uncurry f) (μ.prod ν)) :
  ∫ (x : α), ∫ (y : β), f x y ∂ν ∂μ = ∫ (y : β), ∫ (x : α), f x y ∂μ ∂ν
    theorem NoteKsk.Chapter11.integral_integral_swap.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {E : Type u_3} [MeasurableSpace α]
  [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν]
  {f : α → β → E}
  (hf :
    MeasureTheory.Integrable
      (Function.uncurry f) (μ.prod ν)) :
  ∫ (x : α), ∫ (y : β), f x y ∂ν ∂μ =
    ∫ (y : β), ∫ (x : α), f x y ∂μ ∂ν
    Exchange of iterated integrals for an integrable function.
Proposition11.3.3
uses 0used by 0XL∃∀N
Tagsexample

積分領域の入れ替え. 連続関数 \varphi:[0,1]\to\RR に対して Fubiniより \int_0^1(\int_0^x \varphi(y)\,dy)dx=\int_0^1(\int_y^1 \varphi(y)\,dx)dy=\int_0^1(1-y)\varphi(y)\,dy である． これは領域 0\le y\le x\le1 を，0\le y\le1，y\le x\le1 と読み替えただけである． 例えば \varphi(y)=e^{y^2} のように原始関数が初等的に書けない場合でも，順序交換により計算しやすい形へ変えられる．