10.5. 項別積分🔗

Theorem10.5.1

Statement uses 2

Statement dependency previews

Preview

Corollary 9.4.3

Loading preview

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

used by 1✓L∃∀N

優収束定理による項別積分. f_n\in\calL^1(X) (n\in\NN) とする．さらに，ある g\in\calL^1(X) が存在して，g\ge0 a.e. on X かつ \sum_{n=1}^{\infty}|f_n(x)|\le g(x) a.e. on X を満たすとする．このとき級数 \sum_{n=1}^{\infty}f_n(x) は a.e. で絶対収束し，その和を f と書けば f\in\calL^1(X) で， \int_X f\,d\mu=\sum_{n=1}^{\infty}\int_X f_n\,d\mu が成り立つ．

Lean code for Theorem10.5.1●2 theorems

theoremdefined in NoteKsk/«10limits».lean

complete

theorem NoteKsk.Chapter10.hasSum_integral_of_dominated_convergence.{u_1, u_2,
    u_3}
  {α : Type u_1} {ι : Type u_2} {E : Type u_3} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [Countable ι] {F : ι → α → E} {f : α → E} (bound : ι → α → ℝ)
  (hF_meas : ∀ (n : ι), MeasureTheory.AEStronglyMeasurable (F n) μ)
  (hbound : ∀ (n : ι), ∀ᵐ (x : α) ∂μ, ‖F n x‖ ≤ bound n x)
  (hbound_summable : ∀ᵐ (x : α) ∂μ, Summable fun n ↦ bound n x)
  (hbound_int :
    MeasureTheory.Integrable (fun x ↦ ∑' (n : ι), bound n x) μ)
  (hsum : ∀ᵐ (x : α) ∂μ, HasSum (fun n ↦ F n x) (f x)) :
  HasSum (fun n ↦ ∫ (x : α), F n x ∂μ) (∫ (x : α), f x ∂μ)

theorem NoteKsk.Chapter10.hasSum_integral_of_dominated_convergence.{u_1,
    u_2, u_3}
  {α : Type u_1} {ι : Type u_2}
  {E : Type u_3} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  [Countable ι] {F : ι → α → E}
  {f : α → E} (bound : ι → α → ℝ)
  (hF_meas :
    ∀ (n : ι),
      MeasureTheory.AEStronglyMeasurable
        (F n) μ)
  (hbound :
    ∀ (n : ι),
      ∀ᵐ (x : α) ∂μ, ‖F n x‖ ≤ bound n x)
  (hbound_summable :
    ∀ᵐ (x : α) ∂μ,
      Summable fun n ↦ bound n x)
  (hbound_int :
    MeasureTheory.Integrable
      (fun x ↦ ∑' (n : ι), bound n x) μ)
  (hsum :
    ∀ᵐ (x : α) ∂μ,
      HasSum (fun n ↦ F n x) (f x)) :
  HasSum (fun n ↦ ∫ (x : α), F n x ∂μ)
    (∫ (x : α), f x ∂μ)

Termwise integration under a dominated summability hypothesis.

This is the mathlib `HasSum` form of the lecture theorem
`∫ (∑ f_n) = ∑ ∫ f_n`.

theoremdefined in NoteKsk/«10limits».lean

complete

theorem NoteKsk.Chapter10.integral_tsum_of_summable_integral_norm.{u_1, u_2,
    u_3}
  {α : Type u_1} {ι : Type u_2} {E : Type u_3} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [Countable ι] {F : ι → α → E}
  (hF_int : ∀ (i : ι), MeasureTheory.Integrable (F i) μ)
  (hF_sum : Summable fun i ↦ ∫ (x : α), ‖F i x‖ ∂μ) :
  ∑' (i : ι), ∫ (x : α), F i x ∂μ = ∫ (x : α), ∑' (i : ι), F i x ∂μ

theorem NoteKsk.Chapter10.integral_tsum_of_summable_integral_norm.{u_1,
    u_2, u_3}
  {α : Type u_1} {ι : Type u_2}
  {E : Type u_3} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  [Countable ι] {F : ι → α → E}
  (hF_int :
    ∀ (i : ι),
      MeasureTheory.Integrable (F i) μ)
  (hF_sum :
    Summable fun i ↦
      ∫ (x : α), ‖F i x‖ ∂μ) :
  ∑' (i : ι), ∫ (x : α), F i x ∂μ =
    ∫ (x : α), ∑' (i : ι), F i x ∂μ

A common sufficient condition for exchanging `tsum` and integral.

Proof for Theorem 10.5.1

uses 0

部分和 S_N:=\sum_{n=1}^N f_n を考える． a.e. で \sum_{n=1}^{\infty}|f_n(x)|\le g(x)<\infty だから，数列 \sum f_n(x) は a.e. で絶対収束する．その和の可測な代表を，例えば f:=\limsup_{N\to\infty} S_N と定めれば， S_N(x)\to f(x) a.e. である．

さらに三角不等式より a.e. で |S_N(x)|\le\sum_{n=1}^N |f_n(x)|\le\sum_{n=1}^{\infty}|f_n(x)|\le g(x) だから， Theorem 10.4.1より \int_X S_N\,d\mu\to \int_X f\,d\mu である．一方，有限和の線形性（Corollary 9.4.3）より \int_X S_N\,d\mu=\sum_{n=1}^N \int_X f_n\,d\mu である．したがって

\int_X f\,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.

Corollary10.5.2

Statement uses 2

Statement dependency previews

Preview

Theorem 10.2.1

Loading preview

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

used by 0✓L∃∀N

L^1 絶対収束級数の項別積分. f_n\in\calL^1(X) (n\in\NN) とし， \sum_{n=1}^{\infty}\int_X |f_n|\,d\mu<\infty とする．このとき \sum_{n=1}^{\infty}f_n(x) は a.e. で絶対収束する．その和を f と書けば，f\in\calL^1(X) で， \sum_{n=1}^N f_n\to f in L^1 かつ \int_X f\,d\mu=\sum_{n=1}^{\infty}\int_X f_n\,d\mu が成り立つ．

Lean code for Corollary10.5.2●2 theorems

theoremdefined in NoteKsk/«10limits».lean

complete

theorem NoteKsk.Chapter10.integral_tsum_eq_tsum_integral_of_summable_integral_norm.{u_1,
    u_2, u_3}
  {α : Type u_1} {ι : Type u_2} {E : Type u_3} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [Countable ι] {F : ι → α → E}
  (hF_int : ∀ (i : ι), MeasureTheory.Integrable (F i) μ)
  (hF_sum : Summable fun i ↦ ∫ (x : α), ‖F i x‖ ∂μ) :
  ∫ (x : α), ∑' (i : ι), F i x ∂μ = ∑' (i : ι), ∫ (x : α), F i x ∂μ

theorem NoteKsk.Chapter10.integral_tsum_eq_tsum_integral_of_summable_integral_norm.{u_1,
    u_2, u_3}
  {α : Type u_1} {ι : Type u_2}
  {E : Type u_3} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  [Countable ι] {F : ι → α → E}
  (hF_int :
    ∀ (i : ι),
      MeasureTheory.Integrable (F i) μ)
  (hF_sum :
    Summable fun i ↦
      ∫ (x : α), ‖F i x‖ ∂μ) :
  ∫ (x : α), ∑' (i : ι), F i x ∂μ =
    ∑' (i : ι), ∫ (x : α), F i x ∂μ

The same theorem in the lecture-note orientation: the integration functional
commutes with absolutely summable `L¹` series.

theoremdefined in NoteKsk/«10limits».lean

complete

theorem NoteKsk.Chapter10.integral_tsum_of_summable_integral_norm.{u_1, u_2,
    u_3}
  {α : Type u_1} {ι : Type u_2} {E : Type u_3} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [Countable ι] {F : ι → α → E}
  (hF_int : ∀ (i : ι), MeasureTheory.Integrable (F i) μ)
  (hF_sum : Summable fun i ↦ ∫ (x : α), ‖F i x‖ ∂μ) :
  ∑' (i : ι), ∫ (x : α), F i x ∂μ = ∫ (x : α), ∑' (i : ι), F i x ∂μ

theorem NoteKsk.Chapter10.integral_tsum_of_summable_integral_norm.{u_1,
    u_2, u_3}
  {α : Type u_1} {ι : Type u_2}
  {E : Type u_3} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  [Countable ι] {F : ι → α → E}
  (hF_int :
    ∀ (i : ι),
      MeasureTheory.Integrable (F i) μ)
  (hF_sum :
    Summable fun i ↦
      ∫ (x : α), ‖F i x‖ ∂μ) :
  ∑' (i : ι), ∫ (x : α), F i x ∂μ =
    ∫ (x : α), ∑' (i : ι), F i x ∂μ

A common sufficient condition for exchanging `tsum` and integral.

Proof for Corollary 10.5.2

uses 0

g_N:=\sum_{n=1}^N |f_n| とおく． g_N は非負可測で g_N\le g_{N+1} だから， Theorem 10.2.1より g:=\sup_N g_N=\sum_{n=1}^{\infty}|f_n| は可測で， \int_X g\,d\mu=\lim_{N\to\infty}\sum_{n=1}^N\int_X |f_n|\,d\mu<\infty である．したがって g<\infty a.e. である．零集合 \{g=\infty\} 上で g を 0 に直した関数を \tilde g とおけば，\tilde g\in\calL^1(X) である．よって \sum_n f_n(x) は a.e. で絶対収束する．

また \sum_n |f_n(x)|\le\tilde g(x) a.e. であるから， Theorem 10.5.1より f\in\calL^1(X) かつ \int_X f\,d\mu=\sum_n\int_X f_n\,d\mu である．さらに a.e. で |f-\sum_{n=1}^N f_n|\le\sum_{n>N}|f_n| だから，

\int_X\left|f-\sum_{n=1}^N f_n\right|\,d\mu \le\sum_{n>N}\int_X |f_n|\,d\mu\to0.

したがって \sum_{n=1}^N f_n\to f in L^1 である．

Remark (項別積分の関数空間論・作用素論的な見方). 非負項級数ならCorollary 10.2.3で，符号が混ざる級数でも絶対値で支配されていればTheorem 10.5.1で，項別積分が正当化される．これが「和と積分の交換」の基本形である．

関数空間論の言葉で言えば，積分は L^1(X) 上の線形汎関数である．実際，I([h]):=\int_X h\,d\mu とおくと，|I([h])|\le\|[h]\|_1 であるから，I:L^1(X)\to\RR は有界線形作用素である．もし \sum_n\|[f_n]\|_1<\infty なら，Corollary 10.5.2より部分和は L^1 である [f] に収束し， I(\sum_n[f_n])=\sum_n I([f_n]) が成り立つ．これは「有界線形作用素は十分よく収束する級数と交換できる」という，第14章で扱う有界線形作用素の基本原理の最初の例である．

具体的には，第14章の積分型線形汎関数 f\mapsto\int_0^1 f(x)\,dx や積分作用素 (Tf)(x):=\int_0^x f(t)\,dt はこの見方の典型である．例えば f_n\in C([0,1]) かつ \sum_n\|f_n\|_\infty<\infty なら，各 x\in[0,1] で (T\sum_n f_n)(x)=\sum_n(Tf_n)(x) である．実際，\sum_n|f_n(t)|\le\sum_n\|f_n\|_\infty が可積分な定数で支配するので，項別積分を [0,x] 上で適用すればよい．また第13章のFourier関数系では，Fourier係数 f\mapsto\int f e_k\,d\mu も積分型線形汎関数であり，支配条件の下で級数のFourier係数を項別に計算できる．さらに第12章の Riesz--Fischer の証明でも，差の級数を可積分な級数で制御して極限を作るという同じ考え方が使われる．