8.4. 実数値符号付可測関数の積分🔗

Definition8.4.1

uses 1

Used by 2

Reverse dependency previews

Preview

Definition 8.4.2

Loading preview

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

✓L∃∀N

Tagsleanok

正部分と負部分. f\in M(X;\RR) に対して f^+:=\max(f,0)，f^-:=\max(-f,0) を f の正部分，負部分という．

Lean code for Definition8.4.1●4 declarations

abbrevdefined in NoteKsk/Defs.lean

complete

abbrev NoteKsk.positivePart.{u_1} {α : Type u_1} (f : α → ℝ) : α → ENNReal

abbrev NoteKsk.positivePart.{u_1} {α : Type u_1}
  (f : α → ℝ) : α → ENNReal

Definition body

noncomputable abbrev positivePart {α : Type*} (f : α → ℝ) : α → ENNReal :=
  fun x => ENNReal.ofReal (f x)

Positive part of a real-valued function, represented as an `ENNReal`-valued function.

abbrevdefined in NoteKsk/Defs.lean

complete

abbrev NoteKsk.negativePart.{u_1} {α : Type u_1} (f : α → ℝ) : α → ENNReal

abbrev NoteKsk.negativePart.{u_1} {α : Type u_1}
  (f : α → ℝ) : α → ENNReal

Definition body

noncomputable abbrev negativePart {α : Type*} (f : α → ℝ) : α → ENNReal :=
  fun x => ENNReal.ofReal (-f x)

Negative part of a real-valued function, represented as an `ENNReal`-valued function.

theoremdefined in NoteKsk/«08lintegral».lean

complete

theorem NoteKsk.Chapter08.positivePart_measurable.{u_1} {α : Type u_1}
  [MeasurableSpace α] {f : α → ℝ} (hf : Measurable f) :
  Measurable (NoteKsk.positivePart f)

theorem NoteKsk.Chapter08.positivePart_measurable.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {f : α → ℝ} (hf : Measurable f) :
  Measurable (NoteKsk.positivePart f)

theoremdefined in NoteKsk/«08lintegral».lean

complete

theorem NoteKsk.Chapter08.negativePart_measurable.{u_1} {α : Type u_1}
  [MeasurableSpace α] {f : α → ℝ} (hf : Measurable f) :
  Measurable (NoteKsk.negativePart f)

theorem NoteKsk.Chapter08.negativePart_measurable.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {f : α → ℝ} (hf : Measurable f) :
  Measurable (NoteKsk.negativePart f)

Remark. 常に f=f^+-f^-，|f|=f^++f^- が成り立つ．したがって符号付関数の積分は，非負関数の積分に帰着できる．

Definition8.4.2

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 3

Reverse dependency previews

Preview

Proposition 8.4.3

Loading preview

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

✓L∃∀N

Tagsleanok

可積分関数. f\in M(X;\RR) が可積分であるとは， \int_X f^+\,d\mu<\infty かつ \int_X f^-\,d\mu<\infty が成り立つことをいう．このとき \int_X f\,d\mu:=\int_X f^+\,d\mu-\int_X f^-\,d\mu で定める．可積分関数全体を \calL^1(X) と書く．測度を明示したいときは \calL^1(X,\mu) と書く．

Lean code for Definition8.4.2●4 declarations

abbrevdefined in NoteKsk/Defs.lean

complete

abbrev NoteKsk.LebesgueIntegrable.{u_1} {α : Type u_1} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α) (f : α → ℝ) : Prop

abbrev NoteKsk.LebesgueIntegrable.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  (f : α → ℝ) : Prop

Definition body

abbrev LebesgueIntegrable {α : Type*} [MeasurableSpace α]
    (μ : Measure α) (f : α → ℝ) : Prop :=
  Integrable f μ

Lecture-note synonym for mathlib's Bochner integrability of real-valued functions.

abbrevdefined in NoteKsk/Defs.lean

complete

abbrev NoteKsk.lebesgueIntegral.{u_1} {α : Type u_1} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α) (f : α → ℝ) : ℝ

abbrev NoteKsk.lebesgueIntegral.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  (f : α → ℝ) : ℝ

Definition body

noncomputable abbrev lebesgueIntegral {α : Type*} [MeasurableSpace α]
    (μ : Measure α) (f : α → ℝ) : ℝ :=
  ∫ x, f x ∂μ

The signed Lebesgue integral of a real-valued integrable function.

theoremdefined in NoteKsk/«08lintegral».lean

complete

theorem NoteKsk.Chapter08.integral_eq_positivePart_sub_negativePart.{u_1}
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α}
  {f : α → ℝ} (hf : MeasureTheory.Integrable f μ) :
  ∫ (x : α), f x ∂μ =
    (∫⁻ (x : α), NoteKsk.positivePart f x ∂μ).toReal -
      (∫⁻ (x : α), NoteKsk.negativePart f x ∂μ).toReal

theorem NoteKsk.Chapter08.integral_eq_positivePart_sub_negativePart.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {f : α → ℝ}
  (hf : MeasureTheory.Integrable f μ) :
  ∫ (x : α), f x ∂μ =
    (∫⁻ (x : α),
          NoteKsk.positivePart f
            x ∂μ).toReal -
      (∫⁻ (x : α),
          NoteKsk.negativePart f
            x ∂μ).toReal

theoremdefined in NoteKsk/«08lintegral».lean

complete

theorem NoteKsk.Chapter08.lebesgueIntegral_eq_integral.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} (f : α → ℝ) :
  NoteKsk.lebesgueIntegral μ f = ∫ (x : α), f x ∂μ

theorem NoteKsk.Chapter08.lebesgueIntegral_eq_integral.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  (f : α → ℝ) :
  NoteKsk.lebesgueIntegral μ f =
    ∫ (x : α), f x ∂μ

Remark. \infty-\infty は定義しないので，正部分と負部分の両方が有限であるときにだけ符号付関数の積分を定義する．この条件は，後で見るように \int_X |f|\,d\mu<\infty と同値である．

Remark (Bochner積分との関係). この講義ではまず，教科書でよく採用される f^+ と f^- に分ける方法で実数値関数の積分を定義している．これは符号付き関数を非負関数の積分に帰着する自然な定義である．

一方で，後で関数解析を扱うと，実数値関数だけでなく \RR^n 値や，さらに一般のノルムをもつ線形空間に値をとる関数の積分も必要になる．そのような広い枠組みでは，正部分・負部分に分ける代わりに，ノルム \|f(x)\| が可積分であることを仮定して積分を定める．この積分をBochner積分という．

Bochner積分は無限次元のBanach空間値関数まで含むが， Banach空間はまだ本講義では扱っていない．この段階では，分からない場合は単に「実数値の符号付き関数」または「有限次元ベクトル値関数」の積分だと思って読めばよい．実数値関数については，Bochner積分は上で定義した f^+-f^- によるLebesgue積分と一致する．

Proposition8.4.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 1✓L∃∀N

表示の独立性. f=u-v=u'-v' と書け， u,v,u',v' がすべて非負可測で \int_X u\,d\mu,\ \int_X v\,d\mu,\ \int_X u'\,d\mu,\ \int_X v'\,d\mu<\infty とする．このとき \int_X u\,d\mu-\int_X v\,d\mu=\int_X u'\,d\mu-\int_X v'\,d\mu が成り立つ．

Lean code for Proposition8.4.3●1 theorem

theoremdefined in NoteKsk/«09lintegral-prop».lean

complete

theorem NoteKsk.Chapter09.integral_eq_sub_of_ae_eq_sub.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f u v : α → ℝ}
  (hu : MeasureTheory.Integrable u μ)
  (hv : MeasureTheory.Integrable v μ)
  (hfg : f =ᵐ[μ] fun x ↦ u x - v x) :
  ∫ (x : α), f x ∂μ = ∫ (x : α), u x ∂μ - ∫ (x : α), v x ∂μ

theorem NoteKsk.Chapter09.integral_eq_sub_of_ae_eq_sub.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {f u v : α → ℝ}
  (hu : MeasureTheory.Integrable u μ)
  (hv : MeasureTheory.Integrable v μ)
  (hfg : f =ᵐ[μ] fun x ↦ u x - v x) :
  ∫ (x : α), f x ∂μ =
    ∫ (x : α), u x ∂μ - ∫ (x : α), v x ∂μ

Proof for Proposition 8.4.3

uses 0

u-v=u'-v' だから u+v'=u'+v である．両辺は非負可測関数なので，加法性より

\int_X u\,d\mu+\int_X v'\,d\mu =\int_X (u+v')\,d\mu =\int_X (u'+v)\,d\mu =\int_X u'\,d\mu+\int_X v\,d\mu.

したがって移項して \int_X u\,d\mu-\int_X v\,d\mu =\int_X u'\,d\mu-\int_X v'\,d\mu を得る．

Theorem8.4.4

uses 1

Used by 4

Reverse dependency previews

Preview

Corollary 8.4.5

Loading preview

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

✓L∃∀N

Tagsleanok

可積分性と絶対値. f\in M(X;\RR) に対して，次は同値である．

f\in\calL^1(X)
|f|\in\calL^1(X)

さらに，このとき \int_X |f|\,d\mu=\int_X f^+\,d\mu+\int_X f^-\,d\mu が成り立つ．

Lean code for Theorem8.4.4●2 theorems

theoremdefined in NoteKsk/«08lintegral».lean

complete

theorem NoteKsk.Chapter08.integrable_norm.{u_1, u_2} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} {E : Type u_2}
  [NormedAddCommGroup E] {f : α → E}
  (hf : MeasureTheory.Integrable f μ) :
  MeasureTheory.Integrable (fun x ↦ ‖f x‖) μ

theorem NoteKsk.Chapter08.integrable_norm.{u_1,
    u_2}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {E : Type u_2} [NormedAddCommGroup E]
  {f : α → E}
  (hf : MeasureTheory.Integrable f μ) :
  MeasureTheory.Integrable (fun x ↦ ‖f x‖)
    μ

theoremdefined in NoteKsk/«08lintegral».lean

complete

theorem NoteKsk.Chapter08.lebesgueIntegrable_iff_abs.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ}
  (hf_meas : MeasureTheory.AEStronglyMeasurable f μ) :
  NoteKsk.LebesgueIntegrable μ f ↔
    NoteKsk.LebesgueIntegrable μ fun x ↦ |f x|

theorem NoteKsk.Chapter08.lebesgueIntegrable_iff_abs.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {f : α → ℝ}
  (hf_meas :
    MeasureTheory.AEStronglyMeasurable f
      μ) :
  NoteKsk.LebesgueIntegrable μ f ↔
    NoteKsk.LebesgueIntegrable μ fun x ↦
      |f x|

Proof for Theorem 8.4.4

uses 0

|f|=f^++f^- だから，非負可測関数の加法性より \int_X |f|\,d\mu=\int_X f^+\,d\mu+\int_X f^-\,d\mu である．したがって右辺が有限であることと \int_X f^+\,d\mu<\infty，\int_X f^-\,d\mu<\infty が成り立つことは同値である．これはまさに f の可積分性の定義である．

Corollary8.4.5

uses 1

Used by 4

Reverse dependency previews

Preview

Theorem 8.7.1

Loading preview

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

✓L∃∀N

Tagsleanok

優関数による可積分性の判定. f\in M(X;\RR) とし，g\in\calL^1(X) かつ g\ge0 a.e. on X とする．もし |f|\le g a.e. on X ならば f は可積分である．

Lean code for Corollary8.4.5●1 theorem

theoremdefined in NoteKsk/«08lintegral».lean

complete

theorem NoteKsk.Chapter08.dominated_integrability.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ℝ}
  (hg : MeasureTheory.Integrable g μ)
  (hf : MeasureTheory.AEStronglyMeasurable f μ)
  (hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ g x) : MeasureTheory.Integrable f μ

theorem NoteKsk.Chapter08.dominated_integrability.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {f g : α → ℝ}
  (hg : MeasureTheory.Integrable g μ)
  (hf :
    MeasureTheory.AEStronglyMeasurable f
      μ)
  (hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ g x) :
  MeasureTheory.Integrable f μ

Proof for Corollary 8.4.5

uses 0

仮定より |f|\le |g| a.e. on X である．零集合上で値を変えても非負関数の積分は変わらないので，単調性より \int_X |f|\,d\mu\le \int_X |g|\,d\mu<\infty である．ゆえにTheorem 8.4.4より f は可積分である．

Corollary8.4.6

uses 1used by 0✓L∃∀N

Tagsleanok

可積分関数は有限値を a.e. でとる. f\in\calL^1(X) ならば |f|<\infty a.e. on X が成り立つ．

Lean code for Corollary8.4.6●1 theorem

theoremdefined in NoteKsk/«08lintegral».lean

complete

theorem NoteKsk.Chapter08.integrable_real_finite_ae.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} (f : α → ℝ) :
  ∀ᵐ (x : α) ∂μ, ↑|f x| < ⊤

theorem NoteKsk.Chapter08.integrable_real_finite_ae.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  (f : α → ℝ) : ∀ᵐ (x : α) ∂μ, ↑|f x| < ⊤

In the lecture, signed measurable functions may be extended-real-valued and
integrability implies finiteness a.e.  Here signed integrable functions are
real-valued from the start, so the corresponding finiteness statement is
tautological.

Proof for Corollary 8.4.6

uses 0

N:=\{x \in X \mid |f(x)|=\infty\} とおく．各 n \in \NN について n1_N\le |f| だから，単調性より n\,\mu(N)=\int_X n1_N\,d\mu \le \int_X |f|\,d\mu<\infty である．これがすべての n で成り立つためには \mu(N)=0 でなければならない．

Proposition8.4.7

uses 1

Used by 2

Reverse dependency previews

Preview

Proposition 8.4.8

Loading preview

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

✓L∃∀N

Tagsleanok

零集合上の任意の関数. N \subset X が可測で \mu(N)=0 ならば，任意の f\in M(X;\RR) は N 上で可積分であり， \int_N f\,d\mu=0 が成り立つ．

Lean code for Proposition8.4.7●2 theorems

theoremdefined in NoteKsk/«08lintegral».lean

complete

theorem NoteKsk.Chapter08.integrableOn_of_measure_zero.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} {N : Set α}
  (hN : μ N = 0) (f : α → ℝ) : MeasureTheory.IntegrableOn f N μ

theorem NoteKsk.Chapter08.integrableOn_of_measure_zero.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {N : Set α} (hN : μ N = 0) (f : α → ℝ) :
  MeasureTheory.IntegrableOn f N μ

theoremdefined in NoteKsk/«08lintegral».lean

complete

theorem NoteKsk.Chapter08.setIntegral_eq_zero_of_measure_zero.{u_1}
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α}
  {N : Set α} (hN : μ N = 0) (f : α → ℝ) : ∫ (x : α) in N, f x ∂μ = 0

theorem NoteKsk.Chapter08.setIntegral_eq_zero_of_measure_zero.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {N : Set α} (hN : μ N = 0) (f : α → ℝ) :
  ∫ (x : α) in N, f x ∂μ = 0

Proof for Proposition 8.4.7

uses 0

非負可測関数については零集合上の積分は 0 である（Proposition 8.3.1）．したがって \int_N f^+\,d\mu=\int_N f^-\,d\mu=0 である．よって f は N 上で可積分で， \int_N f\,d\mu=\int_N f^+\,d\mu-\int_N f^-\,d\mu=0 となる．

Proposition8.4.8

Statement uses 2

Statement dependency previews

Preview

Theorem 8.4.4

Loading preview

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

Used by 2

Reverse dependency previews

Preview

Definition 8.4.9

Loading preview

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

✓L∃∀N

Tagsleanok

符号付関数の a.e. 不変性. f,g\in M(X;\RR) とする． f=g a.e. on X で，f\in\calL^1(X) ならば g\in\calL^1(X) であり， \int_X f\,d\mu=\int_X g\,d\mu が成り立つ．

Lean code for Proposition8.4.8●2 theorems

theoremdefined in NoteKsk/«08lintegral».lean

complete

theorem NoteKsk.Chapter08.signed_integral_congr_ae.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ℝ}
  (hf : MeasureTheory.Integrable f μ) (hfg : f =ᵐ[μ] g) :
  MeasureTheory.Integrable g μ ∧ ∫ (x : α), f x ∂μ = ∫ (x : α), g x ∂μ

theorem NoteKsk.Chapter08.signed_integral_congr_ae.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {f g : α → ℝ}
  (hf : MeasureTheory.Integrable f μ)
  (hfg : f =ᵐ[μ] g) :
  MeasureTheory.Integrable g μ ∧
    ∫ (x : α), f x ∂μ = ∫ (x : α), g x ∂μ

theoremdefined in NoteKsk/«08lintegral».lean

complete

theorem NoteKsk.Chapter08.integral_respects_ae_representatives.{u_1}
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α}
  {f g : α → ℝ} (hfg : f =ᵐ[μ] g) :
  ∫ (x : α), f x ∂μ = ∫ (x : α), g x ∂μ

theorem NoteKsk.Chapter08.integral_respects_ae_representatives.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {f g : α → ℝ} (hfg : f =ᵐ[μ] g) :
  ∫ (x : α), f x ∂μ = ∫ (x : α), g x ∂μ

Proof for Proposition 8.4.8

uses 0

N:=\{x \in X \mid f(x)\ne g(x)\} とおくと \mu(N)=0 である． X\setminus N 上では |g|=|f| であり， N 上の積分はどちらも 0 だから

\int_X |g|\,d\mu =\int_{X\setminus N}|g|\,d\mu+\int_N |g|\,d\mu =\int_{X\setminus N}|f|\,d\mu \le \int_X |f|\,d\mu<\infty.

よって g も可積分である．

さらに

\int_X f\,d\mu =\int_{X\setminus N} f\,d\mu+\int_N f\,d\mu =\int_{X\setminus N} g\,d\mu+\int_N g\,d\mu =\int_X g\,d\mu.

Definition8.4.9

uses 1used by 1✓L∃∀N

Tagsleanok

L^1 空間. \calL^1(X) を a.e. 同値関係で割った商集合を L^1(X):=\calL^1(X)/{\sim} と書く． Proposition 8.4.8より，積分値 \int_X f\,d\mu は代表元の取り方に依らず L^1(X) 上で定まる．測度を明示したいときは L^1(X,\mu) と書く．

Lean code for Definition8.4.9●1 definition

abbrevdefined in NoteKsk/Defs.lean

complete

abbrev NoteKsk.L1Space.{u_1} (α : Type u_1) [MeasurableSpace α]
  (μ : MeasureTheory.Measure α) : Type u_1

abbrev NoteKsk.L1Space.{u_1} (α : Type u_1)
  [MeasurableSpace α]
  (μ : MeasureTheory.Measure α) : Type u_1

Definition body

abbrev L1Space (α : Type*) [MeasurableSpace α] (μ : Measure α) : Type _ :=
  α →₁[μ] ℝ

The `L¹` space as mathlib's space of a.e.-equivalence classes of integrable functions.