Lebesgue積分講義ノート

9.6. `\calL^1` と `L^1` の空間構造🔗

ここまでに示した性質は，\calL^1(X) と L^1(X) が単なる集合ではなく，線形構造，順序構造，大きさを測る構造をもつことを意味している．

Proposition9.6.1

Statement uses 5

Statement dependency previews

Preview

Corollary 8.4.5

Loading preview

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

used by 0✓L∃∀N

\calL^1 と L^1 の構造. 次が成り立つ．

\calL^1(X) は実ベクトル空間であり，写像 f\mapsto \int_X f\,d\mu は \calL^1(X) 上の線形写像である．
\|f\|_1:=\int_X |f|\,d\mu とおくと，これは \calL^1(X) 上の半ノルムである．すなわち \|cf\|_1=|c|\,\|f\|_1，\|f+g\|_1\le \|f\|_1+\|g\|_1 が成り立つ．また \|f\|_1=0 であることと f=0 a.e. on X であることは同値である．
L^1(X)=\calL^1(X)/{\sim} 上では

\|[f]\|_1:=\int_X |f|\,d\mu

によってノルムが定まる．したがって L^1(X) はノルム空間である．

\calL^1(X) は点ごとの順序に関してベクトル束（Riesz空間）である．つまり f,g\in\calL^1(X) なら f\vee g:=\max(f,g)，f\wedge g:=\min(f,g)，|f| も \calL^1(X) に属する．さらに，h\in M(X;\RR) が |h|\le |f| a.e. on X を満たし，f\in\calL^1(X) ならば h\in\calL^1(X) である．
L^1(X) には [f]\le [g] \iff f\le g a.e. on X によって順序が定まり，この順序に関して L^1(X) もベクトル束である．さらに |[f]|\le |[g]| なら \|[f]\|_1\le \|[g]\|_1 であり，ノルムは順序と両立している．

Lean code for Proposition9.6.1●7 declarations

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.

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

complete

theorem NoteKsk.Chapter09.integrable_add_real.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ℝ}
  (hf : MeasureTheory.Integrable f μ)
  (hg : MeasureTheory.Integrable g μ) :
  MeasureTheory.Integrable (fun x ↦ f x + g x) μ

theorem NoteKsk.Chapter09.integrable_add_real.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {f g : α → ℝ}
  (hf : MeasureTheory.Integrable f μ)
  (hg : MeasureTheory.Integrable g μ) :
  MeasureTheory.Integrable
    (fun x ↦ f x + g x) μ

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

complete

theorem NoteKsk.Chapter09.integral_add_real.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ℝ}
  (hf : MeasureTheory.Integrable f μ)
  (hg : MeasureTheory.Integrable g μ) :
  ∫ (x : α), f x + g x ∂μ = ∫ (x : α), f x ∂μ + ∫ (x : α), g x ∂μ

theorem NoteKsk.Chapter09.integral_add_real.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {f g : α → ℝ}
  (hf : MeasureTheory.Integrable f μ)
  (hg : MeasureTheory.Integrable g μ) :
  ∫ (x : α), f x + g x ∂μ =
    ∫ (x : α), f x ∂μ + ∫ (x : α), g x ∂μ

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

complete

theorem NoteKsk.Chapter09.integral_smul.{u_1, u_2} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} {E : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℝ E] (c : ℝ) (f : α → E) :
  ∫ (x : α), c • f x ∂μ = c • ∫ (x : α), f x ∂μ

theorem NoteKsk.Chapter09.integral_smul.{u_1, u_2}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {E : Type u_2} [NormedAddCommGroup E]
  [NormedSpace ℝ E] (c : ℝ) (f : α → E) :
  ∫ (x : α), c • f x ∂μ =
    c • ∫ (x : α), f x ∂μ

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

complete

theorem NoteKsk.Chapter09.integral_abs_eq_zero_iff_ae_eq_zero.{u_1}
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α}
  {f : α → ℝ} (hf : MeasureTheory.Integrable f μ) :
  ∫ (x : α), |f x| ∂μ = 0 ↔ f =ᵐ[μ] 0

theorem NoteKsk.Chapter09.integral_abs_eq_zero_iff_ae_eq_zero.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {f : α → ℝ}
  (hf : MeasureTheory.Integrable f μ) :
  ∫ (x : α), |f x| ∂μ = 0 ↔ f =ᵐ[μ] 0

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

complete

theorem NoteKsk.Chapter09.integrable_of_ae_abs_le_const.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [MeasureTheory.IsFiniteMeasure μ] {f : α → ℝ}
  (hf : MeasureTheory.AEStronglyMeasurable f μ) {M : ℝ}
  (hM : ∀ᵐ (x : α) ∂μ, |f x| ≤ M) : MeasureTheory.Integrable f μ

theorem NoteKsk.Chapter09.integrable_of_ae_abs_le_const.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  [MeasureTheory.IsFiniteMeasure μ]
  {f : α → ℝ}
  (hf :
    MeasureTheory.AEStronglyMeasurable f
      μ)
  {M : ℝ}
  (hM : ∀ᵐ (x : α) ∂μ, |f x| ≤ M) :
  MeasureTheory.Integrable f μ

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

complete

theorem NoteKsk.Chapter09.abs_integral_le_const_mul_measure.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [MeasureTheory.IsFiniteMeasure μ] {f : α → ℝ}
  (hf : MeasureTheory.AEStronglyMeasurable f μ) {M : ℝ}
  (hM : ∀ᵐ (x : α) ∂μ, |f x| ≤ M) :
  |∫ (x : α), f x ∂μ| ≤ M * μ.real Set.univ

theorem NoteKsk.Chapter09.abs_integral_le_const_mul_measure.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  [MeasureTheory.IsFiniteMeasure μ]
  {f : α → ℝ}
  (hf :
    MeasureTheory.AEStronglyMeasurable f
      μ)
  {M : ℝ}
  (hM : ∀ᵐ (x : α) ∂μ, |f x| ≤ M) :
  |∫ (x : α), f x ∂μ| ≤
    M * μ.real Set.univ

Proof for Proposition 9.6.1

uses 0

(1) は斉次性と加法性から従う． (2) の斉次性は |cf|=|c|\,|f| から従い，三角不等式は |f+g|\le |f|+|g| と積分の単調性・加法性から従う．また \|f\|_1=0 の判定はProposition 9.3.4である．

(3) について，\calL^1(X) の和とスカラー倍は a.e. 同値関係と両立するので，L^1(X) は実ベクトル空間である．また f=g a.e. なら |f|=|g| a.e. であるから，\|[f]\|_1 は代表元の取り方に依らない．さらに (2) より \|[f]\|_1=0 なら f=0 a.e. であり，これは L^1(X) の元として [f]=0 であることを意味する．

(4) について，f\vee g と f\wedge g は

f\vee g=\frac{f+g+|f-g|}{2},\qquad f\wedge g=\frac{f+g-|f-g|}{2}

と書けるので，\calL^1(X) に属する．また |h|\le |f| a.e. なら Corollary 8.4.5 より h\in\calL^1(X) である．

(5) は，a.e. に一致する代表元に取り替えても大小関係，和，スカラー倍，\vee,\wedge が a.e. の意味で変わらないことから従う．また |[f]|\le |[g]| なら |f|\le |g| a.e. なので，積分の単調性より \|[f]\|_1\le \|[g]\|_1 である．

Remark. \calL^1(X) 上の \|\cdot\|_1 は，関数を点ごとに区別する限りノルムではなく半ノルムである．零でない関数でも，零集合上にだけ値をもつなら \|f\|_1=0 になりうるからである．このため関数解析では，a.e. に等しい関数を同一視した L^1(X) を使う．後で Riesz--Fischer の定理を示すと，このノルム空間 L^1(X) は完備であり，Banach空間になる．さらに順序構造も保たれるので，後の言葉では L^1(X) はBanach束の典型例である．