Lebesgue積分講義ノート

9.2. 集合に関する性質🔗

Proposition9.2.1
uses 1used by 1✓L∃∀N
Tagsleanok

零集合上では積分は消える. \mu(X)=0 で f\in\calL^1(X) ならば \int_X f\,d\mu=0 が成り立つ．

Lean code for Proposition9.2.1●2 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.setIntegral_eq_zero_of_measure_zero.{u_1}
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α}
  {N : Set α} (hN : μ N = 0) (f : α → ℝ) : ∫ (x : α) in N, f x ∂μ = 0
    theorem NoteKsk.Chapter09.setIntegral_eq_zero_of_measure_zero.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {N : Set α} (hN : μ N = 0) (f : α → ℝ) :
  ∫ (x : α) in N, f x ∂μ = 0
Proof for Proposition 9.2.1
uses 0

Proposition 8.4.7そのものである．

Proposition9.2.2
Statement uses 2
Statement dependency previews
Preview
Proposition 8.2.6
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
used by 1✓L∃∀N
Tagsleanok

互いに素な集合への加法性. A,B \subset X を互いに素な可測集合とし， f\in\calL^1(X) とする． このとき \int_{A \sqcup B} f\,d\mu=\int_A f\,d\mu+\int_B f\,d\mu が成り立つ．

Lean code for Proposition9.2.2●2 theorems
  • theoremdefined in NoteKsk/«09lintegral-prop».lean
    complete
    theorem NoteKsk.Chapter09.setIntegral_union_of_disjoint.{u_1, u_2}
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α}
  {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : α → E}
  {A B : Set α} (hAB : Disjoint A B) (hB : MeasurableSet B)
  (hfA : MeasureTheory.IntegrableOn f A μ)
  (hfB : MeasureTheory.IntegrableOn f B μ) :
  ∫ (x : α) in A ∪ B, f x ∂μ =
    ∫ (x : α) in A, f x ∂μ + ∫ (x : α) in B, f x ∂μ
    theorem NoteKsk.Chapter09.setIntegral_union_of_disjoint.{u_1,
    u_2}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {E : Type u_2} [NormedAddCommGroup E]
  [NormedSpace ℝ E] {f : α → E}
  {A B : Set α} (hAB : Disjoint A B)
  (hB : MeasurableSet B)
  (hfA : MeasureTheory.IntegrableOn f A μ)
  (hfB :
    MeasureTheory.IntegrableOn f 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.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 ∂μ
Proof for Proposition 9.2.2
uses 0

f=f^+-f^- と書く． f^+,f^- は非負可積分だから，Proposition 8.2.6より \int_{A \sqcup B} f^+\,d\mu=\int_A f^+\,d\mu+\int_B f^+\,d\mu および \int_{A \sqcup B} f^-\,d\mu=\int_A f^-\,d\mu+\int_B f^-\,d\mu が成り立つ． したがって

\int_{A \sqcup B} f\,d\mu =\int_{A \sqcup B} f^+\,d\mu-\int_{A \sqcup B} f^-\,d\mu =\int_A f\,d\mu+\int_B f\,d\mu.

Proposition9.2.3
uses 1
Used by 4
Reverse dependency previews
Preview
Proposition 9.3.1
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N
Tagsleanok

a.e. 不変性. f,g\in\calL^1(X) とする． もし f=g a.e. on X ならば \int_X f\,d\mu=\int_X g\,d\mu が成り立つ．

Lean code for Proposition9.2.3●3 theorems
  • theoremdefined in NoteKsk/«09lintegral-prop».lean
    complete
    theorem NoteKsk.Chapter09.integral_congr_ae.{u_1, u_2} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} {E : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : α → E}
  (hfg : f =ᵐ[μ] g) : ∫ (x : α), f x ∂μ = ∫ (x : α), g x ∂μ
    theorem NoteKsk.Chapter09.integral_congr_ae.{u_1,
    u_2}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {E : Type u_2} [NormedAddCommGroup E]
  [NormedSpace ℝ E] {f g : α → E}
  (hfg : f =ᵐ[μ] g) :
  ∫ (x : α), f x ∂μ = ∫ (x : α), g x ∂μ
  • theoremdefined in NoteKsk/«09lintegral-prop».lean
    complete
    theorem NoteKsk.Chapter09.integrable_congr_ae.{u_1, u_2} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} {E : Type u_2}
  [TopologicalSpace E] [ContinuousENorm E] {f g : α → E}
  (hf : MeasureTheory.Integrable f μ) (hfg : f =ᵐ[μ] g) :
  MeasureTheory.Integrable g μ
    theorem NoteKsk.Chapter09.integrable_congr_ae.{u_1,
    u_2}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {E : Type u_2} [TopologicalSpace E]
  [ContinuousENorm E] {f g : α → E}
  (hf : MeasureTheory.Integrable f μ)
  (hfg : f =ᵐ[μ] g) :
  MeasureTheory.Integrable g μ
  • 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 ∂μ
Proof for Proposition 9.2.3
uses 0

Proposition 8.4.8そのものである．