8.3. 零集合と almost everywhere
零集合上の積分.
N \subset X が可測で \mu(N)=0 ならば，
任意の f\in M^+(X) に対して
\int_N f\,d\mu=0 が成り立つ．
Lean code for Proposition8.3.1●1 theorem
Associated Lean declarations
-
theoremdefined in NoteKsk/«08lintegral».leancomplete
theorem NoteKsk.Chapter08.setLintegralNN_eq_zero_of_measure_zero.{u_1} {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {N : Set α} (hN : μ N = 0) (f : α → ENNReal) : NoteKsk.setLintegralNN μ N f = 0
theorem NoteKsk.Chapter08.setLintegralNN_eq_zero_of_measure_zero.{u_1} {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {N : Set α} (hN : μ N = 0) (f : α → ENNReal) : NoteKsk.setLintegralNN μ N f = 0
定義より
\int_N f\,d\mu
=\sup\left\{\int_N s\,d\mu \;\middle|\; 0 \le s \le f,\ s \text{ は単関数}\right\}.
ところが N 上の任意の単関数 s=\sum_{k=1}^n a_k1_{A_k} について，
各 A_k \subset N だから \mu(A_k)\le \mu(N)=0 である．
したがって \int_N s\,d\mu=\sum_{k=1}^n a_k \mu(A_k)=0 である．
ゆえに上限も 0 である．
-
NoteKsk.Chapter08.lintegralNN_congr_ae[complete]
非負関数の a.e. 不変性.
f,g\in M^+(X) とする．
f=g a.e. on X ならば
\int_X f\,d\mu=\int_X g\,d\mu が成り立つ．
Lean code for Proposition8.3.2●1 theorem
Associated Lean declarations
-
NoteKsk.Chapter08.lintegralNN_congr_ae[complete]
-
NoteKsk.Chapter08.lintegralNN_congr_ae[complete]
-
theoremdefined in NoteKsk/«08lintegral».leancomplete
theorem NoteKsk.Chapter08.lintegralNN_congr_ae.{u_1} {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ENNReal} (hfg : f =ᵐ[μ] g) : NoteKsk.lintegralNN μ f = NoteKsk.lintegralNN μ g
theorem NoteKsk.Chapter08.lintegralNN_congr_ae.{u_1} {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ENNReal} (hfg : f =ᵐ[μ] g) : NoteKsk.lintegralNN μ f = NoteKsk.lintegralNN μ g
N:=\{x \in X \mid f(x)\ne g(x)\} とおくと \mu(N)=0 である．
したがってProposition 8.3.1より
\int_N f\,d\mu=\int_N g\,d\mu=0 である．
また X=(X\setminus N)\sqcup N だから，
集合に関する加法性より
\int_X f\,d\mu
=\int_{X\setminus N} f\,d\mu+\int_N f\,d\mu
=\int_{X\setminus N} g\,d\mu+\int_N g\,d\mu
=\int_X g\,d\mu.
非負関数の積分が 0 であることの判定.
f\in M^+(X) に対して，次は同値である．
-
\int_X f\,d\mu=0 -
f=0a.e. onX
Lean code for Proposition8.3.3●1 theorem
Associated Lean declarations
-
theoremdefined in NoteKsk/«08lintegral».leancomplete
theorem NoteKsk.Chapter08.lintegralNN_eq_zero_iff_ae_eq_zero.{u_1} {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : Measurable f) : NoteKsk.lintegralNN μ f = 0 ↔ f =ᵐ[μ] 0
theorem NoteKsk.Chapter08.lintegralNN_eq_zero_iff_ae_eq_zero.{u_1} {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : Measurable f) : NoteKsk.lintegralNN μ f = 0 ↔ f =ᵐ[μ] 0
(2) \Rightarrow (1)quad
f=0 a.e. なら，Proposition 8.3.2を g=0 に適用して
\int_X f\,d\mu=\int_X 0\,d\mu=0 である．
(1) \Rightarrow (2)quad
各 n \in \NN に対して
A_n:=\{x \in X \mid f(x)\ge 1/n\} とおく．
すると
n^{-1}1_{A_n}\le f だから単調性より
\frac1n \mu(A_n)
=\int_X \frac1n 1_{A_n}\,d\mu
\le \int_X f\,d\mu=0.
よって \mu(A_n)=0 である．
一方，\{x \in X \mid f(x)>0\}=\bigcup_{n=1}^{\infty}A_n だから可算加法性より \mu(\{f>0\})=0 である．
したがって f=0 a.e. である．