10.4. 優収束定理🔗

Theorem10.4.1

Statement uses 3

Statement dependency previews

Preview

Corollary 8.4.5

Loading preview

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

Used by 5

Reverse dependency previews

Preview

Corollary 10.4.2

Loading preview

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

✓L∃∀N

Tagsleanok

優収束定理. f_n\in M(X;\RR) (n\in\NN)，f\in M(X;\RR) とし，g\in\calL^1(X) かつ g\ge0 a.e. on X とする．もし f_n(x)\to f(x) a.e. on X かつ |f_n(x)|\le g(x) a.e. on X がすべての n について成り立つならば， f\in\calL^1(X) であり， \lim_{n\to\infty}\int_X f_n\,d\mu=\int_X f\,d\mu が成り立つ．

Lean code for Theorem10.4.1●2 theorems

theoremdefined in NoteKsk/«10limits».lean

complete

theorem NoteKsk.Chapter10.integrable_limit_of_dominated_convergence.{u_1, u_2}
  {α : Type u_1} {G : Type u_2} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α} [NormedAddCommGroup G] {F : ℕ → α → G}
  {f : α → G} {bound : α → ℝ}
  (hf_meas : MeasureTheory.AEStronglyMeasurable f μ)
  (hbound_int : MeasureTheory.Integrable bound μ)
  (hbound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖F n x‖ ≤ bound x)
  (hlim :
    ∀ᵐ (x : α) ∂μ,
      Filter.Tendsto (fun n ↦ F n x) Filter.atTop (nhds (f x))) :
  MeasureTheory.Integrable f μ

theorem NoteKsk.Chapter10.integrable_limit_of_dominated_convergence.{u_1,
    u_2}
  {α : Type u_1} {G : Type u_2}
  [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  [NormedAddCommGroup G] {F : ℕ → α → G}
  {f : α → G} {bound : α → ℝ}
  (hf_meas :
    MeasureTheory.AEStronglyMeasurable f
      μ)
  (hbound_int :
    MeasureTheory.Integrable bound μ)
  (hbound :
    ∀ (n : ℕ),
      ∀ᵐ (x : α) ∂μ, ‖F n x‖ ≤ bound x)
  (hlim :
    ∀ᵐ (x : α) ∂μ,
      Filter.Tendsto (fun n ↦ F n x)
        Filter.atTop (nhds (f x))) :
  MeasureTheory.Integrable f μ

The limit function in dominated convergence has finite integral.  We keep the
a.e. strong measurability of the limit as an explicit hypothesis, because this
is the way Bochner integrability is represented in mathlib.

theoremdefined in NoteKsk/«10limits».lean

complete

theorem NoteKsk.Chapter10.tendsto_integral_of_dominated_convergence.{u_1, u_2}
  {α : Type u_1} {G : Type u_2} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α} [NormedAddCommGroup G] [NormedSpace ℝ G]
  {F : ℕ → α → G} {f : α → G} (bound : α → ℝ)
  (hF_meas : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (F n) μ)
  (hbound_int : MeasureTheory.Integrable bound μ)
  (hbound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖F n x‖ ≤ bound 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_integral_of_dominated_convergence.{u_1,
    u_2}
  {α : Type u_1} {G : Type u_2}
  [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  [NormedAddCommGroup G] [NormedSpace ℝ G]
  {F : ℕ → α → G} {f : α → G}
  (bound : α → ℝ)
  (hF_meas :
    ∀ (n : ℕ),
      MeasureTheory.AEStronglyMeasurable
        (F n) μ)
  (hbound_int :
    MeasureTheory.Integrable bound μ)
  (hbound :
    ∀ (n : ℕ),
      ∀ᵐ (x : α) ∂μ, ‖F n x‖ ≤ bound 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 ∂μ))

Dominated convergence theorem for Bochner integrals.

The lecture statement is real-valued; this mathlib form works for functions
with values in any real normed additive group.

Proof for Theorem 10.4.1

uses 0

零集合上で値を変えても積分値は変わらないので，以下では g\ge0，f_n\to f，|f_n|\le g が各点で成り立つとしてよい．まず極限をとれば |f|\le g である．したがってCorollary 8.4.5より f は可積分である．

次に h_n:=|f_n-f| とおくと，h_n は非負可測で h_n\to 0 かつ 0\le h_n\le |f_n|+|f|\le 2g が成り立つ．ここで 2g-h_n \ge 0 なので Theorem 10.3.1 を \{2g-h_n\} に適用すると

\int_X \liminf_{n\to\infty}(2g-h_n)\,d\mu \le \liminf_{n\to\infty}\int_X (2g-h_n)\,d\mu.

左辺の integrand は a.e. で 2g に収束するから

2\int_X g\,d\mu \le \liminf_{n\to\infty}\left(2\int_X g\,d\mu-\int_X h_n\,d\mu\right).

すなわち

2\int_X g\,d\mu \le 2\int_X g\,d\mu-\limsup_{n\to\infty}\int_X h_n\,d\mu.

よって \limsup_{n\to\infty}\int_X h_n\,d\mu\le 0 である．各 \int_X h_n\,d\mu は非負だから \lim_{n\to\infty}\int_X h_n\,d\mu=0，すなわち \int_X |f_n-f|\,d\mu \to 0 である．

最後にProposition 9.3.3より

より \int_X f_n\,d\mu\to \int_X f\,d\mu を得る．

Corollary10.4.2

uses 1used by 0✓L∃∀N

L^1 収束版の優収束定理. Theorem 10.4.1と同じ仮定のもとで

\lim_{n\to\infty}\int_X |f_n-f|\,d\mu=0

が成り立つ．

Lean code for Corollary10.4.2●1 theorem

theoremdefined in NoteKsk/«10limits».lean

complete

theorem NoteKsk.Chapter10.tendsto_integral_of_dominated_convergence.{u_1, u_2}
  {α : Type u_1} {G : Type u_2} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α} [NormedAddCommGroup G] [NormedSpace ℝ G]
  {F : ℕ → α → G} {f : α → G} (bound : α → ℝ)
  (hF_meas : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (F n) μ)
  (hbound_int : MeasureTheory.Integrable bound μ)
  (hbound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖F n x‖ ≤ bound 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_integral_of_dominated_convergence.{u_1,
    u_2}
  {α : Type u_1} {G : Type u_2}
  [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  [NormedAddCommGroup G] [NormedSpace ℝ G]
  {F : ℕ → α → G} {f : α → G}
  (bound : α → ℝ)
  (hF_meas :
    ∀ (n : ℕ),
      MeasureTheory.AEStronglyMeasurable
        (F n) μ)
  (hbound_int :
    MeasureTheory.Integrable bound μ)
  (hbound :
    ∀ (n : ℕ),
      ∀ᵐ (x : α) ∂μ, ‖F n x‖ ≤ bound 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 ∂μ))

Dominated convergence theorem for Bochner integrals.

The lecture statement is real-valued; this mathlib form works for functions
with values in any real normed additive group.

Proof for Corollary 10.4.2

uses 0

Theorem 10.4.1の証明中で示した通りである．

Corollary10.4.3

uses 1used by 0✓L∃∀N

Tagsleanok

有界収束定理. \mu(X)<\infty とし， f_n\in M(X;\RR) (n\in\NN)，f\in M(X;\RR) とする．もし f_n(x)\to f(x) a.e. on X かつある定数 M>0 が存在して |f_n(x)|\le M a.e. on X がすべての n について成り立つならば， f\in\calL^1(X) で \int_X f_n\,d\mu\to \int_X f\,d\mu が成り立つ．

Lean code for Corollary10.4.3●1 theorem

theoremdefined in NoteKsk/«10limits».lean

complete

theorem NoteKsk.Chapter10.tendsto_integral_of_bounded_convergence.{u_1, u_2}
  {α : Type u_1} {G : Type u_2} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α} [NormedAddCommGroup G] [NormedSpace ℝ G]
  [MeasureTheory.IsFiniteMeasure μ] {F : ℕ → α → G} {f : α → G}
  (hF_meas : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (F n) μ)
  (hbound : ∃ C, ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖F n x‖ ≤ C)
  (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_integral_of_bounded_convergence.{u_1,
    u_2}
  {α : Type u_1} {G : Type u_2}
  [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  [NormedAddCommGroup G] [NormedSpace ℝ G]
  [MeasureTheory.IsFiniteMeasure μ]
  {F : ℕ → α → G} {f : α → G}
  (hF_meas :
    ∀ (n : ℕ),
      MeasureTheory.AEStronglyMeasurable
        (F n) μ)
  (hbound :
    ∃ C,
      ∀ (n : ℕ),
        ∀ᵐ (x : α) ∂μ, ‖F n x‖ ≤ C)
  (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 ∂μ))

Bounded convergence theorem on a finite measure space.

Proof for Corollary 10.4.3

uses 0

g:=M1_X とおくと g\ge0 かつ \int_X |g|\,d\mu=M\,\mu(X)<\infty だから g\in\calL^1(X) である．しかも a.e. で |f_n|\le g であるから，Theorem 10.4.1を適用すればよい．