測度論と積分

4.3. 測度に付随する外測度🔗

🔗
定義 (測度に付随する外測度).

X を可測空間とし、\mu を X 上の測度とする。 このとき関数 \mu^* : \mathcal{P}(X) \to [0,\infty] を \mu^*(A) \coloneqq \inf_{\substack{B \subseteq X,\\ \text{$B$ is measurable},\, A \subseteq B}} \mu(B) によって定める。ただし A \subseteq X は任意とする。 この関数 \mu^* を \mu に付随する外測度 という。

Lean code
def Measure.toOuterMeasure (μ : Measure X) (A : Set X) : ℝ≥0∞ := ⨅ (B : Set X) (_ : A ⊆ B) (hB : MeasurableSet B), μ.toFun B hB
補題.

A \subseteq X が可測ならば、全ての部分集合へ拡張した値は元の値と一致する: \mu^*(A) = \mu(A).

Lean code
@[simp] theorem Measure.toFun_apply (μ : Measure X) {A : Set X} (hA : MeasurableSet A) : μ.toFun A hA = μ A := X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet A⊢ μ.toFun A hA = μ A X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet A⊢ μ A = μ.toFun A hA X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet A⊢ μ.toFun A hA ≤ ⨅ i, ⨅ (_ : A ⊆ i), ⨅ (hB : MeasurableSet i), μ.toFun i hB X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set XhAB:A ⊆ BhB:MeasurableSet B⊢ μ.toFun A hA ≤ μ.toFun B hB have hB' : B = A ∪ (B \ A) := X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet A⊢ μ.toFun A hA = μ A All goals completed! 🐙 X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set XhAB:A ⊆ BhB:MeasurableSet BhB':B = A ∪ B \ A := toFun_apply._proof_1 B hABhABA:MeasurableSet (A ∪ B \ A) := MeasurableSet.union hA (MeasurableSet.diff hB hA)⊢ μ.toFun A hA ≤ μ.toFun B hB calc μ.toFun A hA ≤ μ.toFun A hA + μ.toFun (B \ A) (hB.diff hA) := le_self_add _ = μ.toFun (A ∪ (B \ A)) hABA := (μ.union' _ _ (X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set XhAB:A ⊆ BhB:MeasurableSet BhB':B = A ∪ B \ A := toFun_apply._proof_1 B hABhABA:MeasurableSet (A ∪ B \ A) := MeasurableSet.union hA (MeasurableSet.diff hB hA)⊢ Disjoint A (B \ A) All goals completed! 🐙)).symm _ = μ.toFun B hB := X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set XhAB:A ⊆ BhB:MeasurableSet BhB':B = A ∪ B \ A := toFun_apply._proof_1 B hABhABA:MeasurableSet (A ∪ B \ A) := MeasurableSet.union hA (MeasurableSet.diff hB hA)⊢ μ.toFun (A ∪ B \ A) hABA = μ.toFun B hB All goals completed! 🐙
補題.

X 上の測度 \mu に付随する外測度は、次の 3 つの性質を満たす。

  1. \mu^*(\emptyset) = 0

  2. A \subseteq B ならば \mu^*(A) \le \mu^*(B)。

  3. 任意の部分集合列 A_0, A_1, \dots \subseteq X に対して

    \mu^*\left(\bigcup_{n \in \mathbb{N}} A_n\right) \le \sum_{n \in \mathbb{N}} \mu^*(A_n).

Lean code
@[simp] theorem Measure.empty (μ : Measure X) : μ ∅ = 0 := X:Type u_1inst✝:MeasurableSpace Xμ:Measure X⊢ μ ∅ = 0 X:Type u_1inst✝:MeasurableSpace Xμ:Measure X⊢ μ.toFun ∅ ⋯ = 0 All goals completed! 🐙
theorem Measure.mono (μ : Measure X) {A B : Set X} (h : A ⊆ B) : μ A ≤ μ B := le_iInf fun C ↦ le_iInf fun hBC ↦ le_iInf fun hC ↦ iInf₂_le_of_le C (h.trans hBC) (iInf_le_of_le hC (le_of_eq rfl))
theorem Measure.iUnion_le (μ : Measure X) (A : ℕ → Set X) : μ (⋃ i, A i) ≤ ∑' i, μ (A i) := X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:ℕ → Set X⊢ μ (⋃ i, A i) ≤ ∑' (i : ℕ), μ (A i) X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:ℕ → Set X⊢ ∀ (ε : NNReal), 0 < ε → ∑' (i : ℕ), μ (A i) < ∞ → μ (⋃ i, A i) ≤ ∑' (i : ℕ), μ (A i) + ↑ε intro ε X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:ℕ → Set Xε:NNRealhε:0 < ε⊢ ∑' (i : ℕ), μ (A i) < ∞ → μ (⋃ i, A i) ≤ ∑' (i : ℕ), μ (A i) + ↑ε X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:ℕ → Set Xε:NNRealhε:0 < εhb:∑' (i : ℕ), μ (A i) < ∞⊢ μ (⋃ i, A i) ≤ ∑' (i : ℕ), μ (A i) + ↑ε X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:ℕ → Set Xε:NNRealhε:0 < εhb:∑' (i : ℕ), μ (A i) < ∞ε':ℕ → NNRealhε':∀ (i : ℕ), 0 < ε' ihεsum:∑' (i : ℕ), ↑(ε' i) < ↑ε⊢ μ (⋃ i, A i) ≤ ∑' (i : ℕ), μ (A i) + ↑ε choose B hAB hB hlt using show ∀ i, ∃ B : Set X, ∃ hAB : A i ⊆ B, ∃ hB : MeasurableSet B, μ.toFun B hB < μ (A i) + ε' i X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:ℕ → Set X⊢ μ (⋃ i, A i) ≤ ∑' (i : ℕ), μ (A i) X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:ℕ → Set Xε:NNRealhε:0 < εhb:∑' (i : ℕ), μ (A i) < ∞ε':ℕ → NNRealhε':∀ (i : ℕ), 0 < ε' ihεsum:∑' (i : ℕ), ↑(ε' i) < ↑εi:ℕ⊢ ∃ B, ∃ (_ : A i ⊆ B) (hB : MeasurableSet B), μ.toFun B hB < μ (A i) + ↑(ε' i) have hlt : μ (A i) < μ (A i) + ε' i := X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:ℕ → Set X⊢ μ (⋃ i, A i) ≤ ∑' (i : ℕ), μ (A i) exact ENNReal.lt_add_right (ne_top_of_le_ne_top hb.ne <| ENNReal.le_tsum _) (X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:ℕ → Set Xε:NNRealhε:0 < εhb:∑' (i : ℕ), μ (A i) < ∞ε':ℕ → NNRealhε':∀ (i : ℕ), 0 < ε' ihεsum:∑' (i : ℕ), ↑(ε' i) < ↑εi:ℕ⊢ ↑(ε' i) ≠ 0 All goals completed! 🐙) X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:ℕ → Set Xε:NNRealhε:0 < εhb:∑' (i : ℕ), μ (A i) < ∞ε':ℕ → NNRealhε':∀ (i : ℕ), 0 < ε' ihεsum:∑' (i : ℕ), ↑(ε' i) < ↑εi:ℕhlt:⨅ B, ⨅ (_ : A i ⊆ B), ⨅ (hB : MeasurableSet B), μ.toFun B hB < (⨅ B, ⨅ (_ : A i ⊆ B), ⨅ (hB : MeasurableSet B), μ.toFun B hB) + ↑(ε' i)⊢ ∃ B, ∃ (_ : A i ⊆ B) (hB : MeasurableSet B), μ.toFun B hB < μ (A i) + ↑(ε' i) X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:ℕ → Set Xε:NNRealhε:0 < εhb:∑' (i : ℕ), μ (A i) < ∞ε':ℕ → NNRealhε':∀ (i : ℕ), 0 < ε' ihεsum:∑' (i : ℕ), ↑(ε' i) < ↑εi:ℕhlt:⨅ B, ⨅ (_ : A i ⊆ B), ⨅ (hB : MeasurableSet B), μ.toFun B hB < (⨅ B, ⨅ (_ : A i ⊆ B), ⨅ (hB : MeasurableSet B), μ.toFun B hB) + ↑(ε' i)B:Set XhltB:⨅ (_ : A i ⊆ B), ⨅ (hB : MeasurableSet B), μ.toFun B hB < (⨅ B, ⨅ (_ : A i ⊆ B), ⨅ (hB : MeasurableSet B), μ.toFun B hB) + ↑(ε' i)⊢ ∃ B, ∃ (_ : A i ⊆ B) (hB : MeasurableSet B), μ.toFun B hB < μ (A i) + ↑(ε' i) X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:ℕ → Set Xε:NNRealhε:0 < εhb:∑' (i : ℕ), μ (A i) < ∞ε':ℕ → NNRealhε':∀ (i : ℕ), 0 < ε' ihεsum:∑' (i : ℕ), ↑(ε' i) < ↑εi:ℕhlt:⨅ B, ⨅ (_ : A i ⊆ B), ⨅ (hB : MeasurableSet B), μ.toFun B hB < (⨅ B, ⨅ (_ : A i ⊆ B), ⨅ (hB : MeasurableSet B), μ.toFun B hB) + ↑(ε' i)B:Set XhltB✝:⨅ (_ : A i ⊆ B), ⨅ (hB : MeasurableSet B), μ.toFun B hB < (⨅ B, ⨅ (_ : A i ⊆ B), ⨅ (hB : MeasurableSet B), μ.toFun B hB) + ↑(ε' i)hAB:A i ⊆ BhltB:⨅ (hB : MeasurableSet B), μ.toFun B hB < (⨅ B, ⨅ (_ : A i ⊆ B), ⨅ (hB : MeasurableSet B), μ.toFun B hB) + ↑(ε' i)⊢ ∃ B, ∃ (_ : A i ⊆ B) (hB : MeasurableSet B), μ.toFun B hB < μ (A i) + ↑(ε' i) X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:ℕ → Set Xε:NNRealhε:0 < εhb:∑' (i : ℕ), μ (A i) < ∞ε':ℕ → NNRealhε':∀ (i : ℕ), 0 < ε' ihεsum:∑' (i : ℕ), ↑(ε' i) < ↑εi:ℕhlt:⨅ B, ⨅ (_ : A i ⊆ B), ⨅ (hB : MeasurableSet B), μ.toFun B hB < (⨅ B, ⨅ (_ : A i ⊆ B), ⨅ (hB : MeasurableSet B), μ.toFun B hB) + ↑(ε' i)B:Set XhltB✝¹:⨅ (_ : A i ⊆ B), ⨅ (hB : MeasurableSet B), μ.toFun B hB < (⨅ B, ⨅ (_ : A i ⊆ B), ⨅ (hB : MeasurableSet B), μ.toFun B hB) + ↑(ε' i)hAB:A i ⊆ BhltB✝:⨅ (hB : MeasurableSet B), μ.toFun B hB < (⨅ B, ⨅ (_ : A i ⊆ B), ⨅ (hB : MeasurableSet B), μ.toFun B hB) + ↑(ε' i)hB:MeasurableSet BhltB:μ.toFun B hB < (⨅ B, ⨅ (_ : A i ⊆ B), ⨅ (hB : MeasurableSet B), μ.toFun B hB) + ↑(ε' i)⊢ ∃ B, ∃ (_ : A i ⊆ B) (hB : MeasurableSet B), μ.toFun B hB < μ (A i) + ↑(ε' i) All goals completed! 🐙 have hsub : (⋃ i, A i) ⊆ ⋃ i, B i := X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:ℕ → Set X⊢ μ (⋃ i, A i) ≤ ∑' (i : ℕ), μ (A i) All goals completed! 🐙 have hlt' : ∀ i, μ (B i) < μ (A i) + ε' i := X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:ℕ → Set X⊢ μ (⋃ i, A i) ≤ ∑' (i : ℕ), μ (A i) X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:ℕ → Set Xε:NNRealhε:0 < εhb:∑' (i : ℕ), μ (A i) < ∞ε':ℕ → NNRealhε':∀ (i : ℕ), 0 < ε' ihεsum:∑' (i : ℕ), ↑(ε' i) < ↑εB:ℕ → Set XhAB:∀ (i : ℕ), A i ⊆ B ihB:∀ (i : ℕ), MeasurableSet (B i)hlt:∀ (i : ℕ), μ.toFun (B i) ⋯ < μ (A i) + ↑(ε' i)hsub:⋃ i, A i ⊆ ⋃ i, B i := iUnion_subset fun i => HasSubset.Subset.trans (hAB i) (subset_iUnion B i)i:ℕ⊢ μ (B i) < μ (A i) + ↑(ε' i) All goals completed! 🐙 calc μ (⋃ i, A i) ≤ μ (⋃ i, B i) := μ.mono hsub _ ≤ ∑' i, μ (B i) := μ.iUnion_le_of_measurable hB _ ≤ ∑' i, (μ (A i) + ε' i) := X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:ℕ → Set Xε:NNRealhε:0 < εhb:∑' (i : ℕ), μ (A i) < ∞ε':ℕ → NNRealhε':∀ (i : ℕ), 0 < ε' ihεsum:∑' (i : ℕ), ↑(ε' i) < ↑εB:ℕ → Set XhAB:∀ (i : ℕ), A i ⊆ B ihB:∀ (i : ℕ), MeasurableSet (B i)hlt:∀ (i : ℕ), μ.toFun (B i) ⋯ < μ (A i) + ↑(ε' i)hsub:⋃ i, A i ⊆ ⋃ i, B i := iUnion_subset fun i => HasSubset.Subset.trans (hAB i) (subset_iUnion B i)hlt':∀ (i : ℕ), μ (B i) < μ (A i) + ↑(ε' i) := fun i => Eq.mp (congrFun' (congrArg LT.lt (toFun_apply μ (hB i))) (μ (A i) + ↑(ε' i))) (hlt i)⊢ ∑' (i : ℕ), μ (B i) ≤ ∑' (i : ℕ), (μ (A i) + ↑(ε' i)) All goals completed! 🐙 _ = ∑' i, μ (A i) + ∑' i, (ε' i : ℝ≥0∞) := X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:ℕ → Set Xε:NNRealhε:0 < εhb:∑' (i : ℕ), μ (A i) < ∞ε':ℕ → NNRealhε':∀ (i : ℕ), 0 < ε' ihεsum:∑' (i : ℕ), ↑(ε' i) < ↑εB:ℕ → Set XhAB:∀ (i : ℕ), A i ⊆ B ihB:∀ (i : ℕ), MeasurableSet (B i)hlt:∀ (i : ℕ), μ.toFun (B i) ⋯ < μ (A i) + ↑(ε' i)hsub:⋃ i, A i ⊆ ⋃ i, B i := iUnion_subset fun i => HasSubset.Subset.trans (hAB i) (subset_iUnion B i)hlt':∀ (i : ℕ), μ (B i) < μ (A i) + ↑(ε' i) := fun i => Eq.mp (congrFun' (congrArg LT.lt (toFun_apply μ (hB i))) (μ (A i) + ↑(ε' i))) (hlt i)⊢ ∑' (i : ℕ), (μ (A i) + ↑(ε' i)) = ∑' (i : ℕ), μ (A i) + ∑' (i : ℕ), ↑(ε' i) All goals completed! 🐙 _ ≤ ∑' i, μ (A i) + ε := X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:ℕ → Set Xε:NNRealhε:0 < εhb:∑' (i : ℕ), μ (A i) < ∞ε':ℕ → NNRealhε':∀ (i : ℕ), 0 < ε' ihεsum:∑' (i : ℕ), ↑(ε' i) < ↑εB:ℕ → Set XhAB:∀ (i : ℕ), A i ⊆ B ihB:∀ (i : ℕ), MeasurableSet (B i)hlt:∀ (i : ℕ), μ.toFun (B i) ⋯ < μ (A i) + ↑(ε' i)hsub:⋃ i, A i ⊆ ⋃ i, B i := iUnion_subset fun i => HasSubset.Subset.trans (hAB i) (subset_iUnion B i)hlt':∀ (i : ℕ), μ (B i) < μ (A i) + ↑(ε' i) := fun i => Eq.mp (congrFun' (congrArg LT.lt (toFun_apply μ (hB i))) (μ (A i) + ↑(ε' i))) (hlt i)⊢ ∑' (i : ℕ), μ (A i) + ∑' (i : ℕ), ↑(ε' i) ≤ ∑' (i : ℕ), μ (A i) + ↑ε All goals completed! 🐙
補題.

A \subseteq X が可測ならば、A は \mu に付随する外測度 \mu^* に関してカラテオドリである。 すなわち、任意の部分集合 B \subseteq X に対して \mu^*(B) = \mu^*(B \cap A) + \mu^*(B \setminus A). が成り立つ。

Lean code
theorem Measure.toOuterMeasure_caratheodory (μ : Measure X) {A : Set X} (hA : MeasurableSet A) (B : Set X) : μ B = μ (B ∩ A) + μ (B \ A) := X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set X⊢ μ B = μ (B ∩ A) + μ (B \ A) X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set X⊢ μ B ≤ μ (B ∩ A) + μ (B \ A)X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set X⊢ μ (B ∩ A) + μ (B \ A) ≤ μ B X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set X⊢ μ B ≤ μ (B ∩ A) + μ (B \ A) calc μ B = μ ((B ∩ A) ∪ (B \ A)) := X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set X⊢ μ B = μ (B ∩ A ∪ B \ A) have hBA : ((B ∩ A) ∪ (B \ A)) = B := X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set X⊢ μ B = μ (B ∩ A ∪ B \ A) X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set Xx:X⊢ x ∈ B ∩ A ∪ B \ A ↔ x ∈ B All goals completed! 🐙 All goals completed! 🐙 _ ≤ μ (B ∩ A) + μ (B \ A) := μ.union_le _ _ X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set X⊢ μ (B ∩ A) + μ (B \ A) ≤ μ B X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set X⊢ (⨅ B_1, ⨅ (_ : B ∩ A ⊆ B_1), ⨅ (hB : MeasurableSet B_1), μ.toFun B_1 hB) + μ (B \ A) ≤ μ B X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set X⊢ ∀ (i : Set X), (⨅ B_1, ⨅ (_ : B ∩ A ⊆ B_1), ⨅ (hB : MeasurableSet B_1), μ.toFun B_1 hB) + μ (B \ A) ≤ ⨅ (_ : B ⊆ i), ⨅ (hB : MeasurableSet i), μ.toFun i hB X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set XC:Set X⊢ (⨅ B_1, ⨅ (_ : B ∩ A ⊆ B_1), ⨅ (hB : MeasurableSet B_1), μ.toFun B_1 hB) + μ (B \ A) ≤ ⨅ (_ : B ⊆ C), ⨅ (hB : MeasurableSet C), μ.toFun C hB X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set XC:Set X⊢ B ⊆ C → (⨅ B_1, ⨅ (_ : B ∩ A ⊆ B_1), ⨅ (hB : MeasurableSet B_1), μ.toFun B_1 hB) + μ (B \ A) ≤ ⨅ (hB : MeasurableSet C), μ.toFun C hB X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set XC:Set XhBC:B ⊆ C⊢ (⨅ B_1, ⨅ (_ : B ∩ A ⊆ B_1), ⨅ (hB : MeasurableSet B_1), μ.toFun B_1 hB) + μ (B \ A) ≤ ⨅ (hB : MeasurableSet C), μ.toFun C hB X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set XC:Set XhBC:B ⊆ C⊢ ∀ (i : MeasurableSet C), (⨅ B_1, ⨅ (_ : B ∩ A ⊆ B_1), ⨅ (hB : MeasurableSet B_1), μ.toFun B_1 hB) + μ (B \ A) ≤ μ.toFun C i X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set XC:Set XhBC:B ⊆ ChC:MeasurableSet C⊢ (⨅ B_1, ⨅ (_ : B ∩ A ⊆ B_1), ⨅ (hB : MeasurableSet B_1), μ.toFun B_1 hB) + μ (B \ A) ≤ μ.toFun C hC calc μ (B ∩ A) + μ (B \ A) ≤ μ (C ∩ A) + μ (C \ A) := X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set XC:Set XhBC:B ⊆ ChC:MeasurableSet C⊢ μ (B ∩ A) + μ (B \ A) ≤ μ (C ∩ A) + μ (C \ A) exact add_le_add (μ.mono (X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set XC:Set XhBC:B ⊆ ChC:MeasurableSet C⊢ B ∩ A ⊆ C ∩ A intro x X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set XC:Set XhBC:B ⊆ ChC:MeasurableSet Cx:Xhx:x ∈ B ∩ A⊢ x ∈ C ∩ A All goals completed! 🐙)) (μ.mono (X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set XC:Set XhBC:B ⊆ ChC:MeasurableSet C⊢ B \ A ⊆ C \ A intro x X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set XC:Set XhBC:B ⊆ ChC:MeasurableSet Cx:Xhx:x ∈ B \ A⊢ x ∈ C \ A All goals completed! 🐙)) _ = μ ((C ∩ A) ∪ (C \ A)) := X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set XC:Set XhBC:B ⊆ ChC:MeasurableSet C⊢ μ (C ∩ A) + μ (C \ A) = μ (C ∩ A ∪ C \ A) X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set XC:Set XhBC:B ⊆ ChC:MeasurableSet C⊢ μ (C ∩ A ∪ C \ A) = μ (C ∩ A) + μ (C \ A) X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set XC:Set XhBC:B ⊆ ChC:MeasurableSet C⊢ Disjoint (C ∩ A) (C \ A) All goals completed! 🐙 _ = μ.toFun C hC := X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set XC:Set XhBC:B ⊆ ChC:MeasurableSet C⊢ μ (C ∩ A ∪ C \ A) = μ.toFun C hC X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set XC:Set XhBC:B ⊆ ChC:MeasurableSet C⊢ μ C = μ.toFun C hC All goals completed! 🐙
補題.

逆に、関数 \bar{\mu} : \mathcal{P}(X) \to [0,\infty] が次を満たすとする。

  1. \bar{\mu}(\emptyset) = 0 である。

  2. A \subseteq B ならば \bar{\mu}(A) \le \bar{\mu}(B). が成り立つ。

  3. 任意の部分集合列 A_0, A_1, \dots \subseteq X に対して \bar{\mu}\left(\bigcup_{n \in \mathbb{N}} A_n\right) \le \sum_{n \in \mathbb{N}} \bar{\mu}(A_n). が成り立つ。

さらに、任意の可測集合 A \subseteq X がカラテオドリであるとする。すなわち、任意の部分集合 B \subseteq X に対して \bar{\mu}(B) = \bar{\mu}(B \cap A) + \bar{\mu}(B \setminus A). が成り立つとする。 このとき \bar{\mu} を可測集合に制限すると、X 上の測度が定まる。

Lean code
/-- If a function on all subsets satisfies the three outer-measure axioms and every measurable set is Carathéodory, then restricting it to measurable sets defines a measure. -/ def Measure.ofOuterMeasure (μ : Set X → ℝ≥0∞) (μ_empty : μ ∅ = 0) (μ_mono : Monotone μ) (μ_iUnion_le : ∀ A : ℕ → Set X, μ (⋃ i, A i) ≤ ∑' i, μ (A i)) (μ_caratheodory : ∀ {A : Set X}, MeasurableSet A → ∀ B : Set X, μ B = μ (B ∩ A) + μ (B \ A)) : Measure X := X:Type u_1inst✝:MeasurableSpace Xμ:Set X → ℝ≥0∞μ_empty:μ ∅ = 0μ_mono:Monotone μμ_iUnion_le:∀ (A : ℕ → Set X), μ (⋃ i, A i) ≤ ∑' (i : ℕ), μ (A i)μ_caratheodory:∀ {A : Set X}, MeasurableSet A → ∀ (B : Set X), μ B = μ (B ∩ A) + μ (B \ A)⊢ Measure X refine Measure.ofCountablyAdditive (fun A _ ↦ μ A) (X:Type u_1inst✝:MeasurableSpace Xμ:Set X → ℝ≥0∞μ_empty:μ ∅ = 0μ_mono:Monotone μμ_iUnion_le:∀ (A : ℕ → Set X), μ (⋃ i, A i) ≤ ∑' (i : ℕ), μ (A i)μ_caratheodory:∀ {A : Set X}, MeasurableSet A → ∀ (B : Set X), μ B = μ (B ∩ A) + μ (B \ A)⊢ (fun A x => μ A) ∅ ⋯ = 0 All goals completed! 🐙) ?_ intro A X:Type u_1inst✝:MeasurableSpace Xμ:Set X → ℝ≥0∞μ_empty:μ ∅ = 0μ_mono:Monotone μμ_iUnion_le:∀ (A : ℕ → Set X), μ (⋃ i, A i) ≤ ∑' (i : ℕ), μ (A i)μ_caratheodory:∀ {A : Set X}, MeasurableSet A → ∀ (B : Set X), μ B = μ (B ∩ A) + μ (B \ A)A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)⊢ Pairwise (Disjoint on A) → (fun A x => μ A) (⋃ i, A i) ⋯ = ∑' (i : ℕ), (fun A x => μ A) (A i) ⋯ X:Type u_1inst✝:MeasurableSpace Xμ:Set X → ℝ≥0∞μ_empty:μ ∅ = 0μ_mono:Monotone μμ_iUnion_le:∀ (A : ℕ → Set X), μ (⋃ i, A i) ≤ ∑' (i : ℕ), μ (A i)μ_caratheodory:∀ {A : Set X}, MeasurableSet A → ∀ (B : Set X), μ B = μ (B ∩ A) + μ (B \ A)A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)⊢ (fun A x => μ A) (⋃ i, A i) ⋯ = ∑' (i : ℕ), (fun A x => μ A) (A i) ⋯ have h_union : ∀ {S T : Set X}, MeasurableSet S → Disjoint S T → μ (S ∪ T) = μ S + μ T := X:Type u_1inst✝:MeasurableSpace Xμ:Set X → ℝ≥0∞μ_empty:μ ∅ = 0μ_mono:Monotone μμ_iUnion_le:∀ (A : ℕ → Set X), μ (⋃ i, A i) ≤ ∑' (i : ℕ), μ (A i)μ_caratheodory:∀ {A : Set X}, MeasurableSet A → ∀ (B : Set X), μ B = μ (B ∩ A) + μ (B \ A)⊢ Measure X intro S X:Type u_1inst✝:MeasurableSpace Xμ:Set X → ℝ≥0∞μ_empty:μ ∅ = 0μ_mono:Monotone μμ_iUnion_le:∀ (A : ℕ → Set X), μ (⋃ i, A i) ≤ ∑' (i : ℕ), μ (A i)μ_caratheodory:∀ {A : Set X}, MeasurableSet A → ∀ (B : Set X), μ B = μ (B ∩ A) + μ (B \ A)A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)S:Set XT:Set X⊢ MeasurableSet S → Disjoint S T → μ (S ∪ T) = μ S + μ T X:Type u_1inst✝:MeasurableSpace Xμ:Set X → ℝ≥0∞μ_empty:μ ∅ = 0μ_mono:Monotone μμ_iUnion_le:∀ (A : ℕ → Set X), μ (⋃ i, A i) ≤ ∑' (i : ℕ), μ (A i)μ_caratheodory:∀ {A : Set X}, MeasurableSet A → ∀ (B : Set X), μ B = μ (B ∩ A) + μ (B \ A)A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)S:Set XT:Set XhS:MeasurableSet S⊢ Disjoint S T → μ (S ∪ T) = μ S + μ T X:Type u_1inst✝:MeasurableSpace Xμ:Set X → ℝ≥0∞μ_empty:μ ∅ = 0μ_mono:Monotone μμ_iUnion_le:∀ (A : ℕ → Set X), μ (⋃ i, A i) ≤ ∑' (i : ℕ), μ (A i)μ_caratheodory:∀ {A : Set X}, MeasurableSet A → ∀ (B : Set X), μ B = μ (B ∩ A) + μ (B \ A)A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)S:Set XT:Set XhS:MeasurableSet ShST:Disjoint S T⊢ μ (S ∪ T) = μ S + μ T have hdiff : (S ∪ T) \ S = T := X:Type u_1inst✝:MeasurableSpace Xμ:Set X → ℝ≥0∞μ_empty:μ ∅ = 0μ_mono:Monotone μμ_iUnion_le:∀ (A : ℕ → Set X), μ (⋃ i, A i) ≤ ∑' (i : ℕ), μ (A i)μ_caratheodory:∀ {A : Set X}, MeasurableSet A → ∀ (B : Set X), μ B = μ (B ∩ A) + μ (B \ A)⊢ Measure X All goals completed! 🐙 calc μ (S ∪ T) = μ ((S ∪ T) ∩ S) + μ ((S ∪ T) \ S) := μ_caratheodory hS _ _ = μ S + μ T := X:Type u_1inst✝:MeasurableSpace Xμ:Set X → ℝ≥0∞μ_empty:μ ∅ = 0μ_mono:Monotone μμ_iUnion_le:∀ (A : ℕ → Set X), μ (⋃ i, A i) ≤ ∑' (i : ℕ), μ (A i)μ_caratheodory:∀ {A : Set X}, MeasurableSet A → ∀ (B : Set X), μ B = μ (B ∩ A) + μ (B \ A)A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)S:Set XT:Set XhS:MeasurableSet ShST:Disjoint S Thdiff:(S ∪ T) \ S = T := Eq.mpr (id (Eq.trans (congrFun' (congrArg Eq union_diff_left) T) sdiff_eq_left._simp_1)) (Eq.mp (Eq.trans (congrFun' (congrArg Eq union_diff_left) T) sdiff_eq_left._simp_1) (Disjoint.sup_sdiff_cancel_left hST))⊢ μ ((S ∪ T) ∩ S) + μ ((S ∪ T) \ S) = μ S + μ T All goals completed! 🐙 X:Type u_1inst✝:MeasurableSpace Xμ:Set X → ℝ≥0∞μ_empty:μ ∅ = 0μ_mono:Monotone μμ_iUnion_le:∀ (A : ℕ → Set X), μ (⋃ i, A i) ≤ ∑' (i : ℕ), μ (A i)μ_caratheodory:∀ {A : Set X}, MeasurableSet A → ∀ (B : Set X), μ B = μ (B ∩ A) + μ (B \ A)A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)h_union:∀ {S T : Set X}, MeasurableSet S → Disjoint S T → μ (S ∪ T) = μ S + μ T := fun {S T} hS hST => have hdiff := Eq.mpr (id (Eq.trans (congrFun' (congrArg Eq union_diff_left) T) sdiff_eq_left._simp_1)) (Eq.mp (Eq.trans (congrFun' (congrArg Eq union_diff_left) T) sdiff_eq_left._simp_1) (Disjoint.sup_sdiff_cancel_left hST)); Trans.trans (μ_caratheodory hS (S ∪ T)) (Eq.mpr (id (congrArg (fun _a => μ ((S ∪ T) ∩ S) + μ _a = μ S + μ T) hdiff)) (Eq.mpr (id (congrArg (fun _a => μ _a + μ T = μ S + μ T) (have this := Eq.mpr (id (congrArg (fun _a => _a) (propext inter_eq_right))) subset_union_left; this))) (Eq.refl (μ S + μ T))))⊢ (fun A x => μ A) (⋃ i, A i) ⋯ ≤ ∑' (i : ℕ), (fun A x => μ A) (A i) ⋯X:Type u_1inst✝:MeasurableSpace Xμ:Set X → ℝ≥0∞μ_empty:μ ∅ = 0μ_mono:Monotone μμ_iUnion_le:∀ (A : ℕ → Set X), μ (⋃ i, A i) ≤ ∑' (i : ℕ), μ (A i)μ_caratheodory:∀ {A : Set X}, MeasurableSet A → ∀ (B : Set X), μ B = μ (B ∩ A) + μ (B \ A)A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)h_union:∀ {S T : Set X}, MeasurableSet S → Disjoint S T → μ (S ∪ T) = μ S + μ T := fun {S T} hS hST => have hdiff := Eq.mpr (id (Eq.trans (congrFun' (congrArg Eq union_diff_left) T) sdiff_eq_left._simp_1)) (Eq.mp (Eq.trans (congrFun' (congrArg Eq union_diff_left) T) sdiff_eq_left._simp_1) (Disjoint.sup_sdiff_cancel_left hST)); Trans.trans (μ_caratheodory hS (S ∪ T)) (Eq.mpr (id (congrArg (fun _a => μ ((S ∪ T) ∩ S) + μ _a = μ S + μ T) hdiff)) (Eq.mpr (id (congrArg (fun _a => μ _a + μ T = μ S + μ T) (have this := Eq.mpr (id (congrArg (fun _a => _a) (propext inter_eq_right))) subset_union_left; this))) (Eq.refl (μ S + μ T))))⊢ ∑' (i : ℕ), (fun A x => μ A) (A i) ⋯ ≤ (fun A x => μ A) (⋃ i, A i) ⋯ X:Type u_1inst✝:MeasurableSpace Xμ:Set X → ℝ≥0∞μ_empty:μ ∅ = 0μ_mono:Monotone μμ_iUnion_le:∀ (A : ℕ → Set X), μ (⋃ i, A i) ≤ ∑' (i : ℕ), μ (A i)μ_caratheodory:∀ {A : Set X}, MeasurableSet A → ∀ (B : Set X), μ B = μ (B ∩ A) + μ (B \ A)A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)h_union:∀ {S T : Set X}, MeasurableSet S → Disjoint S T → μ (S ∪ T) = μ S + μ T := fun {S T} hS hST => have hdiff := Eq.mpr (id (Eq.trans (congrFun' (congrArg Eq union_diff_left) T) sdiff_eq_left._simp_1)) (Eq.mp (Eq.trans (congrFun' (congrArg Eq union_diff_left) T) sdiff_eq_left._simp_1) (Disjoint.sup_sdiff_cancel_left hST)); Trans.trans (μ_caratheodory hS (S ∪ T)) (Eq.mpr (id (congrArg (fun _a => μ ((S ∪ T) ∩ S) + μ _a = μ S + μ T) hdiff)) (Eq.mpr (id (congrArg (fun _a => μ _a + μ T = μ S + μ T) (have this := Eq.mpr (id (congrArg (fun _a => _a) (propext inter_eq_right))) subset_union_left; this))) (Eq.refl (μ S + μ T))))⊢ (fun A x => μ A) (⋃ i, A i) ⋯ ≤ ∑' (i : ℕ), (fun A x => μ A) (A i) ⋯ All goals completed! 🐙 X:Type u_1inst✝:MeasurableSpace Xμ:Set X → ℝ≥0∞μ_empty:μ ∅ = 0μ_mono:Monotone μμ_iUnion_le:∀ (A : ℕ → Set X), μ (⋃ i, A i) ≤ ∑' (i : ℕ), μ (A i)μ_caratheodory:∀ {A : Set X}, MeasurableSet A → ∀ (B : Set X), μ B = μ (B ∩ A) + μ (B \ A)A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)h_union:∀ {S T : Set X}, MeasurableSet S → Disjoint S T → μ (S ∪ T) = μ S + μ T := fun {S T} hS hST => have hdiff := Eq.mpr (id (Eq.trans (congrFun' (congrArg Eq union_diff_left) T) sdiff_eq_left._simp_1)) (Eq.mp (Eq.trans (congrFun' (congrArg Eq union_diff_left) T) sdiff_eq_left._simp_1) (Disjoint.sup_sdiff_cancel_left hST)); Trans.trans (μ_caratheodory hS (S ∪ T)) (Eq.mpr (id (congrArg (fun _a => μ ((S ∪ T) ∩ S) + μ _a = μ S + μ T) hdiff)) (Eq.mpr (id (congrArg (fun _a => μ _a + μ T = μ S + μ T) (have this := Eq.mpr (id (congrArg (fun _a => _a) (propext inter_eq_right))) subset_union_left; this))) (Eq.refl (μ S + μ T))))⊢ ∑' (i : ℕ), (fun A x => μ A) (A i) ⋯ ≤ (fun A x => μ A) (⋃ i, A i) ⋯ X:Type u_1inst✝:MeasurableSpace Xμ:Set X → ℝ≥0∞μ_empty:μ ∅ = 0μ_mono:Monotone μμ_iUnion_le:∀ (A : ℕ → Set X), μ (⋃ i, A i) ≤ ∑' (i : ℕ), μ (A i)μ_caratheodory:∀ {A : Set X}, MeasurableSet A → ∀ (B : Set X), μ B = μ (B ∩ A) + μ (B \ A)A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)h_union:∀ {S T : Set X}, MeasurableSet S → Disjoint S T → μ (S ∪ T) = μ S + μ T := fun {S T} hS hST => have hdiff := Eq.mpr (id (Eq.trans (congrFun' (congrArg Eq union_diff_left) T) sdiff_eq_left._simp_1)) (Eq.mp (Eq.trans (congrFun' (congrArg Eq union_diff_left) T) sdiff_eq_left._simp_1) (Disjoint.sup_sdiff_cancel_left hST)); Trans.trans (μ_caratheodory hS (S ∪ T)) (Eq.mpr (id (congrArg (fun _a => μ ((S ∪ T) ∩ S) + μ _a = μ S + μ T) hdiff)) (Eq.mpr (id (congrArg (fun _a => μ _a + μ T = μ S + μ T) (have this := Eq.mpr (id (congrArg (fun _a => _a) (propext inter_eq_right))) subset_union_left; this))) (Eq.refl (μ S + μ T))))⊢ ⨆ i, ∑ a ∈ Finset.range (i + 1), (fun A x => μ A) (A a) ⋯ ≤ (fun A x => μ A) (⋃ i, A i) ⋯ X:Type u_1inst✝:MeasurableSpace Xμ:Set X → ℝ≥0∞μ_empty:μ ∅ = 0μ_mono:Monotone μμ_iUnion_le:∀ (A : ℕ → Set X), μ (⋃ i, A i) ≤ ∑' (i : ℕ), μ (A i)μ_caratheodory:∀ {A : Set X}, MeasurableSet A → ∀ (B : Set X), μ B = μ (B ∩ A) + μ (B \ A)A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)h_union:∀ {S T : Set X}, MeasurableSet S → Disjoint S T → μ (S ∪ T) = μ S + μ T := fun {S T} hS hST => have hdiff := Eq.mpr (id (Eq.trans (congrFun' (congrArg Eq union_diff_left) T) sdiff_eq_left._simp_1)) (Eq.mp (Eq.trans (congrFun' (congrArg Eq union_diff_left) T) sdiff_eq_left._simp_1) (Disjoint.sup_sdiff_cancel_left hST)); Trans.trans (μ_caratheodory hS (S ∪ T)) (Eq.mpr (id (congrArg (fun _a => μ ((S ∪ T) ∩ S) + μ _a = μ S + μ T) hdiff)) (Eq.mpr (id (congrArg (fun _a => μ _a + μ T = μ S + μ T) (have this := Eq.mpr (id (congrArg (fun _a => _a) (propext inter_eq_right))) subset_union_left; this))) (Eq.refl (μ S + μ T))))n:ℕ⊢ ∑ a ∈ Finset.range (n + 1), (fun A x => μ A) (A a) ⋯ ≤ (fun A x => μ A) (⋃ i, A i) ⋯ have hacc : μ (accumulate A n) = ∑ i ∈ Finset.range (n + 1), μ (A i) := X:Type u_1inst✝:MeasurableSpace Xμ:Set X → ℝ≥0∞μ_empty:μ ∅ = 0μ_mono:Monotone μμ_iUnion_le:∀ (A : ℕ → Set X), μ (⋃ i, A i) ≤ ∑' (i : ℕ), μ (A i)μ_caratheodory:∀ {A : Set X}, MeasurableSet A → ∀ (B : Set X), μ B = μ (B ∩ A) + μ (B \ A)⊢ Measure X induction n with X:Type u_1inst✝:MeasurableSpace Xμ:Set X → ℝ≥0∞μ_empty:μ ∅ = 0μ_mono:Monotone μμ_iUnion_le:∀ (A : ℕ → Set X), μ (⋃ i, A i) ≤ ∑' (i : ℕ), μ (A i)μ_caratheodory:∀ {A : Set X}, MeasurableSet A → ∀ (B : Set X), μ B = μ (B ∩ A) + μ (B \ A)A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)h_union:∀ {S T : Set X}, MeasurableSet S → Disjoint S T → μ (S ∪ T) = μ S + μ T := fun {S T} hS hST => have hdiff := Eq.mpr (id (Eq.trans (congrFun' (congrArg Eq union_diff_left) T) sdiff_eq_left._simp_1)) (Eq.mp (Eq.trans (congrFun' (congrArg Eq union_diff_left) T) sdiff_eq_left._simp_1) (Disjoint.sup_sdiff_cancel_left hST)); Trans.trans (μ_caratheodory hS (S ∪ T)) (Eq.mpr (id (congrArg (fun _a => μ ((S ∪ T) ∩ S) + μ _a = μ S + μ T) hdiff)) (Eq.mpr (id (congrArg (fun _a => μ _a + μ T = μ S + μ T) (have this := Eq.mpr (id (congrArg (fun _a => _a) (propext inter_eq_right))) subset_union_left; this))) (Eq.refl (μ S + μ T))))⊢ μ (accumulate A 0) = ∑ i ∈ Finset.range (0 + 1), μ (A i) All goals completed! 🐙 X:Type u_1inst✝:MeasurableSpace Xμ:Set X → ℝ≥0∞μ_empty:μ ∅ = 0μ_mono:Monotone μμ_iUnion_le:∀ (A : ℕ → Set X), μ (⋃ i, A i) ≤ ∑' (i : ℕ), μ (A i)μ_caratheodory:∀ {A : Set X}, MeasurableSet A → ∀ (B : Set X), μ B = μ (B ∩ A) + μ (B \ A)A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)h_union:∀ {S T : Set X}, MeasurableSet S → Disjoint S T → μ (S ∪ T) = μ S + μ T := fun {S T} hS hST => have hdiff := Eq.mpr (id (Eq.trans (congrFun' (congrArg Eq union_diff_left) T) sdiff_eq_left._simp_1)) (Eq.mp (Eq.trans (congrFun' (congrArg Eq union_diff_left) T) sdiff_eq_left._simp_1) (Disjoint.sup_sdiff_cancel_left hST)); Trans.trans (μ_caratheodory hS (S ∪ T)) (Eq.mpr (id (congrArg (fun _a => μ ((S ∪ T) ∩ S) + μ _a = μ S + μ T) hdiff)) (Eq.mpr (id (congrArg (fun _a => μ _a + μ T = μ S + μ T) (have this := Eq.mpr (id (congrArg (fun _a => _a) (propext inter_eq_right))) subset_union_left; this))) (Eq.refl (μ S + μ T))))n:ℕih:μ (accumulate A n) = ∑ i ∈ Finset.range (n + 1), μ (A i)⊢ μ (accumulate A (n + 1)) = ∑ i ∈ Finset.range (n + 1 + 1), μ (A i) calc μ (accumulate A (n + 1)) = μ (accumulate A n) + μ (A (n + 1)) := X:Type u_1inst✝:MeasurableSpace Xμ:Set X → ℝ≥0∞μ_empty:μ ∅ = 0μ_mono:Monotone μμ_iUnion_le:∀ (A : ℕ → Set X), μ (⋃ i, A i) ≤ ∑' (i : ℕ), μ (A i)μ_caratheodory:∀ {A : Set X}, MeasurableSet A → ∀ (B : Set X), μ B = μ (B ∩ A) + μ (B \ A)A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)h_union:∀ {S T : Set X}, MeasurableSet S → Disjoint S T → μ (S ∪ T) = μ S + μ T := fun {S T} hS hST => have hdiff := Eq.mpr (id (Eq.trans (congrFun' (congrArg Eq union_diff_left) T) sdiff_eq_left._simp_1)) (Eq.mp (Eq.trans (congrFun' (congrArg Eq union_diff_left) T) sdiff_eq_left._simp_1) (Disjoint.sup_sdiff_cancel_left hST)); Trans.trans (μ_caratheodory hS (S ∪ T)) (Eq.mpr (id (congrArg (fun _a => μ ((S ∪ T) ∩ S) + μ _a = μ S + μ T) hdiff)) (Eq.mpr (id (congrArg (fun _a => μ _a + μ T = μ S + μ T) (have this := Eq.mpr (id (congrArg (fun _a => _a) (propext inter_eq_right))) subset_union_left; this))) (Eq.refl (μ S + μ T))))n:ℕih:μ (accumulate A n) = ∑ i ∈ Finset.range (n + 1), μ (A i)⊢ μ (accumulate A (n + 1)) = μ (accumulate A n) + μ (A (n + 1)) X:Type u_1inst✝:MeasurableSpace Xμ:Set X → ℝ≥0∞μ_empty:μ ∅ = 0μ_mono:Monotone μμ_iUnion_le:∀ (A : ℕ → Set X), μ (⋃ i, A i) ≤ ∑' (i : ℕ), μ (A i)μ_caratheodory:∀ {A : Set X}, MeasurableSet A → ∀ (B : Set X), μ B = μ (B ∩ A) + μ (B \ A)A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)h_union:∀ {S T : Set X}, MeasurableSet S → Disjoint S T → μ (S ∪ T) = μ S + μ T := fun {S T} hS hST => have hdiff := Eq.mpr (id (Eq.trans (congrFun' (congrArg Eq union_diff_left) T) sdiff_eq_left._simp_1)) (Eq.mp (Eq.trans (congrFun' (congrArg Eq union_diff_left) T) sdiff_eq_left._simp_1) (Disjoint.sup_sdiff_cancel_left hST)); Trans.trans (μ_caratheodory hS (S ∪ T)) (Eq.mpr (id (congrArg (fun _a => μ ((S ∪ T) ∩ S) + μ _a = μ S + μ T) hdiff)) (Eq.mpr (id (congrArg (fun _a => μ _a + μ T = μ S + μ T) (have this := Eq.mpr (id (congrArg (fun _a => _a) (propext inter_eq_right))) subset_union_left; this))) (Eq.refl (μ S + μ T))))n:ℕih:μ (accumulate A n) = ∑ i ∈ Finset.range (n + 1), μ (A i)⊢ μ (accumulate A n ∪ A (n + 1)) = μ (accumulate A n) + μ (A (n + 1)) All goals completed! 🐙 _ = ∑ i ∈ Finset.range (n + 1), μ (A i) + μ (A (n + 1)) := X:Type u_1inst✝:MeasurableSpace Xμ:Set X → ℝ≥0∞μ_empty:μ ∅ = 0μ_mono:Monotone μμ_iUnion_le:∀ (A : ℕ → Set X), μ (⋃ i, A i) ≤ ∑' (i : ℕ), μ (A i)μ_caratheodory:∀ {A : Set X}, MeasurableSet A → ∀ (B : Set X), μ B = μ (B ∩ A) + μ (B \ A)A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)h_union:∀ {S T : Set X}, MeasurableSet S → Disjoint S T → μ (S ∪ T) = μ S + μ T := fun {S T} hS hST => have hdiff := Eq.mpr (id (Eq.trans (congrFun' (congrArg Eq union_diff_left) T) sdiff_eq_left._simp_1)) (Eq.mp (Eq.trans (congrFun' (congrArg Eq union_diff_left) T) sdiff_eq_left._simp_1) (Disjoint.sup_sdiff_cancel_left hST)); Trans.trans (μ_caratheodory hS (S ∪ T)) (Eq.mpr (id (congrArg (fun _a => μ ((S ∪ T) ∩ S) + μ _a = μ S + μ T) hdiff)) (Eq.mpr (id (congrArg (fun _a => μ _a + μ T = μ S + μ T) (have this := Eq.mpr (id (congrArg (fun _a => _a) (propext inter_eq_right))) subset_union_left; this))) (Eq.refl (μ S + μ T))))n:ℕih:μ (accumulate A n) = ∑ i ∈ Finset.range (n + 1), μ (A i)⊢ μ (accumulate A n) + μ (A (n + 1)) = ∑ i ∈ Finset.range (n + 1), μ (A i) + μ (A (n + 1)) All goals completed! 🐙 _ = ∑ i ∈ Finset.range (n + 2), μ (A i) := X:Type u_1inst✝:MeasurableSpace Xμ:Set X → ℝ≥0∞μ_empty:μ ∅ = 0μ_mono:Monotone μμ_iUnion_le:∀ (A : ℕ → Set X), μ (⋃ i, A i) ≤ ∑' (i : ℕ), μ (A i)μ_caratheodory:∀ {A : Set X}, MeasurableSet A → ∀ (B : Set X), μ B = μ (B ∩ A) + μ (B \ A)A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)h_union:∀ {S T : Set X}, MeasurableSet S → Disjoint S T → μ (S ∪ T) = μ S + μ T := fun {S T} hS hST => have hdiff := Eq.mpr (id (Eq.trans (congrFun' (congrArg Eq union_diff_left) T) sdiff_eq_left._simp_1)) (Eq.mp (Eq.trans (congrFun' (congrArg Eq union_diff_left) T) sdiff_eq_left._simp_1) (Disjoint.sup_sdiff_cancel_left hST)); Trans.trans (μ_caratheodory hS (S ∪ T)) (Eq.mpr (id (congrArg (fun _a => μ ((S ∪ T) ∩ S) + μ _a = μ S + μ T) hdiff)) (Eq.mpr (id (congrArg (fun _a => μ _a + μ T = μ S + μ T) (have this := Eq.mpr (id (congrArg (fun _a => _a) (propext inter_eq_right))) subset_union_left; this))) (Eq.refl (μ S + μ T))))n:ℕih:μ (accumulate A n) = ∑ i ∈ Finset.range (n + 1), μ (A i)⊢ ∑ i ∈ Finset.range (n + 1), μ (A i) + μ (A (n + 1)) = ∑ i ∈ Finset.range (n + 2), μ (A i) All goals completed! 🐙 calc ∑ i ∈ Finset.range (n + 1), μ (A i) = μ (accumulate A n) := hacc.symm _ ≤ μ (⋃ i, A i) := μ_mono (Set.accumulate_subset_iUnion n)