10.3. Fatouの補題🔗

Theorem10.3.1

uses 1used by 1✓L∃∀N

Tagsleanok

Fatouの補題. f_n\in M^+(X) (n\in\NN) とする．このとき

\int_X \liminf_{n\to\infty} f_n\,d\mu \le \liminf_{n\to\infty}\int_X f_n\,d\mu

が成り立つ．

Lean code for Theorem10.3.1●2 theorems

theoremdefined in NoteKsk/«10limits».lean

complete

theorem NoteKsk.Chapter10.fatou_lintegral.{u_1, u_2} {α : Type u_1}
  {ι : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α}
  {f : ι → α → ENNReal} {l : Filter ι} [l.IsCountablyGenerated]
  (hf : ∀ (i : ι), Measurable (f i)) :
  ∫⁻ (x : α), Filter.liminf (fun i ↦ f i x) l ∂μ ≤
    Filter.liminf (fun i ↦ ∫⁻ (x : α), f i x ∂μ) l

theorem NoteKsk.Chapter10.fatou_lintegral.{u_1,
    u_2}
  {α : Type u_1} {ι : Type u_2}
  [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {f : ι → α → ENNReal} {l : Filter ι}
  [l.IsCountablyGenerated]
  (hf : ∀ (i : ι), Measurable (f i)) :
  ∫⁻ (x : α),
      Filter.liminf (fun i ↦ f i x) l ∂μ ≤
    Filter.liminf
      (fun i ↦ ∫⁻ (x : α), f i x ∂μ) l

Fatou's lemma for `ENNReal`-valued functions.

theoremdefined in NoteKsk/«10limits».lean

complete

theorem NoteKsk.Chapter10.fatou_lintegral_atTop.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α}
  {f : ℕ → α → ENNReal} (hf : ∀ (n : ℕ), Measurable (f n)) :
  ∫⁻ (x : α), Filter.liminf (fun n ↦ f n x) Filter.atTop ∂μ ≤
    Filter.liminf (fun n ↦ ∫⁻ (x : α), f n x ∂μ) Filter.atTop

theorem NoteKsk.Chapter10.fatou_lintegral_atTop.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {f : ℕ → α → ENNReal}
  (hf : ∀ (n : ℕ), Measurable (f n)) :
  ∫⁻ (x : α),
      Filter.liminf (fun n ↦ f n x)
        Filter.atTop ∂μ ≤
    Filter.liminf
      (fun n ↦ ∫⁻ (x : α), f n x ∂μ)
      Filter.atTop

Sequential Fatou lemma.

Proof for Theorem 10.3.1

uses 0

各 n に対して g_n:=\inf_{k\ge n}f_k とおく．すると g_n は非負可測で，g_1\le g_2\le \cdots かつ g_n \uparrow \liminf_{n\to\infty} f_n である．したがってTheorem 10.2.1より \int_X \liminf_{n\to\infty} f_n\,d\mu=\lim_{n\to\infty}\int_X g_n\,d\mu である．しかも各 n と各 k\ge n に対して g_n\le f_k だから Proposition 8.2.4より \int_X g_n\,d\mu\le \int_X f_k\,d\mu である．ゆえに \int_X g_n\,d\mu\le \inf_{k\ge n}\int_X f_k\,d\mu である．両辺で n\to\infty とすると

\int_X \liminf_{n\to\infty} f_n\,d\mu \le \lim_{n\to\infty}\inf_{k\ge n}\int_X f_k\,d\mu =\liminf_{n\to\infty}\int_X f_n\,d\mu.

Remark. Theorem 10.3.1は，「極限の積分は積分の極限以下とは限らないが，少なくとも (liminf) については不等式が成り立つ」という定理である． Theorem 10.4.1の証明でも重要な役割を果たす．

Remark (逆向きは一般には成り立たない). Fatouの補題の逆向きの不等式は，一般には成り立たない．例えば X=(0,1) にLebesgue測度を入れ，f_n:=n1_{(0,1/n)} とおく．このとき各 x\in(0,1) について十分大きな n では x\notin(0,1/n) だから，f_n(x)\to0 であり，したがって \liminf_{n\to\infty}f_n=0 である．よって \int_X \liminf_{n\to\infty}f_n\,d\lambda=0 である．一方で \int_X f_n\,d\lambda=n\lambda((0,1/n))=1 がすべての n について成り立つので，\liminf_{n\to\infty}\int_X f_n\,d\lambda=1 である．したがって逆向き \liminf_n\int_X f_n\,d\lambda\le\int_X\liminf_n f_n\,d\lambda は 1\le0 を主張することになり，成り立たない．これは，関数の質量が一点の近くへ集中して，点ごとの極限からは消えてしまう例である．