Lebesgue積分講義ノート

9.4. 線形性🔗

Proposition9.4.1
uses 1
Used by 2
Reverse dependency previews
Preview
Theorem 9.5.1
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N
Tagsleanok

斉次性. f\in\calL^1(X)，c \in \RR とする． このとき \int_X cf\,d\mu=c\int_X f\,d\mu が成り立つ．

Lean code for Proposition9.4.1●2 theorems
  • theoremdefined in NoteKsk/«09lintegral-prop».lean
    complete
    theorem NoteKsk.Chapter09.integral_const_mul_real.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} (c : ℝ)
  (f : α → ℝ) : ∫ (x : α), c * f x ∂μ = c * ∫ (x : α), f x ∂μ
    theorem NoteKsk.Chapter09.integral_const_mul_real.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α} (c : ℝ)
  (f : α → ℝ) :
  ∫ (x : α), c * f x ∂μ =
    c * ∫ (x : α), f 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 ∂μ
Proof for Proposition 9.4.1
uses 0

まず c\ge 0 の場合を示す．f=f^+-f^- だから cf=(cf^+)-(cf^-) であり，cf^+,cf^- は非負可積分である． したがって

\int_X cf\,d\mu =\int_X cf^+\,d\mu-\int_X cf^-\,d\mu =c\int_X f^+\,d\mu-c\int_X f^-\,d\mu =c\int_X f\,d\mu.

次に c<0 とする． このとき cf=(-c)(-f) であり，-c>0 だから前半の結果を -f に適用して \int_X cf\,d\mu=(-c)\int_X (-f)\,d\mu=(-c)(-\int_X f\,d\mu)=c\int_X f\,d\mu を得る．

Proposition9.4.2
Statement uses 2
Statement dependency previews
Preview
Proposition 8.4.3
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
Used by 3
Reverse dependency previews
Preview
Corollary 9.4.3
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N
Tagsleanok

加法性. f,g\in\calL^1(X) とする． このとき f+g\in\calL^1(X) で， \int_X (f+g)\,d\mu=\int_X f\,d\mu+\int_X g\,d\mu が成り立つ．

Lean code for Proposition9.4.2●4 theorems
  • 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_neg_real.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} (f : α → ℝ) :
  ∫ (x : α), -f x ∂μ = -∫ (x : α), f x ∂μ
    theorem NoteKsk.Chapter09.integral_neg_real.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  (f : α → ℝ) :
  ∫ (x : α), -f x ∂μ = -∫ (x : α), f x ∂μ
  • theoremdefined in NoteKsk/«09lintegral-prop».lean
    complete
    theorem NoteKsk.Chapter09.integral_sub_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_sub_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 ∂μ
Proof for Proposition 9.4.2
uses 0

まず |f+g|\le |f|+|g| だから，右辺の可積分性より Corollary 8.4.5から f+g も可積分である．

次に f=f^+-f^-，g=g^+-g^- と書くと f+g=(f^++g^+)-(f^-+g^-) である． f^++g^+ と f^-+g^- は非負可積分であるから， prop:nonnegative-integral-basic,prop:integral-representation-independenceより

\int_X (f+g)\,d\mu =\int_X (f^++g^+)\,d\mu-\int_X (f^-+g^-)\,d\mu

である． また \int_X (f^++g^+)\,d\mu=\int_X f^+\,d\mu+\int_X g^+\,d\mu かつ \int_X (f^-+g^-)\,d\mu=\int_X f^-\,d\mu+\int_X g^-\,d\mu だから， 右辺は \int_X f\,d\mu+\int_X g\,d\mu に等しい．

Corollary9.4.3
uses 1used by 1✓L∃∀N
Tagsleanok

有限和. f_1,\dots,f_n\in\calL^1(X) とすると \int_X (\sum_{k=1}^n f_k)\,d\mu=\sum_{k=1}^n \int_X f_k\,d\mu が成り立つ．

Lean code for Corollary9.4.3●1 theorem
  • theoremdefined in NoteKsk/«09lintegral-prop».lean
    complete
    theorem NoteKsk.Chapter09.integral_finset_sum.{u_1, u_2} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} {ι : Type u_2}
  (s : Finset ι) {f : ι → α → ℝ}
  (hf : ∀ i ∈ s, MeasureTheory.Integrable (f i) μ) :
  ∫ (x : α), ∑ i ∈ s, f i x ∂μ = ∑ i ∈ s, ∫ (x : α), f i x ∂μ
    theorem NoteKsk.Chapter09.integral_finset_sum.{u_1,
    u_2}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {ι : Type u_2} (s : Finset ι)
  {f : ι → α → ℝ}
  (hf :
    ∀ i ∈ s,
      MeasureTheory.Integrable (f i) μ) :
  ∫ (x : α), ∑ i ∈ s, f i x ∂μ =
    ∑ i ∈ s, ∫ (x : α), f i x ∂μ
Proof for Corollary 9.4.3
uses 0

Proposition 9.4.2を繰り返し用いればよい．