7.5. 測度の総和
定義.
X を可測空間とし、I を型、\mu_i を X 上の測度族とする。
それらの 総和 を、任意の可測集合 A \subseteq X に対して
\left(\sum_{i \in I} \mu_i\right)(A) \coloneqq \sum_{i \in I} \mu_i(A)
で定まる測度として定義する。
Lean code
/-- The sum of an indexed family of measures. -/
def sum (μ : ι → Measure X) : Measure X :=
Measure.ofMeasurable (fun A _ ↦ ∑' i, μ i A) (X:Type u_1ι:Type u_2inst✝:MeasurableSpace Xμ:ι → Measure X⊢ (fun A x => ∑' (i : ι), (μ i) A) ∅ ⋯ = 0 All goals completed! 🐙) <| X:Type u_1ι:Type u_2inst✝:MeasurableSpace Xμ:ι → Measure X⊢ ∀ ⦃f : ℕ → Set X⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
Pairwise (Function.onFun Disjoint f) →
(fun A x => ∑' (i : ι), (μ i) A) (⋃ i, f i) ⋯ = ∑' (i : ℕ), (fun A x => ∑' (i : ι), (μ i) A) (f i) ⋯
intro A X:Type u_1ι:Type u_2inst✝:MeasurableSpace Xμ:ι → Measure XA:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)⊢ Pairwise (Function.onFun Disjoint A) →
(fun A x => ∑' (i : ι), (μ i) A) (⋃ i, A i) ⋯ = ∑' (i : ℕ), (fun A x => ∑' (i : ι), (μ i) A) (A i) ⋯ X:Type u_1ι:Type u_2inst✝:MeasurableSpace Xμ:ι → Measure XA:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Function.onFun Disjoint A)⊢ (fun A x => ∑' (i : ι), (μ i) A) (⋃ i, A i) ⋯ = ∑' (i : ℕ), (fun A x => ∑' (i : ι), (μ i) A) (A i) ⋯
X:Type u_1ι:Type u_2inst✝:MeasurableSpace Xμ:ι → Measure XA:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Function.onFun Disjoint A)⊢ (fun A x => ∑' (i : ι), (μ i) A) (⋃ i, A i) ⋯ = ∑' (b : ι) (a : ℕ), (μ b) (A a)
X:Type u_1ι:Type u_2inst✝:MeasurableSpace Xμ:ι → Measure XA:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Function.onFun Disjoint A)⊢ ∀ (b : ι), (μ b) (⋃ i, A i) = ∑' (a : ℕ), (μ b) (A a)
X:Type u_1ι:Type u_2inst✝:MeasurableSpace Xμ:ι → Measure XA:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Function.onFun Disjoint A)i:ι⊢ (μ i) (⋃ i, A i) = ∑' (a : ℕ), (μ i) (A a)
All goals completed! 🐙@[simp]
theorem sum_apply (μ : ι → Measure X) {A : Set X} (hA : MeasurableSet A) :
Measure.sum μ A = ∑' i, μ i A := X:Type u_1ι:Type u_2inst✝:MeasurableSpace Xμ:ι → Measure XA:Set XhA:MeasurableSet A⊢ (sum μ) A = ∑' (i : ι), (μ i) A
X:Type u_1ι:Type u_2inst✝:MeasurableSpace Xμ:ι → Measure XA:Set XhA:MeasurableSet A⊢ (Measure.ofMeasurable (fun A x => ∑' (i : ι), (μ i) A) ⋯ ⋯) A = ∑' (i : ι), (μ i) A
All goals completed! 🐙
補題.
下積分はこの可算和と交換する:
\underline{\int}_{x \in X} f(x)\,d\left(\sum_{i \in I} \mu_i\right)
=
\sum_{i \in I} \underline{\int}_{x \in X} f(x)\,d\mu_i.
Lean code
theorem lintegral_sum_measure (f : X → ℝ≥0∞) (μ : ι → Measure X) :
∫⁻ x, f x ∂(Measure.sum μ) = ∑' i, ∫⁻ x, f x ∂μ i := X:Type u_1ι:Type u_2inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:ι → Measure X⊢ ∫⁻ (x : X), f x ∂Measure.sum μ = ∑' (i : ι), ∫⁻ (x : X), f x ∂μ i
X:Type u_1ι:Type u_2inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:ι → Measure X⊢ ∫⁻ (x : X), f x ∂Measure.sum μ = ⨆ s, ∑ a ∈ s, ∫⁻ (x : X), f x ∂μ a
classical
simp_rw X:Type u_1ι:Type u_2inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:ι → Measure X⊢ ∫⁻ (x : X), f x ∂Measure.sum μ = ⨆ s, ∑ a ∈ s, ∫⁻ (x : X), f x ∂μ a← lintegral_finset_sum_measure, lintegral]
conv_rhs => X:Type u_1ι:Type u_2inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:ι → Measure X| ⨆ j, ⨆ i, ⨆ (_ : ⇑j ≤ fun x => f x), j.lintegral (∑ i ∈ i, μ i)
conv_rhs =>
X:Type u_1ι:Type u_2inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:ι → Measure X| fun j => ⨆ i, ⨆ (_ : ⇑j ≤ fun x => f x), j.lintegral (∑ i ∈ i, μ i)
X:Type u_1ι:Type u_2inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:ι → Measure Xg:X →ₛ ℝ≥0∞| ⨆ i, ⨆ (_ : ⇑g ≤ fun x => f x), g.lintegral (∑ i ∈ i, μ i)
X:Type u_1ι:Type u_2inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:ι → Measure Xg:X →ₛ ℝ≥0∞| ⨆ (_ : ⇑g ≤ fun x => f x), ⨆ i, g.lintegral (∑ i ∈ i, μ i)
X:Type u_1ι:Type u_2inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:ι → Measure X⊢ ∀ (i : X →ₛ ℝ≥0∞),
⨆ (_ : ⇑i ≤ fun x => f x), i.lintegral (Measure.sum μ) =
⨆ (_ : ⇑i ≤ fun x => f x), ⨆ i_1, i.lintegral (∑ i ∈ i_1, μ i)
X:Type u_1ι:Type u_2inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:ι → Measure Xg:X →ₛ ℝ≥0∞⊢ ⨆ (_ : ⇑g ≤ fun x => f x), g.lintegral (Measure.sum μ) = ⨆ (_ : ⇑g ≤ fun x => f x), ⨆ i, g.lintegral (∑ i ∈ i, μ i)
X:Type u_1ι:Type u_2inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:ι → Measure Xg:X →ₛ ℝ≥0∞⊢ (⇑g ≤ fun x => f x) → g.lintegral (Measure.sum μ) = ⨆ i, g.lintegral (∑ i ∈ i, μ i)
X:Type u_1ι:Type u_2inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:ι → Measure Xg:X →ₛ ℝ≥0∞hg:⇑g ≤ fun x => f x⊢ g.lintegral (Measure.sum μ) = ⨆ i, g.lintegral (∑ i ∈ i, μ i)
simp_rw X:Type u_1ι:Type u_2inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:ι → Measure Xg:X →ₛ ℝ≥0∞hg:⇑g ≤ fun x => f x⊢ g.lintegral (Measure.sum μ) = ⨆ i, g.lintegral (∑ i ∈ i, μ i)MTI.SimpleFunc.lintegral_finset_sum]
X:Type u_1ι:Type u_2inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:ι → Measure Xg:X →ₛ ℝ≥0∞hg:⇑g ≤ fun x => f x⊢ ∑' (i : ι), g.lintegral (μ i) = ⨆ i, ∑ i ∈ i, g.lintegral (μ i)
All goals completed! 🐙