Lebesgue積分講義ノート

7.7. ほとんど至る所（almost everywhere）🔗

Definition7.7.1
uses 0
Used by 2
Reverse dependency previews
Preview
Proposition 7.7.2
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N
Tagsleanok

ほとんど至る所（almost everywhere）. 測度空間(X,\calM,\mu) 上の述語P（つまり，各点 x \in X に命題P(x)を対応付ける写像）

と可測集合E \in \calM に対し， 「PがE上ほとんど至る所（almost everywhere）成り立つ」または「ほとんど至る所の点x \in EでPが成り立つ」

P \text{ }\mu\text{-a.e.\ on } E, \quad P(x) \text{ at }\mu\text{-a.e. } x \in E

とは，Pが成り立たない点の集合が\mu-零集合となることをいう

\exists N \in \calM \text{ such that } \mu(N)=0 \text{ and } \{ x \in E \mid \neg P(x) \} \subset N.

Lean code for Definition7.7.1●1 definition
  • defdefined in NoteKsk/Defs.lean
    complete
    def NoteKsk.AlmostEverywhereOn.{u_1} {α : Type u_1} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α) (E : Set α) (P : α → Prop) : Prop
    def NoteKsk.AlmostEverywhereOn.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  (E : Set α) (P : α → Prop) : Prop

    Definition body

    def AlmostEverywhereOn {α : Type*} [MeasurableSpace α]
    (μ : Measure α) (E : Set α) (P : α → Prop) : Prop :=
  ∀ᵐ x ∂ μ.restrict E, P x
    `P` holds almost everywhere on `E`, expressed using mathlib's restricted
measure.  This is the formal counterpart of the lecture notation
`P μ-a.e. on E`.
Proposition7.7.2
uses 1used by 1✓L∃∀N
Tagsleanok

測度空間 (X,\calM,\mu) と E\in\calM を固定する． E 上の拡大実数値関数全体において， f\sim g \iff f=g \text{ }\mu\text{-a.e.\ on } E で定める関係 \sim は同値関係である．

Lean code for Proposition7.7.2●2 declarations
  • defdefined in NoteKsk/Defs.lean
    complete
    def NoteKsk.AEEqualOn.{u_1, u_2} {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β] (μ : MeasureTheory.Measure α)
  (E : Set α) (f g : α → β) : Prop
    def NoteKsk.AEEqualOn.{u_1, u_2}
  {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β]
  (μ : MeasureTheory.Measure α)
  (E : Set α) (f g : α → β) : Prop

    Definition body

    def AEEqualOn {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
    (μ : Measure α) (E : Set α) (f g : α → β) : Prop :=
  f =ᵐ[μ.restrict E] g
    Almost-everywhere equality on a set, expressed using the restricted measure.
  • theoremdefined in NoteKsk/«07mble-funcs».lean
    complete
    theorem NoteKsk.Chapter07.aeEqualOn_equivalence.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β]
  (μ : MeasureTheory.Measure α) (E : Set α) :
  Equivalence (NoteKsk.AEEqualOn μ E)
    theorem NoteKsk.Chapter07.aeEqualOn_equivalence.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β]
  (μ : MeasureTheory.Measure α)
  (E : Set α) :
  Equivalence (NoteKsk.AEEqualOn μ E)
Proof for Proposition 7.7.2
uses 0

反射律quad \{f\ne f\}=\emptyset だから f\sim f である．

対称律quad \{f\ne g\}=\{g\ne f\} だから f\sim g なら g\sim f である．

推移律quad f\sim g かつ g\sim h とする． このとき

\{f\ne g\}\subset N_1,\qquad \{g\ne h\}\subset N_2

かつ \mu(N_1)=\mu(N_2)=0 を満たす N_1,N_2\in\calM が存在する． すると \{f\ne h\}\subset \{f\ne g\}\cup\{g\ne h\} である． したがって

\{f\ne h\}\subset N_1\cup N_2

であり，N_1\cup N_2 は零集合である． したがって f\sim h である．

Proposition7.7.3
Statement uses 2
Statement dependency previews
Preview
Theorem 7.3.4
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
used by 1✓L∃∀N
Tagsleanok

a.e. 修正による可測性. (X,\calM,\mu) を完備な測度空間とし，E\in\calM とする． f\in M(E) とし， g:E\to\eRR が

f=g \quad \mu\text{-a.e.\ on } E

を満たすとする． このとき g も \calM(E)-可測である．

Lean code for Proposition7.7.3●1 theorem
  • theoremdefined in NoteKsk/«07mble-funcs».lean
    complete
    theorem NoteKsk.Chapter07.measurable_of_ae_eq_complete.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α} [μ.IsComplete] {f g : α → β}
  (hf : Measurable f) (hfg : f =ᵐ[μ] g) : Measurable g
    theorem NoteKsk.Chapter07.measurable_of_ae_eq_complete.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  [μ.IsComplete] {f g : α → β}
  (hf : Measurable f) (hfg : f =ᵐ[μ] g) :
  Measurable g
Proof for Proposition 7.7.3
uses 0

A:=\{x\in E\mid f(x)\ne g(x)\}

とおく． f=g が \mu-a.e. on E で成り立つから， A\subset N かつ \mu(N)=0 を満たす N\in\calM が存在する． 測度空間は完備なので，A および A の任意の部分集合は \calM に属する． 特にそれらは \calM(E) に属する．

任意の a\in\RR に対して

\{g>a\} = \bigl(\{f>a\}\cap(E\setminus A)\bigr)\cup\bigl(\{g>a\}\cap A\bigr)

である． 右辺第1項は可測であり， 第2項は A の部分集合だから可測である． よって

\{g>a\}

は可測である． したがってTheorem 7.3.4より g は \calM(E)-可測である．