Lebesgue積分講義ノート

8.2. 非負可測関数の積分🔗

Definition8.2.1
uses 1
Used by 5
Reverse dependency previews
Preview
Lemma 8.2.2
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N
Tagsleanok

非負可測関数の積分. 非負可測関数 f\in M^+(X) に対して

\int_X f\,d\mu := \sup\left\{\int_X s\,d\mu \;\middle|\; s\in S^+(X),\ 0 \le s \le f\right\}

と定める．

Lean code for Definition8.2.1●2 declarations
  • abbrevdefined in NoteKsk/Defs.lean
    complete
    abbrev NoteKsk.lintegralNN.{u_1} {α : Type u_1} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α) (f : α → ENNReal) : ENNReal
    abbrev NoteKsk.lintegralNN.{u_1} {α : Type u_1}
  [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  (f : α → ENNReal) : ENNReal

    Definition body

    noncomputable abbrev lintegralNN {α : Type*} [MeasurableSpace α]
    (μ : Measure α) (f : α → ENNReal) : ENNReal :=
  ∫⁻ x, f x ∂μ
    The lower Lebesgue integral of an `ENNReal`-valued function.
  • theoremdefined in NoteKsk/«08lintegral».lean
    complete
    theorem NoteKsk.Chapter08.lintegralNN_def.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} (f : α → ENNReal) :
  NoteKsk.lintegralNN μ f =
    ⨆ g, ⨆ (_ : ⇑g ≤ f), MeasureTheory.SimpleFunc.lintegral g μ
    theorem NoteKsk.Chapter08.lintegralNN_def.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  (f : α → ENNReal) :
  NoteKsk.lintegralNN μ f =
    ⨆ g,
      ⨆ (_ : ⇑g ≤ f),
        MeasureTheory.SimpleFunc.lintegral
          g μ

Remark. この定義は構成的でなく，具体的な計算法は示されていない． 以下に述べる単関数近似はLebesgue積分の具体的な計算法（構成）を与える． これはLebesgue積分が俗に「横切り」の積分と説明される所以である． 単関数近似自体は後述の単調収束定理の系であり，計算法としても非常にナイーブで効率が悪い．実用的にはより効率的な数値積分アルゴリズムが多数考案されている．

Lemma8.2.2
uses 1used by 1✓L∃∀N
Tagsleanok

単関数による近似. 任意の f\in M^+(X) に対して， S^+(X) の列 \{s_n\}_{n=1}^{\infty} で 0 \le s_1 \le s_2 \le \cdots \le f かつ s_n(x) \to f(x) (x \in X) を満たすものが存在する．

Lean code for Lemma8.2.2●4 theorems
  • theoremdefined in NoteKsk/«08lintegral».lean
    complete
    theorem NoteKsk.Chapter08.monotone_eapprox.{u_1} {α : Type u_1}
  [MeasurableSpace α] (f : α → ENNReal) :
  Monotone (MeasureTheory.SimpleFunc.eapprox f)
    theorem NoteKsk.Chapter08.monotone_eapprox.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  (f : α → ENNReal) :
  Monotone
    (MeasureTheory.SimpleFunc.eapprox f)
  • theoremdefined in NoteKsk/«08lintegral».lean
    complete
    theorem NoteKsk.Chapter08.iSup_eapprox_apply.{u_1} {α : Type u_1}
  [MeasurableSpace α] {f : α → ENNReal} (hf : Measurable f) (x : α) :
  ⨆ n, (MeasureTheory.SimpleFunc.eapprox f n) x = f x
    theorem NoteKsk.Chapter08.iSup_eapprox_apply.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {f : α → ENNReal} (hf : Measurable f)
  (x : α) :
  ⨆ n,
      (MeasureTheory.SimpleFunc.eapprox f
          n)
        x =
    f x
  • theoremdefined in NoteKsk/«08lintegral».lean
    complete
    theorem NoteKsk.Chapter08.iSup_coe_eapprox.{u_1} {α : Type u_1}
  [MeasurableSpace α] {f : α → ENNReal} (hf : Measurable f) :
  ⨆ n, ⇑(MeasureTheory.SimpleFunc.eapprox f n) = f
    theorem NoteKsk.Chapter08.iSup_coe_eapprox.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {f : α → ENNReal} (hf : Measurable f) :
  ⨆ n,
      ⇑(MeasureTheory.SimpleFunc.eapprox f
          n) =
    f
  • theoremdefined in NoteKsk/«08lintegral».lean
    complete
    theorem NoteKsk.Chapter08.exists_monotone_simpleFunc_approx.{u_1} {α : Type u_1}
  [MeasurableSpace α] {f : α → ENNReal} (hf : Measurable f) :
  ∃ s,
    Monotone s ∧
      (∀ (n : ℕ) (x : α), (s n) x ≤ f x) ∧ ∀ (x : α), ⨆ n, (s n) x = f x
    theorem NoteKsk.Chapter08.exists_monotone_simpleFunc_approx.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {f : α → ENNReal} (hf : Measurable f) :
  ∃ s,
    Monotone s ∧
      (∀ (n : ℕ) (x : α), (s n) x ≤ f x) ∧
        ∀ (x : α), ⨆ n, (s n) x = f x
Proof for Lemma 8.2.2
uses 0

各 n \in \NN に対して

s_n(x) := \begin{cases} \dfrac{k}{2^n} &\left( \dfrac{k}{2^n} \le f(x) < \dfrac{k+1}{2^n}, \ \ 0 \le k \le n2^n-1 \right),\\[1.2ex] n & (f(x)\ge n) \end{cases}

と定める． すると s_n は有限個の値しかとらず， 各値をとる集合は \{x \in X \mid k/2^n \le f(x) < (k+1)/2^n\} または \{x \in X \mid f(x)\ge n\} の形で書けるので可測である． したがって s_n は単関数である．

また定義から 0 \le s_n(x) \le f(x) が成り立つ． さらに，f(x)<\infty のとき n>f(x) なら 0 \le f(x)-s_n(x)<2^{-n} であり， f(x)=\infty のときは s_n(x)=n \to \infty である． したがって s_n(x)\to f(x) である．

最後に，二進展開の精度が上がるので s_n(x)\le s_{n+1}(x) が成り立つ． よって所望の単関数列を得る．

Theorem8.2.3
Statement uses 2
Statement dependency previews
Preview
Definition 8.2.1
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
used by 1✓L∃∀N
Tagsleanok

非負可測関数の積分は単関数近似の極限. f\in M^+(X) とし， s_n\in S^+(X) を 0 \le s_1 \le s_2 \le \cdots \le f かつ s_n \to f を満たす単関数列とする． このとき \int_X f\,d\mu=\lim_{n\to\infty}\int_X s_n\,d\mu が成り立つ．

Lean code for Theorem8.2.3●3 theorems
  • theoremdefined in NoteKsk/«08lintegral».lean
    complete
    theorem NoteKsk.Chapter08.lintegralNN_eq_iSup_eapprox_lintegral.{u_1}
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α}
  {f : α → ENNReal} (hf : Measurable f) :
  NoteKsk.lintegralNN μ f =
    ⨆ n, (MeasureTheory.SimpleFunc.eapprox f n).lintegral μ
    theorem NoteKsk.Chapter08.lintegralNN_eq_iSup_eapprox_lintegral.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {f : α → ENNReal} (hf : Measurable f) :
  NoteKsk.lintegralNN μ f =
    ⨆ n,
      (MeasureTheory.SimpleFunc.eapprox f
            n).lintegral
        μ
  • theoremdefined in NoteKsk/«08lintegral».lean
    complete
    theorem NoteKsk.Chapter08.lintegral_iSup_of_measurable.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α}
  {f : ℕ → α → ENNReal} (hf : ∀ (n : ℕ), Measurable (f n))
  (hmono : Monotone f) :
  (NoteKsk.lintegralNN μ fun x ↦ ⨆ n, f n x) =
    ⨆ n, NoteKsk.lintegralNN μ (f n)
    theorem NoteKsk.Chapter08.lintegral_iSup_of_measurable.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {f : ℕ → α → ENNReal}
  (hf : ∀ (n : ℕ), Measurable (f n))
  (hmono : Monotone f) :
  (NoteKsk.lintegralNN μ fun x ↦
      ⨆ n, f n x) =
    ⨆ n, NoteKsk.lintegralNN μ (f n)
  • theoremdefined in NoteKsk/«08lintegral».lean
    complete
    theorem NoteKsk.Chapter08.lintegral_iSup_of_aeMeasurable.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α}
  {f : ℕ → α → ENNReal} (hf : ∀ (n : ℕ), AEMeasurable (f n) μ)
  (hmono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x) :
  (NoteKsk.lintegralNN μ fun x ↦ ⨆ n, f n x) =
    ⨆ n, NoteKsk.lintegralNN μ (f n)
    theorem NoteKsk.Chapter08.lintegral_iSup_of_aeMeasurable.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {f : ℕ → α → ENNReal}
  (hf : ∀ (n : ℕ), AEMeasurable (f n) μ)
  (hmono :
    ∀ᵐ (x : α) ∂μ,
      Monotone fun n ↦ f n x) :
  (NoteKsk.lintegralNN μ fun x ↦
      ⨆ n, f n x) =
    ⨆ n, NoteKsk.lintegralNN μ (f n)
Proof for Theorem 8.2.3
uses 0

各 n について s_n \le f だから， 定義より \int_X s_n\,d\mu \le \int_X f\,d\mu である． また s_n \le s_{n+1} だから，単関数の単調性より \int_X s_n\,d\mu \le \int_X s_{n+1}\,d\mu である． したがって列 \{\int_X s_n\,d\mu\}_{n=1}^{\infty} は単調増加であり， L:=\lim_{n\to\infty}\int_X s_n\,d\mu が存在して L \le \int_X f\,d\mu である．

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

そこで u_n^{(\alpha)}:=\sum_{j=1}^m \alpha a_j 1_{A_{j,n}^{(\alpha)}} とおくと，u_n^{(\alpha)} は非負単関数であり， A_{j,n}^{(\alpha)} 上では \alpha a_j \le s_n だから u_n^{(\alpha)} \le s_n が成り立つ． したがって \int_X u_n^{(\alpha)}\,d\mu \le \int_X s_n\,d\mu \le L である．

一方，測度の下からの連続性より \mu(A_{j,n}^{(\alpha)}) \to \mu(A_j) であるから，

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

よって \alpha\int_X t\,d\mu \le L である． \alpha \uparrow 1 とすれば \int_X t\,d\mu \le L である． t \le f を満たす単関数 t は任意であったから， 定義より \int_X f\,d\mu \le L である．以上より \int_X f\,d\mu=L が従う．

Proposition8.2.4
Statement uses 2
Statement dependency previews
Preview
Proposition 8.1.5
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
Used by 5
Reverse dependency previews
Preview
Proposition 8.2.6
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N
Tagsleanok

非負可測関数の基本性質. f,g\in M^+(X) と c \ge 0 に対して次が成り立つ．

  • \int_X (f+g)\,d\mu = \int_X f\,d\mu + \int_X g\,d\mu

  • \int_X cf\,d\mu = c\int_X f\,d\mu

  • f \le g なら \int_X f\,d\mu \le \int_X g\,d\mu

Lean code for Proposition8.2.4●3 theorems
  • theoremdefined in NoteKsk/«08lintegral».lean
    complete
    theorem NoteKsk.Chapter08.lintegralNN_add.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ENNReal}
  (hf : Measurable f) :
  (NoteKsk.lintegralNN μ fun x ↦ f x + g x) =
    NoteKsk.lintegralNN μ f + NoteKsk.lintegralNN μ g
    theorem NoteKsk.Chapter08.lintegralNN_add.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {f g : α → ENNReal}
  (hf : Measurable f) :
  (NoteKsk.lintegralNN μ fun x ↦
      f x + g x) =
    NoteKsk.lintegralNN μ f +
      NoteKsk.lintegralNN μ g
  • theoremdefined in NoteKsk/«08lintegral».lean
    complete
    theorem NoteKsk.Chapter08.lintegralNN_const_mul.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ENNReal}
  (c : ENNReal) (hf : Measurable f) :
  (NoteKsk.lintegralNN μ fun x ↦ c * f x) = c * NoteKsk.lintegralNN μ f
    theorem NoteKsk.Chapter08.lintegralNN_const_mul.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {f : α → ENNReal} (c : ENNReal)
  (hf : Measurable f) :
  (NoteKsk.lintegralNN μ fun x ↦
      c * f x) =
    c * NoteKsk.lintegralNN μ f
  • theoremdefined in NoteKsk/«08lintegral».lean
    complete
    theorem NoteKsk.Chapter08.lintegralNN_mono.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ENNReal}
  (hfg : f ≤ g) : NoteKsk.lintegralNN μ f ≤ NoteKsk.lintegralNN μ g
    theorem NoteKsk.Chapter08.lintegralNN_mono.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {f g : α → ENNReal} (hfg : f ≤ g) :
  NoteKsk.lintegralNN μ f ≤
    NoteKsk.lintegralNN μ g
Proof for Proposition 8.2.4
uses 0

単関数列 s_n \uparrow f，t_n \uparrow g を取る． すると s_n+t_n \uparrow f+g，cs_n \uparrow cf である． したがってthm:nonnegative-integral-simple-approximation,prop:simple-function-integral-basicより

\int_X (f+g)\,d\mu =\lim_{n\to\infty}\int_X (s_n+t_n)\,d\mu =\lim_{n\to\infty}\left(\int_X s_n\,d\mu+\int_X t_n\,d\mu\right) =\int_X f\,d\mu+\int_X g\,d\mu,

および \int_X cf\,d\mu=\lim_{n\to\infty}\int_X cs_n\,d\mu =\lim_{n\to\infty} c\int_X s_n\,d\mu=c\int_X f\,d\mu を得る．

また f\le g なら，f 以下の非負単関数はすべて g 以下でもある． したがって上限をとれば \int_X f\,d\mu\le \int_X g\,d\mu であり，(3) が従う．

Definition8.2.5
uses 1
Used by 3
Reverse dependency previews
Preview
Proposition 8.2.6
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N
Tagsleanok

部分集合上の積分. A \subset X を可測集合とする． 非負可測関数 f\in M^+(X) に対して \int_A f\,d\mu := \int_X f1_A\,d\mu と定める． 符号付可測関数の場合も同様に定める．

Lean code for Definition8.2.5●2 declarations
  • abbrevdefined in NoteKsk/Defs.lean
    complete
    abbrev NoteKsk.setLintegralNN.{u_1} {α : Type u_1} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α) (s : Set α) (f : α → ENNReal) : ENNReal
    abbrev NoteKsk.setLintegralNN.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  (s : Set α) (f : α → ENNReal) : ENNReal

    Definition body

    noncomputable abbrev setLintegralNN {α : Type*} [MeasurableSpace α]
    (μ : Measure α) (s : Set α) (f : α → ENNReal) : ENNReal :=
  ∫⁻ x in s, f x ∂μ
    The lower Lebesgue integral over a subset.
  • theoremdefined in NoteKsk/«08lintegral».lean
    complete
    theorem NoteKsk.Chapter08.setLintegralNN_eq_indicator.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} {A : Set α}
  (hA : MeasurableSet A) (f : α → ENNReal) :
  NoteKsk.setLintegralNN μ A f = NoteKsk.lintegralNN μ (A.indicator f)
    theorem NoteKsk.Chapter08.setLintegralNN_eq_indicator.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {A : Set α} (hA : MeasurableSet A)
  (f : α → ENNReal) :
  NoteKsk.setLintegralNN μ A f =
    NoteKsk.lintegralNN μ (A.indicator f)
Proposition8.2.6
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 2
Reverse dependency previews
Preview
Proposition 8.3.2
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N
Tagsleanok

集合に関する加法性. A,B \subset X を互いに素な可測集合とし， f\in M^+(X) とする． このとき \int_{A \sqcup B} f\,d\mu=\int_A f\,d\mu+\int_B f\,d\mu が成り立つ．

Lean code for Proposition8.2.6●1 theorem
  • theoremdefined in NoteKsk/«08lintegral».lean
    complete
    theorem NoteKsk.Chapter08.setLintegralNN_disjoint_union.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} {A B : Set α}
  (hB : MeasurableSet B) (hAB : Disjoint A B) (f : α → ENNReal) :
  NoteKsk.setLintegralNN μ (A ∪ B) f =
    NoteKsk.setLintegralNN μ A f + NoteKsk.setLintegralNN μ B f
    theorem NoteKsk.Chapter08.setLintegralNN_disjoint_union.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {A B : Set α} (hB : MeasurableSet B)
  (hAB : Disjoint A B) (f : α → ENNReal) :
  NoteKsk.setLintegralNN μ (A ∪ B) f =
    NoteKsk.setLintegralNN μ A f +
      NoteKsk.setLintegralNN μ B f
Proof for Proposition 8.2.6
uses 0

1_{A \sqcup B}=1_A+1_B だから，非負可測関数の加法性より

\int_{A \sqcup B} f\,d\mu =\int_X f1_{A \sqcup B}\,d\mu =\int_X f1_A\,d\mu+\int_X f1_B\,d\mu =\int_A f\,d\mu+\int_B f\,d\mu.