Lebesgue積分講義ノート

9.1. 準備：正部分と負部分🔗

以後，測度空間 (X,\calM,\mu) を固定し，f,g\in M(X) とする．

Proposition9.1.1
uses 1used by 1✓L∃∀N
Tagsleanok

基本恒等式. 任意の可測関数 f に対して f=f^+-f^-，|f|=f^++f^-，f^+f^-=0 が成り立つ．

Lean code for Proposition9.1.1●7 declarations
  • abbrevdefined in NoteKsk/Defs.lean
    complete
    abbrev NoteKsk.realPositivePart.{u_1} {α : Type u_1} (f : α → ℝ) : α → ℝ
    abbrev NoteKsk.realPositivePart.{u_1}
  {α : Type u_1} (f : α → ℝ) : α → ℝ

    Definition body

    noncomputable abbrev realPositivePart {α : Type*} (f : α → ℝ) : α → ℝ :=
  fun x => max (f x) 0
    Positive part of a real-valued function, represented as a real-valued function.
This is the notation used in Chapter 09 for identities such as
`f = f⁺ - f⁻`.  The earlier `positivePart` is `ENNReal`-valued because it is
adapted to lower Lebesgue integrals.
  • abbrevdefined in NoteKsk/Defs.lean
    complete
    abbrev NoteKsk.realNegativePart.{u_1} {α : Type u_1} (f : α → ℝ) : α → ℝ
    abbrev NoteKsk.realNegativePart.{u_1}
  {α : Type u_1} (f : α → ℝ) : α → ℝ

    Definition body

    noncomputable abbrev realNegativePart {α : Type*} (f : α → ℝ) : α → ℝ :=
  fun x => max (-f x) 0
    Negative part of a real-valued function, represented as a real-valued function.
This is kept separate from the `ENNReal`-valued `negativePart` used in Chapter 08.
  • theoremdefined in NoteKsk/«09lintegral-prop».lean
    complete
    theorem NoteKsk.Chapter09.realPositivePart_nonneg.{u_1} {α : Type u_1}
  (f : α → ℝ) (x : α) : 0 ≤ NoteKsk.realPositivePart f x
    theorem NoteKsk.Chapter09.realPositivePart_nonneg.{u_1}
  {α : Type u_1} (f : α → ℝ) (x : α) :
  0 ≤ NoteKsk.realPositivePart f x
  • theoremdefined in NoteKsk/«09lintegral-prop».lean
    complete
    theorem NoteKsk.Chapter09.realNegativePart_nonneg.{u_1} {α : Type u_1}
  (f : α → ℝ) (x : α) : 0 ≤ NoteKsk.realNegativePart f x
    theorem NoteKsk.Chapter09.realNegativePart_nonneg.{u_1}
  {α : Type u_1} (f : α → ℝ) (x : α) :
  0 ≤ NoteKsk.realNegativePart f x
  • theoremdefined in NoteKsk/«09lintegral-prop».lean
    complete
    theorem NoteKsk.Chapter09.realPositivePart_sub_realNegativePart.{u_1}
  {α : Type u_1} (f : α → ℝ) (x : α) :
  NoteKsk.realPositivePart f x - NoteKsk.realNegativePart f x = f x
    theorem NoteKsk.Chapter09.realPositivePart_sub_realNegativePart.{u_1}
  {α : Type u_1} (f : α → ℝ) (x : α) :
  NoteKsk.realPositivePart f x -
      NoteKsk.realNegativePart f x =
    f x
  • theoremdefined in NoteKsk/«09lintegral-prop».lean
    complete
    theorem NoteKsk.Chapter09.realPositivePart_add_realNegativePart.{u_1}
  {α : Type u_1} (f : α → ℝ) (x : α) :
  NoteKsk.realPositivePart f x + NoteKsk.realNegativePart f x = |f x|
    theorem NoteKsk.Chapter09.realPositivePart_add_realNegativePart.{u_1}
  {α : Type u_1} (f : α → ℝ) (x : α) :
  NoteKsk.realPositivePart f x +
      NoteKsk.realNegativePart f x =
    |f x|
  • theoremdefined in NoteKsk/«09lintegral-prop».lean
    complete
    theorem NoteKsk.Chapter09.realPositivePart_mul_realNegativePart.{u_1}
  {α : Type u_1} (f : α → ℝ) (x : α) :
  NoteKsk.realPositivePart f x * NoteKsk.realNegativePart f x = 0
    theorem NoteKsk.Chapter09.realPositivePart_mul_realNegativePart.{u_1}
  {α : Type u_1} (f : α → ℝ) (x : α) :
  NoteKsk.realPositivePart f x *
      NoteKsk.realNegativePart f x =
    0
Proof for Proposition 9.1.1
uses 0

f(x)\ge 0 のとき f^+(x)=f(x)，f^-(x)=0 であり， f(x)<0 のとき f^+(x)=0，f^-(x)=-f(x) である． したがって各点 x ごとに上の3つの等式が成り立つ．

Proposition9.1.2
Statement uses 2
Statement dependency previews
Preview
Definition 8.4.2
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
Used by 2
Reverse dependency previews
Preview
Proposition 9.2.2
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N
Tagsleanok

非負関数による表示. f\in\calL^1(X) であることと， ある u,v\in\calL^1(X) が存在して u,v\ge0 かつ f=u-v と書けることは同値である． このとき \int_X f\,d\mu=\int_X u\,d\mu-\int_X v\,d\mu が成り立つ．

Lean code for Proposition9.1.2●5 theorems
  • theoremdefined in NoteKsk/«09lintegral-prop».lean
    complete
    theorem NoteKsk.Chapter09.realPositivePart_integrable.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ}
  (hf : MeasureTheory.Integrable f μ) :
  MeasureTheory.Integrable (NoteKsk.realPositivePart f) μ
    theorem NoteKsk.Chapter09.realPositivePart_integrable.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {f : α → ℝ}
  (hf : MeasureTheory.Integrable f μ) :
  MeasureTheory.Integrable
    (NoteKsk.realPositivePart f) μ
  • theoremdefined in NoteKsk/«09lintegral-prop».lean
    complete
    theorem NoteKsk.Chapter09.realNegativePart_integrable.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ}
  (hf : MeasureTheory.Integrable f μ) :
  MeasureTheory.Integrable (NoteKsk.realNegativePart f) μ
    theorem NoteKsk.Chapter09.realNegativePart_integrable.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {f : α → ℝ}
  (hf : MeasureTheory.Integrable f μ) :
  MeasureTheory.Integrable
    (NoteKsk.realNegativePart f) μ
  • theoremdefined in NoteKsk/«09lintegral-prop».lean
    complete
    theorem NoteKsk.Chapter09.integrable_iff_exists_integrable_sub_nonneg.{u_1}
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α}
  {f : α → ℝ} :
  MeasureTheory.Integrable f μ ↔
    ∃ u v,
      MeasureTheory.Integrable u μ ∧
        MeasureTheory.Integrable v μ ∧
          0 ≤ᵐ[μ] u ∧ 0 ≤ᵐ[μ] v ∧ f =ᵐ[μ] fun x ↦ u x - v x
    theorem NoteKsk.Chapter09.integrable_iff_exists_integrable_sub_nonneg.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {f : α → ℝ} :
  MeasureTheory.Integrable f μ ↔
    ∃ u v,
      MeasureTheory.Integrable u μ ∧
        MeasureTheory.Integrable v μ ∧
          0 ≤ᵐ[μ] u ∧
            0 ≤ᵐ[μ] v ∧
              f =ᵐ[μ] fun x ↦ u x - v x
    The lecture statement uses pointwise nonnegative measurable functions and
pointwise equality `f = u - v`.  This formal version uses a.e. nonnegativity
and a.e. equality, which is the mathlib-native formulation for Bochner
integrals and is equivalent for integration purposes.
  • 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 ∂μ
  • theoremdefined in NoteKsk/«09lintegral-prop».lean
    complete
    theorem NoteKsk.Chapter09.integral_eq_realPositivePart_sub_realNegativePart.{u_1}
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α}
  {f : α → ℝ} (hf : MeasureTheory.Integrable f μ) :
  ∫ (x : α), f x ∂μ =
    ∫ (x : α), NoteKsk.realPositivePart f x ∂μ -
      ∫ (x : α), NoteKsk.realNegativePart f x ∂μ
    theorem NoteKsk.Chapter09.integral_eq_realPositivePart_sub_realNegativePart.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {f : α → ℝ}
  (hf : MeasureTheory.Integrable f μ) :
  ∫ (x : α), f x ∂μ =
    ∫ (x : α),
        NoteKsk.realPositivePart f x ∂μ -
      ∫ (x : α),
        NoteKsk.realNegativePart f x ∂μ
Proof for Proposition 9.1.2
uses 0

Proposition 8.4.3より， f=u-v と書ければ積分値 \int_X u\,d\mu-\int_X v\,d\mu は表示に依らない．

まず f が可積分なら f=f^+-f^- であり， f^+,f^- は非負可積分であるから条件を満たす．

逆に f=u-v と書け，u,v が非負可積分とする． このとき f^+\le u，f^-\le v が成り立つ． 実際，f(x)\ge 0 なら f^+(x)=f(x)=u(x)-v(x)\le u(x) であり，f(x)<0 なら f^+(x)=0\le u(x) である． f^-\le v も同様である． したがってProposition 8.2.4より \int_X f^+\,d\mu\le \int_X u\,d\mu<\infty， \int_X f^-\,d\mu\le \int_X v\,d\mu<\infty である． よって f は可積分である．