Lebesgue積分講義ノート

7.8. 概収束🔗

Definition7.8.1
uses 1used by 1✓L∃∀N
Tagsleanok

概収束. 測度空間 (X,\calM,\mu) と E\in\calM を固定し， f_n,f:E\to\eRR とする． \{f_n\}_{n=1}^{\infty} が f に概収束する，または a.e. 収束するとは， ある \mu-零集合 N\in\calM が存在して，すべての x\in E\setminus N に対して数列 \{f_n(x)\}_{n=1}^{\infty} が \eRR の意味で f(x) に収束することをいう． このとき

f_n\to f \quad \mu\text{-a.e.\ on } E

と書く． つまり，

\{x\in E\mid f_n(x)\not\to f(x)\}

が \mu-零集合に含まれることをいう． 各 f_n や f を零集合上で変更しても，例外集合は可算和をとるだけなので， この条件は a.e. 同値類に対してもよく定義されている．

Lean code for Definition7.8.1●1 definition
  • defdefined in NoteKsk/Defs.lean
    complete
    def NoteKsk.AEConvergesOn.{u_1, u_2} {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [TopologicalSpace β] (μ : MeasureTheory.Measure α)
  (E : Set α) (f : ℕ → α → β) (g : α → β) : Prop
    def NoteKsk.AEConvergesOn.{u_1, u_2}
  {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [TopologicalSpace β]
  (μ : MeasureTheory.Measure α)
  (E : Set α) (f : ℕ → α → β)
  (g : α → β) : Prop

    Definition body

    def AEConvergesOn {α β : Type*} [MeasurableSpace α] [TopologicalSpace β]
    (μ : Measure α) (E : Set α) (f : ℕ → α → β) (g : α → β) : Prop :=
  ∀ᵐ x ∂ μ.restrict E, Filter.Tendsto (fun n : ℕ => f n x) Filter.atTop (𝓝 (g x))

/-! ## Lebesgue integral vocabulary -/
    Almost-everywhere convergence on a set.
Corollary7.8.2
Statement uses 3
Statement dependency previews
Preview
Proposition 7.6.4
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
used by 0✓L∃∀N
Tagsleanok

概収束の極限の可測性. (X,\calM,\mu) を完備な測度空間とし，E\in\calM とする． f_n\in M(E) (n\in\NN) とし，

f_n\to f\quad \mu\text{-a.e.\ on } E

とする． このとき f は \calM(E)-可測である．

Lean code for Corollary7.8.2●2 theorems
  • theoremdefined in NoteKsk/«07mble-funcs».lean
    complete
    theorem NoteKsk.Chapter07.measurable_of_ae_tendsto_real.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} [μ.IsComplete]
  {f : ℕ → α → ℝ} {g : α → ℝ} (hf : ∀ (n : ℕ), Measurable (f n))
  (hlim :
    ∀ᵐ (x : α) ∂μ,
      Filter.Tendsto (fun n ↦ f n x) Filter.atTop (nhds (g x))) :
  Measurable g
    theorem NoteKsk.Chapter07.measurable_of_ae_tendsto_real.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  [μ.IsComplete] {f : ℕ → α → ℝ}
  {g : α → ℝ}
  (hf : ∀ (n : ℕ), Measurable (f n))
  (hlim :
    ∀ᵐ (x : α) ∂μ,
      Filter.Tendsto (fun n ↦ f n x)
        Filter.atTop (nhds (g x))) :
  Measurable g
  • theoremdefined in NoteKsk/«07mble-funcs».lean
    complete
    theorem NoteKsk.Chapter07.measurable_of_ae_tendsto_ereal.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} [μ.IsComplete]
  {f : ℕ → α → EReal} {g : α → EReal} (hf : ∀ (n : ℕ), Measurable (f n))
  (hlim :
    ∀ᵐ (x : α) ∂μ,
      Filter.Tendsto (fun n ↦ f n x) Filter.atTop (nhds (g x))) :
  Measurable g
    theorem NoteKsk.Chapter07.measurable_of_ae_tendsto_ereal.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  [μ.IsComplete] {f : ℕ → α → EReal}
  {g : α → EReal}
  (hf : ∀ (n : ℕ), Measurable (f n))
  (hlim :
    ∀ᵐ (x : α) ∂μ,
      Filter.Tendsto (fun n ↦ f n x)
        Filter.atTop (nhds (g x))) :
  Measurable g
Proof for Corollary 7.8.2
uses 0

g:=\limsup_{n\to\infty}f_n

とおくと，Proposition 7.6.4を 可測空間 (E,\calM(E)) に適用して，g は \calM(E)-可測である． また極限が存在する点では

g(x)=\lim_{n\to\infty}f_n(x)=f(x)

である． したがって

f=g \quad \mu\text{-a.e.\ on } E.

ゆえにProposition 7.7.3より f は \calM(E)-可測である．