Lebesgue積分講義ノート

9.5. 計算則のまとめ🔗

Theorem9.5.1
Statement uses 9
Statement dependency previews
Preview
Proposition 9.2.1
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
used by 0✓L∃∀N
Tagsleanok

測度空間上の積分の基本公式. f,g\in\calL^1(X) とする． このとき次が成り立つ．

  • \mu(X)=0 なら \int_X f\,d\mu=0

  • f=g a.e. なら \int_X f\,d\mu=\int_X g\,d\mu

  • f\le g a.e. なら \int_X f\,d\mu\le \int_X g\,d\mu

  • 任意の c \in \RR に対して \int_X cf\,d\mu=c\int_X f\,d\mu

  • \int_X (f+g)\,d\mu=\int_X f\,d\mu+\int_X g\,d\mu

  • \left|\int_X f\,d\mu\right|\le \int_X |f|\,d\mu

  • \int_X |f|\,d\mu=0 \iff f=0 a.e. on X

  • A,B \subset X が互いに素な可測集合なら \int_{A \sqcup B} f\,d\mu=\int_A f\,d\mu+\int_B f\,d\mu

  • \alpha>0 に対して \mu(\{|f|\ge \alpha\})\le \alpha^{-1}\int_X |f|\,d\mu

Lean code for Theorem9.5.1●9 theorems
  • theoremdefined in NoteKsk/«09lintegral-prop».lean
    complete
    theorem NoteKsk.Chapter09.integral_eq_zero_of_measure_univ_zero.{u_1}
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α}
  {f : α → ℝ} (hμ : μ Set.univ = 0) : ∫ (x : α), f x ∂μ = 0
    theorem NoteKsk.Chapter09.integral_eq_zero_of_measure_univ_zero.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {f : α → ℝ} (hμ : μ Set.univ = 0) :
  ∫ (x : α), f x ∂μ = 0
  • theoremdefined in NoteKsk/«09lintegral-prop».lean
    complete
    theorem NoteKsk.Chapter09.integral_aestrongly_congr.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ℝ}
  (hf : MeasureTheory.Integrable f μ) (hfg : f =ᵐ[μ] g) :
  MeasureTheory.Integrable g μ ∧ ∫ (x : α), f x ∂μ = ∫ (x : α), g x ∂μ
    theorem NoteKsk.Chapter09.integral_aestrongly_congr.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {f g : α → ℝ}
  (hf : MeasureTheory.Integrable f μ)
  (hfg : f =ᵐ[μ] g) :
  MeasureTheory.Integrable g μ ∧
    ∫ (x : α), f x ∂μ = ∫ (x : α), g x ∂μ
  • theoremdefined in NoteKsk/«09lintegral-prop».lean
    complete
    theorem NoteKsk.Chapter09.integral_mono_ae_real.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ℝ}
  (hf : MeasureTheory.Integrable f μ)
  (hg : MeasureTheory.Integrable g μ) (hfg : f ≤ᵐ[μ] g) :
  ∫ (x : α), f x ∂μ ≤ ∫ (x : α), g x ∂μ
    theorem NoteKsk.Chapter09.integral_mono_ae_real.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {f g : α → ℝ}
  (hf : MeasureTheory.Integrable f μ)
  (hg : MeasureTheory.Integrable g μ)
  (hfg : f ≤ᵐ[μ] g) :
  ∫ (x : α), f x ∂μ ≤ ∫ (x : α), g x ∂μ
  • theoremdefined in NoteKsk/«09lintegral-prop».lean
    complete
    theorem NoteKsk.Chapter09.integral_const_mul_real.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} (c : ℝ)
  (f : α → ℝ) : ∫ (x : α), c * f x ∂μ = c * ∫ (x : α), f x ∂μ
    theorem NoteKsk.Chapter09.integral_const_mul_real.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α} (c : ℝ)
  (f : α → ℝ) :
  ∫ (x : α), c * f x ∂μ =
    c * ∫ (x : α), f x ∂μ
  • theoremdefined in NoteKsk/«09lintegral-prop».lean
    complete
    theorem NoteKsk.Chapter09.integral_add_real.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ℝ}
  (hf : MeasureTheory.Integrable f μ)
  (hg : MeasureTheory.Integrable g μ) :
  ∫ (x : α), f x + g x ∂μ = ∫ (x : α), f x ∂μ + ∫ (x : α), g x ∂μ
    theorem NoteKsk.Chapter09.integral_add_real.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {f g : α → ℝ}
  (hf : MeasureTheory.Integrable f μ)
  (hg : MeasureTheory.Integrable g μ) :
  ∫ (x : α), f x + g x ∂μ =
    ∫ (x : α), f x ∂μ + ∫ (x : α), g x ∂μ
  • theoremdefined in NoteKsk/«09lintegral-prop».lean
    complete
    theorem NoteKsk.Chapter09.abs_integral_le_integral_abs.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} (f : α → ℝ) :
  |∫ (x : α), f x ∂μ| ≤ ∫ (x : α), |f x| ∂μ
    theorem NoteKsk.Chapter09.abs_integral_le_integral_abs.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  (f : α → ℝ) :
  |∫ (x : α), f x ∂μ| ≤
    ∫ (x : α), |f x| ∂μ
  • theoremdefined in NoteKsk/«09lintegral-prop».lean
    complete
    theorem NoteKsk.Chapter09.integral_abs_eq_zero_iff_ae_eq_zero.{u_1}
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α}
  {f : α → ℝ} (hf : MeasureTheory.Integrable f μ) :
  ∫ (x : α), |f x| ∂μ = 0 ↔ f =ᵐ[μ] 0
    theorem NoteKsk.Chapter09.integral_abs_eq_zero_iff_ae_eq_zero.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {f : α → ℝ}
  (hf : MeasureTheory.Integrable f μ) :
  ∫ (x : α), |f x| ∂μ = 0 ↔ f =ᵐ[μ] 0
  • theoremdefined in NoteKsk/«09lintegral-prop».lean
    complete
    theorem NoteKsk.Chapter09.setIntegral_union_of_disjoint_of_integrable.{u_1}
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α}
  {f : α → ℝ} (hf : MeasureTheory.Integrable f μ) {A B : Set α}
  (hAB : Disjoint A B) (hB : MeasurableSet B) :
  ∫ (x : α) in A ∪ B, f x ∂μ =
    ∫ (x : α) in A, f x ∂μ + ∫ (x : α) in B, f x ∂μ
    theorem NoteKsk.Chapter09.setIntegral_union_of_disjoint_of_integrable.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {f : α → ℝ}
  (hf : MeasureTheory.Integrable f μ)
  {A B : Set α} (hAB : Disjoint A B)
  (hB : MeasurableSet B) :
  ∫ (x : α) in A ∪ B, f x ∂μ =
    ∫ (x : α) in A, f x ∂μ +
      ∫ (x : α) in B, f x ∂μ
  • theoremdefined in NoteKsk/«09lintegral-prop».lean
    complete
    theorem NoteKsk.Chapter09.chebyshev_integrable_abs.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ}
  (hf : MeasureTheory.Integrable f μ) {a : ℝ} (ha : 0 < a) :
  μ {x | a ≤ |f x|} ≤
    (∫⁻ (x : α), ENNReal.ofReal |f x| ∂μ) / ENNReal.ofReal a
    theorem NoteKsk.Chapter09.chebyshev_integrable_abs.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {f : α → ℝ}
  (hf : MeasureTheory.Integrable f μ)
  {a : ℝ} (ha : 0 < a) :
  μ {x | a ≤ |f x|} ≤
    (∫⁻ (x : α),
        ENNReal.ofReal |f x| ∂μ) /
      ENNReal.ofReal a
    The lecture statement
`μ {x | a ≤ |f x|} ≤ a⁻¹ ∫ |f| dμ` is formalized in `ENNReal` form.
The right-hand side uses the lower Lebesgue integral of `ENNReal.ofReal |f|`.
Proof for Theorem 9.5.1
uses 0

各項は順に prop:integral-zero-on-null-set,prop:integral-ae-invariance,prop:integral-monotonicity,prop:integral-homogeneity,prop:integral-additivity,prop:integral-absolute-value-bound,prop:integral-zero-iff-ae-zero,prop:integral-disjoint-additivity,prop:chebyshev-inequality で示した内容である．

Remark. この章で得た公式は，今後の章でほぼ毎回使う． 特に f=g a.e. なら積分値を区別しなくてよいこと，および \left|\int f\right|\le \int |f| という評価は， 収束定理を運用する際の基本になる．

Proposition9.5.2
uses 0used by 0XL∃∀N
Tagsexample

\mu(X)<\infty とし， f\in M(X) が |f(x)|\le M a.e. on X を満たすとする． このとき f は可積分で，\left|\int_X f\,d\mu\right|\le M\,\mu(X) が成り立つ．

Proof for Proposition 9.5.2
uses 0

|f|\le M1_X だから \int_X |f|\,d\mu\le M\,\mu(X)<\infty である． よって f は可積分である． さらにProposition 9.3.3より \left|\int_X f\,d\mu\right|\le \int_X |f|\,d\mu\le M\,\mu(X) である．