10.2. 単調収束定理🔗

Theorem10.2.1

uses 1

Used by 4

Reverse dependency previews

Preview

Corollary 10.2.2

Loading preview

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

✓L∃∀N

Tagsleanok

単調収束定理. f_n\in M^+(X) (n\in\NN) とする．もし f_1\le f_2\le \cdots ならば，各 x\in X に対して f(x):=\lim_{n\to\infty}f_n(x)=\sup_{n\in\NN}f_n(x) と定めることができる．このとき f\in M^+(X) であり， \int_X f_n\,d\mu \uparrow \int_X f\,d\mu，すなわち \lim_{n\to\infty}\int_X f_n\,d\mu=\int_X f\,d\mu が成り立つ．

Lean code for Theorem10.2.1●3 theorems

theoremdefined in NoteKsk/«10limits».lean

complete

theorem NoteKsk.Chapter10.monotone_convergence_lintegral.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α}
  {f : ℕ → α → ENNReal} (hf : ∀ (n : ℕ), Measurable (f n))
  (hmono : Monotone f) :
  ∫⁻ (x : α), ⨆ n, f n x ∂μ = ⨆ n, ∫⁻ (x : α), f n x ∂μ

theorem NoteKsk.Chapter10.monotone_convergence_lintegral.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {f : ℕ → α → ENNReal}
  (hf : ∀ (n : ℕ), Measurable (f n))
  (hmono : Monotone f) :
  ∫⁻ (x : α), ⨆ n, f n x ∂μ =
    ⨆ n, ∫⁻ (x : α), f n x ∂μ

Monotone convergence theorem for nonnegative functions, in `lintegral` form.

theoremdefined in NoteKsk/«10limits».lean

complete

theorem NoteKsk.Chapter10.monotone_convergence_lintegral_ae.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α}
  {f : ℕ → α → ENNReal} (hf : ∀ (n : ℕ), AEMeasurable (f n) μ)
  (hmono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x) :
  ∫⁻ (x : α), ⨆ n, f n x ∂μ = ⨆ n, ∫⁻ (x : α), f n x ∂μ

theorem NoteKsk.Chapter10.monotone_convergence_lintegral_ae.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {f : ℕ → α → ENNReal}
  (hf : ∀ (n : ℕ), AEMeasurable (f n) μ)
  (hmono :
    ∀ᵐ (x : α) ∂μ,
      Monotone fun n ↦ f n x) :
  ∫⁻ (x : α), ⨆ n, f n x ∂μ =
    ⨆ n, ∫⁻ (x : α), f n x ∂μ

Almost-everywhere measurable version of monotone convergence.  This is often
the most convenient form for later convergence arguments.

theoremdefined in NoteKsk/«10limits».lean

complete

theorem NoteKsk.Chapter10.tendsto_lintegral_of_monotone.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α}
  {f : ℕ → α → ENNReal} {F : α → ENNReal}
  (hf : ∀ (n : ℕ), AEMeasurable (f n) μ)
  (hmono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x)
  (hlim :
    ∀ᵐ (x : α) ∂μ,
      Filter.Tendsto (fun n ↦ f n x) Filter.atTop (nhds (F x))) :
  Filter.Tendsto (fun n ↦ ∫⁻ (x : α), f n x ∂μ) Filter.atTop
    (nhds (∫⁻ (x : α), F x ∂μ))

theorem NoteKsk.Chapter10.tendsto_lintegral_of_monotone.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {f : ℕ → α → ENNReal} {F : α → ENNReal}
  (hf : ∀ (n : ℕ), AEMeasurable (f n) μ)
  (hmono :
    ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x)
  (hlim :
    ∀ᵐ (x : α) ∂μ,
      Filter.Tendsto (fun n ↦ f n x)
        Filter.atTop (nhds (F x))) :
  Filter.Tendsto
    (fun n ↦ ∫⁻ (x : α), f n x ∂μ)
    Filter.atTop
    (nhds (∫⁻ (x : α), F x ∂μ))

Monotone convergence expressed as convergence of the integrals.

Proof for Theorem 10.2.1

uses 0

単調性より各 x\in X で \lim_{n\to\infty}f_n(x) が \eRR の意味で存在し，それは \sup_n f_n(x) に等しい．したがって f=\sup_n f_n であり，Proposition 7.6.3より f は可測である．また f\ge0 だから f\in M^+(X) である．

まず f_n \le f だからProposition 8.2.4より \int_X f_n\,d\mu\le \int_X f\,d\mu であり，列 \{\int_X f_n\,d\mu\} は拡大実数値の単調増加列である．したがって L:=\lim_{n\to\infty}\int_X f_n\,d\mu が存在して L\le \int_X f\,d\mu である．

逆向きの不等式を示す． s \le f を満たす任意の非負単関数 s=\sum_{j=1}^m a_j1_{A_j} を取る．ここで a_j\ge 0，A_j は互いに素な可測集合とする．任意の 0<\alpha<1 に対して B_{j,n}:=A_j \cap \{x \in X \mid f_n(x)\ge \alpha a_j\} とおく． f_n(x)\uparrow f(x)\ge a_j が A_j 上で成り立つので B_{j,1}\subset B_{j,2}\subset \cdots かつ \bigcup_{n=1}^{\infty}B_{j,n}=A_j である．

そこで u_n:=\sum_{j=1}^m \alpha a_j 1_{B_{j,n}} とおくと，u_n は非負単関数で u_n\le f_n が成り立つ．したがって \int_X u_n\,d\mu\le \int_X f_n\,d\mu\le L である．一方，測度の下からの連続性より \mu(B_{j,n})\to \mu(A_j) だから

\int_X u_n\,d\mu =\sum_{j=1}^m \alpha a_j \mu(B_{j,n}) \to \sum_{j=1}^m \alpha a_j \mu(A_j) =\alpha \int_X s\,d\mu.

よって \alpha \int_X s\,d\mu\le L である． \alpha \uparrow 1 とすれば \int_X s\,d\mu\le L である． s \le f を満たす単関数 s は任意だから，非負可測関数の積分の定義（Definition 8.2.1）より \int_X f\,d\mu\le L である．したがって \int_X f\,d\mu=L である．

Remark (単関数近似との関係). 本講義では積分の基本性質を早めに使うため，Theorem 8.2.3を先に直接証明した．しかし単調収束定理が得られた後では，これはその系としてただちに従う．実際，f\in M^+(X) とし，s_n\in S^+(X) が 0\le s_1\le s_2\le\cdots\le f かつ s_n\to f を満たすなら，Theorem 10.2.1より \int_X s_n\,d\mu\uparrow\int_X f\,d\mu である．これはまさにTheorem 8.2.3の主張である．

Remark (a.e. 版と \sup による表現). Theorem 10.2.1の単調性 f_n\le f_{n+1} は，各点ではなく a.e. on X の意味で仮定してよい．また極限関数も，各点収束極限ではなく a.e. 収束極限として与えられていてよい．より正確には，f_n\le f_{n+1} a.e. on X がすべての n について成り立ち，f_n\to f a.e. on X で，さらに f\in M^+(X) ならば，同じ結論 \int_X f_n\,d\mu\to\int_X f\,d\mu が成り立つ．

実際，単調性と収束がともに成り立つ点全体の外側を含む可測零集合を N とする． g_n を X\setminus N 上では f_n，N 上では 0 と定めると，g_n\in M^+(X)，g_1\le g_2\le\cdots，かつ g_n\to g:=\sup_n g_n が各点で成り立つ．単調収束定理より \int_X g_n\,d\mu\to\int_X g\,d\mu である．一方，g_n=f_n a.e. かつ g=f a.e. だから，非負関数の a.e. 不変性により \int_X f_n\,d\mu\to\int_X f\,d\mu である．なお，この議論は一般の測度空間では可測な代表 g について述べるのが自然であり，f 自体の可測性を結論したいときは f\in M^+(X) を仮定するか，完備性を用いて Corollary 7.8.2 を適用する．

最後に，単調列では各点で \lim_{n\to\infty}f_n=\sup_n f_n であるから，定理の極限は \lim の代わりに \sup と書いても同じである．

Corollary10.2.2

Statement uses 2

Statement dependency previews

Preview

Proposition 9.2.3

Loading preview

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

used by 0XL∃∀N

\calL^1 関数に対する単調収束定理（Beppo--Levi）. f_n\in\calL^1(X) (n\in\NN) とし，f_1\le f_2\le\cdots a.e. on X とする．もし \sup_n\int_X f_n\,d\mu<\infty ならば，ある f\in\calL^1(X) が存在して f_n\to f a.e. on X， \int_X f\,d\mu=\lim_{n\to\infty}\int_X f_n\,d\mu，かつ \int_X |f-f_n|\,d\mu\to0 が成り立つ．

Proof for Corollary 10.2.2

uses 0

可算個の例外集合をまとめ，零集合上で値を変えることで，はじめから f_1\le f_2\le\cdots が各点で成り立つとしてよい．この変更は a.e. 不変性により積分値を変えない．

h_n:=f_n-f_1 とおくと，h_n\in M^+(X) で h_1\le h_2\le\cdots である． h:=\sup_n h_n とおくと，Theorem 10.2.1より \int_X h\,d\mu=\lim_{n\to\infty}\int_X h_n\,d\mu =\lim_{n\to\infty}\int_X f_n\,d\mu-\int_X f_1\,d\mu<\infty である．したがってChebyshev不等式より h<\infty a.e. on X である． \{h=\infty\} 上で h を 0 に直した関数を \tilde h とおけば，\tilde h\in\calL^1(X) で \int_X \tilde h\,d\mu=\int_X h\,d\mu である．

f:=f_1+\tilde h と定めると f\in\calL^1(X) であり，f_n=f_1+h_n\to f_1+h=f a.e. on X である．さらに \int_X f\,d\mu=\int_X f_1\,d\mu+\int_X \tilde h\,d\mu =\lim_{n\to\infty}\int_X f_n\,d\mu である．最後に 0\le f-f_n a.e. だから， \int_X |f-f_n|\,d\mu=\int_X(f-f_n)\,d\mu =\int_X f\,d\mu-\int_X f_n\,d\mu\to0 である．

Corollary10.2.3

Statement uses 2

Statement dependency previews

Preview

Proposition 8.2.4

Loading preview

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

used by 0✓L∃∀N

Tagsleanok

非負級数の項別積分. f_n\in M^+(X) (n\in\NN) とする．このとき \int_X (\sum_{n=1}^{\infty}f_n)\,d\mu=\sum_{n=1}^{\infty}\int_X f_n\,d\mu が成り立つ．

Lean code for Corollary10.2.3●1 theorem

theoremdefined in NoteKsk/«10limits».lean

complete

theorem NoteKsk.Chapter10.lintegral_tsum.{u_1, u_2} {α : Type u_1}
  {ι : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α}
  {f : ι → α → ENNReal} [Countable ι]
  (hf : ∀ (i : ι), AEMeasurable (f i) μ) :
  ∫⁻ (x : α), ∑' (i : ι), f i x ∂μ = ∑' (i : ι), ∫⁻ (x : α), f i x ∂μ

theorem NoteKsk.Chapter10.lintegral_tsum.{u_1,
    u_2}
  {α : Type u_1} {ι : Type u_2}
  [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {f : ι → α → ENNReal} [Countable ι]
  (hf : ∀ (i : ι), AEMeasurable (f i) μ) :
  ∫⁻ (x : α), ∑' (i : ι), f i x ∂μ =
    ∑' (i : ι), ∫⁻ (x : α), f i x ∂μ

Termwise integration for nonnegative series.

Proof for Corollary 10.2.3

uses 0

部分和 S_N:=\sum_{n=1}^N f_n を考えると S_1\le S_2\le \cdots かつ S_N \uparrow \sum_{n=1}^{\infty}f_n である．したがってTheorem 10.2.1より \int_X (\sum_{n=1}^{\infty}f_n)\,d\mu=\lim_{N\to\infty}\int_X S_N\,d\mu である．一方，非負可測関数の有限和に関する線形性（Proposition 8.2.4）より \int_X S_N\,d\mu=\sum_{n=1}^N \int_X f_n\,d\mu である．よって

\int_X \left(\sum_{n=1}^{\infty}f_n\right)\,d\mu =\lim_{N\to\infty}\sum_{n=1}^N \int_X f_n\,d\mu =\sum_{n=1}^{\infty}\int_X f_n\,d\mu.