8.1. 単関数の積分🔗

Definition8.1.1

uses 1

Used by 2

Reverse dependency previews

Preview

Definition 8.1.2

Loading preview

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

✓L∃∀N

Tagsleanok

非負単関数. 写像 s:X \to [0,\infty) が非負の単関数（simple function）または階段関数（step function）であるとは， 有限個の非負実数 a_1,\dots,a_n と互いに素な可測集合 A_1,\dots,A_n \subset X を用いて s=\sum_{k=1}^n a_k 1_{A_k} と書けることをいう．非負単関数全体を S^+(X) と書く．

Lean code for Definition8.1.1●2 declarations

abbrevdefined in NoteKsk/Defs.lean

complete

abbrev NoteKsk.SimpleNNFun.{u_1} (α : Type u_1) [MeasurableSpace α] : Type u_1

abbrev NoteKsk.SimpleNNFun.{u_1} (α : Type u_1)
  [MeasurableSpace α] : Type u_1

Definition body

abbrev SimpleNNFun (α : Type*) [MeasurableSpace α] : Type _ :=
  MeasureTheory.SimpleFunc α ENNReal

Nonnegative extended-real-valued simple functions.

theoremdefined in NoteKsk/«08lintegral».lean

complete

theorem NoteKsk.Chapter08.simpleNNFun_measurable.{u_1} {α : Type u_1}
  [MeasurableSpace α] (s : NoteKsk.SimpleNNFun α) :
  Measurable fun x ↦ s x

theorem NoteKsk.Chapter08.simpleNNFun_measurable.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  (s : NoteKsk.SimpleNNFun α) :
  Measurable fun x ↦ s x

Remark. 単関数は関数値が有限個しかない可測関数であり，S^+(X) = \{ \sum_{k=1}^n a_k 1_{A_k} \mid a_k \ge 0, \bigsqcup_{k=1}^n A_k = X, n \in \NN \} と書ける． S^+(X)\subset M^+(X) である．

特に指示関数 1_A は最も基本的な単関数である．

Definition8.1.2

uses 1

Used by 2

Reverse dependency previews

Preview

Proposition 8.1.3

Loading preview

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

✓L∃∀N

Tagsleanok

単関数の積分. 非負単関数 s\in S^+(X) を s=\sum_{k=1}^n a_k 1_{A_k} と書くとき，

\int_X s\,d\mu := \sum_{k=1}^n a_k\,\mu(A_k)

と定める．

Lean code for Definition8.1.2●2 declarations

abbrevdefined in NoteKsk/Defs.lean

complete

abbrev NoteKsk.simpleLintegral.{u_1} {α : Type u_1} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α) (f : NoteKsk.SimpleNNFun α) : ENNReal

abbrev NoteKsk.simpleLintegral.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  (f : NoteKsk.SimpleNNFun α) : ENNReal

Definition body

noncomputable abbrev simpleLintegral {α : Type*} [MeasurableSpace α]
    (μ : Measure α) (f : SimpleNNFun α) : ENNReal :=
  f.lintegral μ

The integral of a nonnegative simple function, using mathlib's `SimpleFunc.lintegral`.

theoremdefined in NoteKsk/«08lintegral».lean

complete

theorem NoteKsk.Chapter08.lintegralNN_eq_simple.{u_1} {α : Type u_1}
  [MeasurableSpace α] (μ : MeasureTheory.Measure α)
  (s : NoteKsk.SimpleNNFun α) :
  (NoteKsk.lintegralNN μ fun x ↦ s x) = NoteKsk.simpleLintegral μ s

theorem NoteKsk.Chapter08.lintegralNN_eq_simple.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  (s : NoteKsk.SimpleNNFun α) :
  (NoteKsk.lintegralNN μ fun x ↦ s x) =
    NoteKsk.simpleLintegral μ s

Proposition8.1.3

uses 1used by 0✓L∃∀N

Tagsleanok

単関数の積分のwell-definedness. 非負単関数 s の表示の仕方によらず，\int_X s\,d\mu は同じ値を与える．

Lean code for Proposition8.1.3●1 theorem

theoremdefined in NoteKsk/«08lintegral».lean

complete

theorem NoteKsk.Chapter08.simpleLintegral_congr.{u_1} {α : Type u_1}
  [MeasurableSpace α] (μ : MeasureTheory.Measure α)
  {s t : NoteKsk.SimpleNNFun α} (hst : ∀ (x : α), s x = t x) :
  NoteKsk.simpleLintegral μ s = NoteKsk.simpleLintegral μ t

theorem NoteKsk.Chapter08.simpleLintegral_congr.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  {s t : NoteKsk.SimpleNNFun α}
  (hst : ∀ (x : α), s x = t x) :
  NoteKsk.simpleLintegral μ s =
    NoteKsk.simpleLintegral μ t

Well-definedness of the simple-function integral is built into mathlib's bundled
`SimpleFunc`: if two bundled simple functions have the same pointwise values,
their integrals agree.

Proof for Proposition 8.1.3

uses 0

s=\sum_{i=1}^n a_i 1_{A_i}=\sum_{j=1}^m b_j 1_{B_j} と2通りに表したとする．ここで \{A_i\} と \{B_j\} はそれぞれ互いに素で可測である．各 i,j に対して C_{ij}:=A_i \cap B_j とおくと，\{C_{ij}\}_{i,j} は互いに素な可測集合族であり， A_i=\bigsqcup_{j=1}^m C_{ij}，B_j=\bigsqcup_{i=1}^n C_{ij} が成り立つ．また x \in C_{ij} なら s(x)=a_i=b_j だから，C_{ij} 上では係数が一致する．ゆえに測度の可算加法性より

\sum_{i=1}^n a_i\,\mu(A_i) =\sum_{i,j}a_i\,\mu(C_{ij}) =\sum_{i,j}b_j\,\mu(C_{ij}) =\sum_{j=1}^m b_j\,\mu(B_j).

したがって積分値は表示に依らない．

Proposition8.1.4

uses 0used by 0XL∃∀N

Tagsexample

可測集合 A \subset X に対して \int_X 1_A\,d\mu = \mu(A) である
定数関数 c \ge 0 に対して \int_X c\,d\mu = c\,\mu(X) である

Proposition8.1.5

uses 1used by 1✓L∃∀N

Tagsleanok

単関数の基本性質. s,t\in S^+(X) と c \ge 0 に対して次が成り立つ．

\int_X (s+t)\,d\mu = \int_X s\,d\mu + \int_X t\,d\mu
\int_X cs\,d\mu = c \int_X s\,d\mu
s \le t なら \int_X s\,d\mu \le \int_X t\,d\mu

Lean code for Proposition8.1.5●5 theorems

theoremdefined in NoteKsk/«08lintegral».lean

complete

theorem NoteKsk.Chapter08.simpleLintegral_add.{u_1} {α : Type u_1}
  [MeasurableSpace α] (μ : MeasureTheory.Measure α)
  (s t : NoteKsk.SimpleNNFun α) :
  NoteKsk.simpleLintegral μ (s + t) =
    NoteKsk.simpleLintegral μ s + NoteKsk.simpleLintegral μ t

theorem NoteKsk.Chapter08.simpleLintegral_add.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  (s t : NoteKsk.SimpleNNFun α) :
  NoteKsk.simpleLintegral μ (s + t) =
    NoteKsk.simpleLintegral μ s +
      NoteKsk.simpleLintegral μ t

theoremdefined in NoteKsk/«08lintegral».lean

complete

theorem NoteKsk.Chapter08.simpleLintegral_const_mul.{u_1} {α : Type u_1}
  [MeasurableSpace α] (μ : MeasureTheory.Measure α) (c : ENNReal)
  (s : NoteKsk.SimpleNNFun α) :
  NoteKsk.simpleLintegral μ (MeasureTheory.SimpleFunc.const α c * s) =
    c * NoteKsk.simpleLintegral μ s

theorem NoteKsk.Chapter08.simpleLintegral_const_mul.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  (c : ENNReal)
  (s : NoteKsk.SimpleNNFun α) :
  NoteKsk.simpleLintegral μ
      (MeasureTheory.SimpleFunc.const α
          c *
        s) =
    c * NoteKsk.simpleLintegral μ s

theoremdefined in NoteKsk/«08lintegral».lean

complete

theorem NoteKsk.Chapter08.simpleLintegral_mono.{u_1} {α : Type u_1}
  [MeasurableSpace α] (μ : MeasureTheory.Measure α)
  {s t : NoteKsk.SimpleNNFun α} (hst : s ≤ t) :
  NoteKsk.simpleLintegral μ s ≤ NoteKsk.simpleLintegral μ t

theorem NoteKsk.Chapter08.simpleLintegral_mono.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  {s t : NoteKsk.SimpleNNFun α}
  (hst : s ≤ t) :
  NoteKsk.simpleLintegral μ s ≤
    NoteKsk.simpleLintegral μ t

theoremdefined in NoteKsk/«08lintegral».lean

complete

theorem NoteKsk.Chapter08.lintegral_indicator_one_eq_measure.{u_1}
  {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α)
  {A : Set α} (hA : MeasurableSet A) :
  ∫⁻ (x : α), A.indicator (fun x ↦ 1) x ∂μ = μ A

theorem NoteKsk.Chapter08.lintegral_indicator_one_eq_measure.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  {A : Set α} (hA : MeasurableSet A) :
  ∫⁻ (x : α),
      A.indicator (fun x ↦ 1) x ∂μ =
    μ A

theoremdefined in NoteKsk/«08lintegral».lean

complete

theorem NoteKsk.Chapter08.lintegral_const_eq.{u_1} {α : Type u_1}
  [MeasurableSpace α] (μ : MeasureTheory.Measure α) (c : ENNReal) :
  ∫⁻ (_x : α), c ∂μ = c * μ Set.univ

theorem NoteKsk.Chapter08.lintegral_const_eq.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  (c : ENNReal) :
  ∫⁻ (_x : α), c ∂μ = c * μ Set.univ

Proof for Proposition 8.1.5

uses 0

まず s=\sum_{i=1}^n a_i 1_{A_i}，t=\sum_{j=1}^m b_j 1_{B_j} と書く．共通細分 C_{ij}:=A_i \cap B_j を取れば，s+t=\sum_{i=1}^n \sum_{j=1}^m (a_i+b_j)1_{C_{ij}} である．したがって

\int_X (s+t)\,d\mu =\sum_{i,j}(a_i+b_j)\mu(C_{ij}) =\sum_i a_i \mu(A_i)+\sum_j b_j \mu(B_j) =\int_X s\,d\mu+\int_X t\,d\mu.

これで (1) が従う．

(2) は cs=\sum_{i=1}^n (ca_i)1_{A_i} と書けば直ちに従う．

(3) を示す． t-s は非負単関数であるから (1), (2) より \int_X t\,d\mu=\int_X s\,d\mu+\int_X (t-s)\,d\mu\ge \int_X s\,d\mu である．