8.5. 積分の絶対連続性
積分の絶対連続性.
f\in\calL^1(X) とする．
このとき任意の \eps>0 に対して，ある \delta>0 が存在して，
可測集合 A \subset X が \mu(A)<\delta を満たせば
\int_A |f|\,d\mu<\eps が成り立つ．
Lean code for Theorem8.5.1●4 theorems
Associated Lean declarations
-
theoremdefined in NoteKsk/«08lintegral».leancomplete
theorem NoteKsk.Chapter08.lintegral_absolute_continuity.{u_1} {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hfin : NoteKsk.lintegralNN μ f ≠ ⊤) {ε : ENNReal} (hε : ε ≠ 0) : ∃ δ > 0, ∀ (A : Set α), μ A < δ → NoteKsk.setLintegralNN μ A f < ε
theorem NoteKsk.Chapter08.lintegral_absolute_continuity.{u_1} {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hfin : NoteKsk.lintegralNN μ f ≠ ⊤) {ε : ENNReal} (hε : ε ≠ 0) : ∃ δ > 0, ∀ (A : Set α), μ A < δ → NoteKsk.setLintegralNN μ A f < ε
-
theoremdefined in NoteKsk/«08lintegral».leancomplete
theorem NoteKsk.Chapter08.integrable_abs_lintegral_ne_top.{u_1} {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : MeasureTheory.Integrable f μ) : ∫⁻ (x : α), ENNReal.ofReal |f x| ∂μ ≠ ⊤
theorem NoteKsk.Chapter08.integrable_abs_lintegral_ne_top.{u_1} {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : MeasureTheory.Integrable f μ) : ∫⁻ (x : α), ENNReal.ofReal |f x| ∂μ ≠ ⊤
-
theoremdefined in NoteKsk/«08lintegral».leancomplete
theorem NoteKsk.Chapter08.integral_absolute_continuity.{u_1} {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : MeasureTheory.Integrable f μ) {ε : ℝ} (hε : 0 < ε) : ∃ δ > 0, ∀ (A : Set α), μ A < δ → ∫⁻ (x : α) in A, ENNReal.ofReal |f x| ∂μ < ENNReal.ofReal ε
theorem NoteKsk.Chapter08.integral_absolute_continuity.{u_1} {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : MeasureTheory.Integrable f μ) {ε : ℝ} (hε : 0 < ε) : ∃ δ > 0, ∀ (A : Set α), μ A < δ → ∫⁻ (x : α) in A, ENNReal.ofReal |f x| ∂μ < ENNReal.ofReal ε
Mathlib states the `ε`-`δ` absolute continuity theorem with `ENNReal` bounds for measures. This is the formal version of the lecture statement `μ A < δ ⇒ ∫_A |f| < ε`.
-
theoremdefined in NoteKsk/«08lintegral».leancomplete
theorem NoteKsk.Chapter08.integral_absolute_continuity_filter.{u_1, u_2} {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {ι : Type u_2} {f : α → ℝ} (hf : MeasureTheory.Integrable f μ) {l : Filter ι} {A : ι → Set α} (hA : Filter.Tendsto (⇑μ ∘ A) l (nhds 0)) : Filter.Tendsto (fun i ↦ ∫ (x : α) in A i, f x ∂μ) l (nhds 0)
theorem NoteKsk.Chapter08.integral_absolute_continuity_filter.{u_1, u_2} {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {ι : Type u_2} {f : α → ℝ} (hf : MeasureTheory.Integrable f μ) {l : Filter ι} {A : ι → Set α} (hA : Filter.Tendsto (⇑μ ∘ A) l (nhds 0)) : Filter.Tendsto (fun i ↦ ∫ (x : α) in A i, f x ∂μ) l (nhds 0)
h:=|f| とおくと，h は非負可積分である．
積分の定義より，ある s\in S^+(X) で s \le h を満たすものが存在して
\int_X h\,d\mu-\int_X s\,d\mu<\eps/2 となる．
いま s=\sum_{k=1}^n a_k1_{A_k} と書き，M:=\max_{1\le k\le n}a_k とおく．
M=0 なら s=0 だから
\int_X h\,d\mu<\eps/2 である．
この場合は任意の \delta>0 でよい．
M>0 の場合は \delta:=\eps/(2M) とおく．
可測集合 A \subset X が \mu(A)<\delta を満たすとする．
すると集合に関する加法性と s\le h から
\int_X h\,d\mu
=\int_A h\,d\mu+\int_{X\setminus A}h\,d\mu
\ge \int_A h\,d\mu+\int_{X\setminus A}s\,d\mu.
よって
\int_A h\,d\mu
\le \int_X h\,d\mu-\int_{X\setminus A}s\,d\mu
=\left(\int_X h\,d\mu-\int_X s\,d\mu\right)+\int_A s\,d\mu
<\frac{\eps}{2}+M\,\mu(A)
<\frac{\eps}{2}+M\delta=\eps.
これで示された．