2.3. カラテオドリの判定条件
定義.
集合 A \subseteq \mathbb{R} が カラテオドリ であるとは、任意の集合 B \subseteq \mathbb{R} に対して
m(B) = m(B \cap A) + m(B \setminus A) が成り立つことをいう。
Lean code
補題.
A_1, A_2 \subseteq \mathbb{R} とする。
A_1 と A_2 が交わらず、A_1 がカラテオドリであると仮定する。
このとき m(A_1 \cup A_2) = m(A_1) + m(A_2) が成り立つ。
Lean code
theorem measure_c_union {A₁ A₂ : Set ℝ} (h : A₁ ∩ A₂ ⊆ ∅) (h₁ : IsCaratheodory A₁) :
measure (A₁ ∪ A₂) = measure A₁ + measure A₂ := A₁:Set ℝA₂:Set ℝh:A₁ ∩ A₂ ⊆ ∅h₁:IsCaratheodory A₁⊢ measure (A₁ ∪ A₂) = measure A₁ + measure A₂
All goals completed! 🐙
補題.
カラテオドリ集合の和集合、補集合、共通部分も再びカラテオドリである。
Lean code
theorem IsCaratheodory.union {A B : Set ℝ} (hA : IsCaratheodory A) (hB : IsCaratheodory B) :
IsCaratheodory (A ∪ B) := A:Set ℝB:Set ℝhA:IsCaratheodory AhB:IsCaratheodory B⊢ IsCaratheodory (A ∪ B)
A:Set ℝB:Set ℝhA:IsCaratheodory AhB:IsCaratheodory BC:Set ℝ⊢ measure C = measure (C ∩ (A ∪ B)) + measure (C \ (A ∪ B))
have eq₁ :=
calc measure C
_ = measure (C ∩ A) + measure (C \ A) := A:Set ℝB:Set ℝhA:IsCaratheodory AhB:IsCaratheodory BC:Set ℝ⊢ measure C = measure (C ∩ A) + measure (C \ A) All goals completed! 🐙
_ = measure (C ∩ A ∩ B) + measure ((C ∩ A) \ B) +
measure ((C \ A) ∩ B) + measure ((C \ A) \ B) := A:Set ℝB:Set ℝhA:IsCaratheodory AhB:IsCaratheodory BC:Set ℝ⊢ measure (C ∩ A) + measure (C \ A) =
measure (C ∩ A ∩ B) + measure ((C ∩ A) \ B) + measure (C \ A ∩ B) + measure ((C \ A) \ B)
All goals completed! 🐙
have eq₂ :=
calc measure (C ∩ (A ∪ B)) + measure (C \ (A ∪ B))
_ = measure (C ∩ (A ∪ B) ∩ A) + measure ((C ∩ (A ∪ B)) \ A) +
measure (C \ (A ∪ B)) := A:Set ℝB:Set ℝhA:IsCaratheodory AhB:IsCaratheodory BC:Set ℝeq₁:measure C = measure (C ∩ A ∩ B) + measure ((C ∩ A) \ B) + measure (C \ A ∩ B) + measure ((C \ A) \ B) :=
Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a => _a = measure (C ∩ A) + measure (C \ A)) (hA C)))
(Eq.refl (measure (C ∩ A) + measure (C \ A)))))
(union._proof_1 hB C)⊢ measure (C ∩ (A ∪ B)) + measure (C \ (A ∪ B)) =
measure (C ∩ (A ∪ B) ∩ A) + measure ((C ∩ (A ∪ B)) \ A) + measure (C \ (A ∪ B))
All goals completed! 🐙
_ = measure (C ∩ A ∩ B) + measure ((C ∩ A) \ B) +
measure ((C ∩ (A ∪ B)) \ A) + measure (C \ (A ∪ B)) := A:Set ℝB:Set ℝhA:IsCaratheodory AhB:IsCaratheodory BC:Set ℝeq₁:measure C = measure (C ∩ A ∩ B) + measure ((C ∩ A) \ B) + measure (C \ A ∩ B) + measure ((C \ A) \ B) :=
Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a => _a = measure (C ∩ A) + measure (C \ A)) (hA C)))
(Eq.refl (measure (C ∩ A) + measure (C \ A)))))
(union._proof_1 hB C)⊢ measure (C ∩ (A ∪ B) ∩ A) + measure ((C ∩ (A ∪ B)) \ A) + measure (C \ (A ∪ B)) =
measure (C ∩ A ∩ B) + measure ((C ∩ A) \ B) + measure ((C ∩ (A ∪ B)) \ A) + measure (C \ (A ∪ B))
have : C ∩ (A ∪ B) ∩ A = C ∩ A := A:Set ℝB:Set ℝhA:IsCaratheodory AhB:IsCaratheodory BC:Set ℝeq₁:measure C = measure (C ∩ A ∩ B) + measure ((C ∩ A) \ B) + measure (C \ A ∩ B) + measure ((C \ A) \ B) :=
Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a => _a = measure (C ∩ A) + measure (C \ A)) (hA C)))
(Eq.refl (measure (C ∩ A) + measure (C \ A)))))
(union._proof_1 hB C)⊢ measure (C ∩ (A ∪ B) ∩ A) + measure ((C ∩ (A ∪ B)) \ A) + measure (C \ (A ∪ B)) =
measure (C ∩ A ∩ B) + measure ((C ∩ A) \ B) + measure ((C ∩ (A ∪ B)) \ A) + measure (C \ (A ∪ B)) All goals completed! 🐙
All goals completed! 🐙
A:Set ℝB:Set ℝhA:IsCaratheodory AhB:IsCaratheodory BC:Set ℝeq₁:measure C = measure (C ∩ A ∩ B) + measure ((C ∩ A) \ B) + measure (C \ A ∩ B) + measure ((C \ A) \ B) :=
Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a => _a = measure (C ∩ A) + measure (C \ A)) (hA C)))
(Eq.refl (measure (C ∩ A) + measure (C \ A)))))
(union._proof_1 hB C)eq₂:measure (C ∩ (A ∪ B)) + measure (C \ (A ∪ B)) =
measure (C ∩ A ∩ B) + measure ((C ∩ A) \ B) + measure ((C ∩ (A ∪ B)) \ A) + measure (C \ (A ∪ B)) :=
Trans.trans
(Trans.trans rfl
(Eq.mpr
(id
(congrArg
(fun _a =>
_a + measure (C \ (A ∪ B)) =
measure (C ∩ (A ∪ B) ∩ A) + measure ((C ∩ (A ∪ B)) \ A) + measure (C \ (A ∪ B)))
(hA (C ∩ (A ∪ B)))))
(Eq.refl (measure (C ∩ (A ∪ B) ∩ A) + measure ((C ∩ (A ∪ B)) \ A) + measure (C \ (A ∪ B))))))
(have this := union._proof_2 C;
union._proof_3 hB C this)⊢ measure (C ∩ A ∩ B) + measure ((C ∩ A) \ B) + measure (C \ A ∩ B) + measure ((C \ A) \ B) =
measure (C ∩ A ∩ B) + measure ((C ∩ A) \ B) + measure ((C ∩ (A ∪ B)) \ A) + measure (C \ (A ∪ B))
have : (C ∩ (A ∪ B)) \ A = C \ A ∩ B := A:Set ℝB:Set ℝhA:IsCaratheodory AhB:IsCaratheodory B⊢ IsCaratheodory (A ∪ B) All goals completed! 🐙
have : (C \ A) \ B = C \ (A ∪ B) := A:Set ℝB:Set ℝhA:IsCaratheodory AhB:IsCaratheodory B⊢ IsCaratheodory (A ∪ B) All goals completed! 🐙
All goals completed! 🐙theorem IsCaratheodory.compl {A : Set ℝ} : IsCaratheodory A → IsCaratheodory Aᶜ := A:Set ℝ⊢ IsCaratheodory A → IsCaratheodory Aᶜ
intro hA A:Set ℝhA:IsCaratheodory AC:Set ℝ⊢ measure C = measure (C ∩ Aᶜ) + measure (C \ Aᶜ)
calc
measure C = measure (C ∩ A) + measure (C \ A) := hA C
_ = measure (C \ Aᶜ) + measure (C ∩ Aᶜ) := A:Set ℝhA:IsCaratheodory AC:Set ℝ⊢ measure (C ∩ A) + measure (C \ A) = measure (C \ Aᶜ) + measure (C ∩ Aᶜ)
All goals completed! 🐙
_ = measure (C ∩ Aᶜ) + measure (C \ Aᶜ) := A:Set ℝhA:IsCaratheodory AC:Set ℝ⊢ measure (C \ Aᶜ) + measure (C ∩ Aᶜ) = measure (C ∩ Aᶜ) + measure (C \ Aᶜ) All goals completed! 🐙theorem IsCaratheodory.inter {A₁ A₂ : Set ℝ} (h₁ : IsCaratheodory A₁) (h₂ : IsCaratheodory A₂) :
IsCaratheodory (A₁ ∩ A₂) := A₁:Set ℝA₂:Set ℝh₁:IsCaratheodory A₁h₂:IsCaratheodory A₂⊢ IsCaratheodory (A₁ ∩ A₂)
A₁:Set ℝA₂:Set ℝh₁:IsCaratheodory A₁h₂:IsCaratheodory A₂⊢ IsCaratheodory (A₁ᶜ ∪ A₂ᶜ)
All goals completed! 🐙
補題.
カラテオドリ集合の可算和も再びカラテオドリである。
Lean code
theorem isCaratheodory_disjointed {A : ℕ → Set ℝ} (h : ∀ i, IsCaratheodory (A i)) (i : ℕ) :
IsCaratheodory (disjointed A i) :=
disjointedRec (fun _ j ht ↦ ht.diff <| h j) (h i)theorem isCaratheodory_iUnion_of_disjoint {A : ℕ → Set ℝ} (h : ∀ i, IsCaratheodory (A i))
(hd : Pairwise (Disjoint on A)) : IsCaratheodory (⋃ i, A i) := A:ℕ → Set ℝh:∀ (i : ℕ), IsCaratheodory (A i)hd:Pairwise (Disjoint on A)⊢ IsCaratheodory (⋃ i, A i)
A:ℕ → Set ℝh:∀ (i : ℕ), IsCaratheodory (A i)hd:Pairwise (Disjoint on A)⊢ ∀ (B : Set ℝ), measure (B ∩ ⋃ i, A i) + measure (B \ ⋃ i, A i) ≤ measure B
A:ℕ → Set ℝh:∀ (i : ℕ), IsCaratheodory (A i)hd:Pairwise (Disjoint on A)B:Set ℝ⊢ measure (B ∩ ⋃ i, A i) + measure (B \ ⋃ i, A i) ≤ measure B
have hp : measure (B ∩ ⋃ i, A i) ≤ ⨆ n, measure (B ∩ ⋃ i < n, A i) := A:ℕ → Set ℝh:∀ (i : ℕ), IsCaratheodory (A i)hd:Pairwise (Disjoint on A)⊢ IsCaratheodory (⋃ i, A i)
A:ℕ → Set ℝh:∀ (i : ℕ), IsCaratheodory (A i)hd:Pairwise (Disjoint on A)B:Set ℝ⊢ measure (B ∩ ⋃ i, A i) = measure (⋃ n, B ∩ A n)A:ℕ → Set ℝh:∀ (i : ℕ), IsCaratheodory (A i)hd:Pairwise (Disjoint on A)B:Set ℝ⊢ ⨆ n, measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i) = ∑' (n : ℕ), measure (B ∩ A n)
A:ℕ → Set ℝh:∀ (i : ℕ), IsCaratheodory (A i)hd:Pairwise (Disjoint on A)B:Set ℝ⊢ measure (B ∩ ⋃ i, A i) = measure (⋃ n, B ∩ A n) All goals completed! 🐙
A:ℕ → Set ℝh:∀ (i : ℕ), IsCaratheodory (A i)hd:Pairwise (Disjoint on A)B:Set ℝ⊢ ⨆ n, measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i) = ∑' (n : ℕ), measure (B ∩ A n) A:ℕ → Set ℝh:∀ (i : ℕ), IsCaratheodory (A i)hd:Pairwise (Disjoint on A)B:Set ℝ⊢ ⨆ n, measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i) = ⨆ i, ∑ n ∈ Finset.range i, measure (B ∩ A n)
All goals completed! 🐙
grw [hpA:ℕ → Set ℝh:∀ (i : ℕ), IsCaratheodory (A i)hd:Pairwise (Disjoint on A)B:Set ℝhp:measure (B ∩ ⋃ i, A i) ≤ ⨆ n, measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i) :=
Eq.mpr
(eq_of_heq
((fun α self a a' e'_3 a_1 a'_1 e'_4 =>
Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_3 ≍ x → (a ≤ a_1) ≍ (a' ≤ a'_1)) e'_3
(fun h =>
Eq.ndrec (motive := fun a' => ∀ (e_3 : a = a'), e_3 ≍ Eq.refl a → (a ≤ a_1) ≍ (a' ≤ a'_1))
(fun e_3 h =>
Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_4 ≍ x → (a ≤ a_1) ≍ (a ≤ a'_1)) e'_4
(fun h =>
Eq.ndrec (motive := fun a' => ∀ (e_4 : a_1 = a'), e_4 ≍ Eq.refl a_1 → (a ≤ a_1) ≍ (a ≤ a'))
(fun e_4 h => HEq.refl (a ≤ a_1)) (Eq.symm h) e'_4)
(Eq.refl a'_1) (HEq.refl e'_4))
(Eq.symm h) e'_3)
(Eq.refl a') (HEq.refl e'_3))
ℝ≥0∞ instPartialOrder.toLE (measure (B ∩ ⋃ i, A i)) (measure (⋃ n, B ∩ A n))
(of_eq_true
(Eq.trans (congrFun' (congrArg Eq (congrArg measure (inter_iUnion B A))) (measure (⋃ i, B ∩ A i)))
(eq_self (measure (⋃ i, B ∩ A i)))))
(⨆ n, measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i)) (∑' (n : ℕ), measure (B ∩ A n))
(Eq.mpr (id (congrArg (Eq (⨆ n, measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i))) ENNReal.tsum_eq_iSup_nat))
(iSup_congr fun n => Eq.symm (isCaratheodory_sum h hd)))))
(measure_iUnion_le fun i => B ∩ A i)⊢ (⨆ n, measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i)) + measure (B \ ⋃ i, A i) ≤ measure B
A:ℕ → Set ℝh:∀ (i : ℕ), IsCaratheodory (A i)hd:Pairwise (Disjoint on A)B:Set ℝhp:measure (B ∩ ⋃ i, A i) ≤ ⨆ n, measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i) :=
Eq.mpr
(eq_of_heq
((fun α self a a' e'_3 a_1 a'_1 e'_4 =>
Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_3 ≍ x → (a ≤ a_1) ≍ (a' ≤ a'_1)) e'_3
(fun h =>
Eq.ndrec (motive := fun a' => ∀ (e_3 : a = a'), e_3 ≍ Eq.refl a → (a ≤ a_1) ≍ (a' ≤ a'_1))
(fun e_3 h =>
Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_4 ≍ x → (a ≤ a_1) ≍ (a ≤ a'_1)) e'_4
(fun h =>
Eq.ndrec (motive := fun a' => ∀ (e_4 : a_1 = a'), e_4 ≍ Eq.refl a_1 → (a ≤ a_1) ≍ (a ≤ a'))
(fun e_4 h => HEq.refl (a ≤ a_1)) (Eq.symm h) e'_4)
(Eq.refl a'_1) (HEq.refl e'_4))
(Eq.symm h) e'_3)
(Eq.refl a') (HEq.refl e'_3))
ℝ≥0∞ instPartialOrder.toLE (measure (B ∩ ⋃ i, A i)) (measure (⋃ n, B ∩ A n))
(of_eq_true
(Eq.trans (congrFun' (congrArg Eq (congrArg measure (inter_iUnion B A))) (measure (⋃ i, B ∩ A i)))
(eq_self (measure (⋃ i, B ∩ A i)))))
(⨆ n, measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i)) (∑' (n : ℕ), measure (B ∩ A n))
(Eq.mpr (id (congrArg (Eq (⨆ n, measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i))) ENNReal.tsum_eq_iSup_nat))
(iSup_congr fun n => Eq.symm (isCaratheodory_sum h hd)))))
(measure_iUnion_le fun i => B ∩ A i)⊢ ⨆ i, measure (B ∩ ⋃ i_1, ⋃ (_ : i_1 < i), A i_1) + measure (B \ ⋃ i, A i) ≤ measure B
A:ℕ → Set ℝh:∀ (i : ℕ), IsCaratheodory (A i)hd:Pairwise (Disjoint on A)B:Set ℝhp:measure (B ∩ ⋃ i, A i) ≤ ⨆ n, measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i) :=
Eq.mpr
(eq_of_heq
((fun α self a a' e'_3 a_1 a'_1 e'_4 =>
Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_3 ≍ x → (a ≤ a_1) ≍ (a' ≤ a'_1)) e'_3
(fun h =>
Eq.ndrec (motive := fun a' => ∀ (e_3 : a = a'), e_3 ≍ Eq.refl a → (a ≤ a_1) ≍ (a' ≤ a'_1))
(fun e_3 h =>
Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_4 ≍ x → (a ≤ a_1) ≍ (a ≤ a'_1)) e'_4
(fun h =>
Eq.ndrec (motive := fun a' => ∀ (e_4 : a_1 = a'), e_4 ≍ Eq.refl a_1 → (a ≤ a_1) ≍ (a ≤ a'))
(fun e_4 h => HEq.refl (a ≤ a_1)) (Eq.symm h) e'_4)
(Eq.refl a'_1) (HEq.refl e'_4))
(Eq.symm h) e'_3)
(Eq.refl a') (HEq.refl e'_3))
ℝ≥0∞ instPartialOrder.toLE (measure (B ∩ ⋃ i, A i)) (measure (⋃ n, B ∩ A n))
(of_eq_true
(Eq.trans (congrFun' (congrArg Eq (congrArg measure (inter_iUnion B A))) (measure (⋃ i, B ∩ A i)))
(eq_self (measure (⋃ i, B ∩ A i)))))
(⨆ n, measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i)) (∑' (n : ℕ), measure (B ∩ A n))
(Eq.mpr (id (congrArg (Eq (⨆ n, measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i))) ENNReal.tsum_eq_iSup_nat))
(iSup_congr fun n => Eq.symm (isCaratheodory_sum h hd)))))
(measure_iUnion_le fun i => B ∩ A i)n:ℕ⊢ measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i) + measure (B \ ⋃ i, A i) ≤ measure B
calc
measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i) + measure (B \ ⋃ i, A i)
_ ≤ measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i) + measure (B \ ⋃ i, ⋃ (_ : i < n), A i) := A:ℕ → Set ℝh:∀ (i : ℕ), IsCaratheodory (A i)hd:Pairwise (Disjoint on A)B:Set ℝhp:measure (B ∩ ⋃ i, A i) ≤ ⨆ n, measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i) :=
Eq.mpr
(eq_of_heq
((fun α self a a' e'_3 a_1 a'_1 e'_4 =>
Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_3 ≍ x → (a ≤ a_1) ≍ (a' ≤ a'_1)) e'_3
(fun h =>
Eq.ndrec (motive := fun a' => ∀ (e_3 : a = a'), e_3 ≍ Eq.refl a → (a ≤ a_1) ≍ (a' ≤ a'_1))
(fun e_3 h =>
Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_4 ≍ x → (a ≤ a_1) ≍ (a ≤ a'_1)) e'_4
(fun h =>
Eq.ndrec (motive := fun a' => ∀ (e_4 : a_1 = a'), e_4 ≍ Eq.refl a_1 → (a ≤ a_1) ≍ (a ≤ a'))
(fun e_4 h => HEq.refl (a ≤ a_1)) (Eq.symm h) e'_4)
(Eq.refl a'_1) (HEq.refl e'_4))
(Eq.symm h) e'_3)
(Eq.refl a') (HEq.refl e'_3))
ℝ≥0∞ instPartialOrder.toLE (measure (B ∩ ⋃ i, A i)) (measure (⋃ n, B ∩ A n))
(of_eq_true
(Eq.trans (congrFun' (congrArg Eq (congrArg measure (inter_iUnion B A))) (measure (⋃ i, B ∩ A i)))
(eq_self (measure (⋃ i, B ∩ A i)))))
(⨆ n, measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i)) (∑' (n : ℕ), measure (B ∩ A n))
(Eq.mpr (id (congrArg (Eq (⨆ n, measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i))) ENNReal.tsum_eq_iSup_nat))
(iSup_congr fun n => Eq.symm (isCaratheodory_sum h hd)))))
(measure_iUnion_le fun i => B ∩ A i)n:ℕ⊢ measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i) + measure (B \ ⋃ i, A i) ≤
measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i) + measure (B \ ⋃ i, ⋃ (_ : i < n), A i)
A:ℕ → Set ℝh:∀ (i : ℕ), IsCaratheodory (A i)hd:Pairwise (Disjoint on A)B:Set ℝhp:measure (B ∩ ⋃ i, A i) ≤ ⨆ n, measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i) :=
Eq.mpr
(eq_of_heq
((fun α self a a' e'_3 a_1 a'_1 e'_4 =>
Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_3 ≍ x → (a ≤ a_1) ≍ (a' ≤ a'_1)) e'_3
(fun h =>
Eq.ndrec (motive := fun a' => ∀ (e_3 : a = a'), e_3 ≍ Eq.refl a → (a ≤ a_1) ≍ (a' ≤ a'_1))
(fun e_3 h =>
Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_4 ≍ x → (a ≤ a_1) ≍ (a ≤ a'_1)) e'_4
(fun h =>
Eq.ndrec (motive := fun a' => ∀ (e_4 : a_1 = a'), e_4 ≍ Eq.refl a_1 → (a ≤ a_1) ≍ (a ≤ a'))
(fun e_4 h => HEq.refl (a ≤ a_1)) (Eq.symm h) e'_4)
(Eq.refl a'_1) (HEq.refl e'_4))
(Eq.symm h) e'_3)
(Eq.refl a') (HEq.refl e'_3))
ℝ≥0∞ instPartialOrder.toLE (measure (B ∩ ⋃ i, A i)) (measure (⋃ n, B ∩ A n))
(of_eq_true
(Eq.trans (congrFun' (congrArg Eq (congrArg measure (inter_iUnion B A))) (measure (⋃ i, B ∩ A i)))
(eq_self (measure (⋃ i, B ∩ A i)))))
(⨆ n, measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i)) (∑' (n : ℕ), measure (B ∩ A n))
(Eq.mpr (id (congrArg (Eq (⨆ n, measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i))) ENNReal.tsum_eq_iSup_nat))
(iSup_congr fun n => Eq.symm (isCaratheodory_sum h hd)))))
(measure_iUnion_le fun i => B ∩ A i)n:ℕ⊢ measure (B \ ⋃ i, A i) ≤ measure (B \ ⋃ i, ⋃ (_ : i < n), A i)
A:ℕ → Set ℝh:∀ (i : ℕ), IsCaratheodory (A i)hd:Pairwise (Disjoint on A)B:Set ℝhp:measure (B ∩ ⋃ i, A i) ≤ ⨆ n, measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i) :=
Eq.mpr
(eq_of_heq
((fun α self a a' e'_3 a_1 a'_1 e'_4 =>
Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_3 ≍ x → (a ≤ a_1) ≍ (a' ≤ a'_1)) e'_3
(fun h =>
Eq.ndrec (motive := fun a' => ∀ (e_3 : a = a'), e_3 ≍ Eq.refl a → (a ≤ a_1) ≍ (a' ≤ a'_1))
(fun e_3 h =>
Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_4 ≍ x → (a ≤ a_1) ≍ (a ≤ a'_1)) e'_4
(fun h =>
Eq.ndrec (motive := fun a' => ∀ (e_4 : a_1 = a'), e_4 ≍ Eq.refl a_1 → (a ≤ a_1) ≍ (a ≤ a'))
(fun e_4 h => HEq.refl (a ≤ a_1)) (Eq.symm h) e'_4)
(Eq.refl a'_1) (HEq.refl e'_4))
(Eq.symm h) e'_3)
(Eq.refl a') (HEq.refl e'_3))
ℝ≥0∞ instPartialOrder.toLE (measure (B ∩ ⋃ i, A i)) (measure (⋃ n, B ∩ A n))
(of_eq_true
(Eq.trans (congrFun' (congrArg Eq (congrArg measure (inter_iUnion B A))) (measure (⋃ i, B ∩ A i)))
(eq_self (measure (⋃ i, B ∩ A i)))))
(⨆ n, measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i)) (∑' (n : ℕ), measure (B ∩ A n))
(Eq.mpr (id (congrArg (Eq (⨆ n, measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i))) ENNReal.tsum_eq_iSup_nat))
(iSup_congr fun n => Eq.symm (isCaratheodory_sum h hd)))))
(measure_iUnion_le fun i => B ∩ A i)n:ℕ⊢ ⋃ i, ⋃ (_ : i < n), A i ⊆ ⋃ i, A i
All goals completed! 🐙
_ = measure B := A:ℕ → Set ℝh:∀ (i : ℕ), IsCaratheodory (A i)hd:Pairwise (Disjoint on A)B:Set ℝhp:measure (B ∩ ⋃ i, A i) ≤ ⨆ n, measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i) :=
Eq.mpr
(eq_of_heq
((fun α self a a' e'_3 a_1 a'_1 e'_4 =>
Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_3 ≍ x → (a ≤ a_1) ≍ (a' ≤ a'_1)) e'_3
(fun h =>
Eq.ndrec (motive := fun a' => ∀ (e_3 : a = a'), e_3 ≍ Eq.refl a → (a ≤ a_1) ≍ (a' ≤ a'_1))
(fun e_3 h =>
Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_4 ≍ x → (a ≤ a_1) ≍ (a ≤ a'_1)) e'_4
(fun h =>
Eq.ndrec (motive := fun a' => ∀ (e_4 : a_1 = a'), e_4 ≍ Eq.refl a_1 → (a ≤ a_1) ≍ (a ≤ a'))
(fun e_4 h => HEq.refl (a ≤ a_1)) (Eq.symm h) e'_4)
(Eq.refl a'_1) (HEq.refl e'_4))
(Eq.symm h) e'_3)
(Eq.refl a') (HEq.refl e'_3))
ℝ≥0∞ instPartialOrder.toLE (measure (B ∩ ⋃ i, A i)) (measure (⋃ n, B ∩ A n))
(of_eq_true
(Eq.trans (congrFun' (congrArg Eq (congrArg measure (inter_iUnion B A))) (measure (⋃ i, B ∩ A i)))
(eq_self (measure (⋃ i, B ∩ A i)))))
(⨆ n, measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i)) (∑' (n : ℕ), measure (B ∩ A n))
(Eq.mpr (id (congrArg (Eq (⨆ n, measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i))) ENNReal.tsum_eq_iSup_nat))
(iSup_congr fun n => Eq.symm (isCaratheodory_sum h hd)))))
(measure_iUnion_le fun i => B ∩ A i)n:ℕ⊢ measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i) + measure (B \ ⋃ i, ⋃ (_ : i < n), A i) = measure B
have h : IsCaratheodory (⋃ i, ⋃ (_ : i < n), A i) := A:ℕ → Set ℝh:∀ (i : ℕ), IsCaratheodory (A i)hd:Pairwise (Disjoint on A)B:Set ℝhp:measure (B ∩ ⋃ i, A i) ≤ ⨆ n, measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i) :=
Eq.mpr
(eq_of_heq
((fun α self a a' e'_3 a_1 a'_1 e'_4 =>
Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_3 ≍ x → (a ≤ a_1) ≍ (a' ≤ a'_1)) e'_3
(fun h =>
Eq.ndrec (motive := fun a' => ∀ (e_3 : a = a'), e_3 ≍ Eq.refl a → (a ≤ a_1) ≍ (a' ≤ a'_1))
(fun e_3 h =>
Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_4 ≍ x → (a ≤ a_1) ≍ (a ≤ a'_1)) e'_4
(fun h =>
Eq.ndrec (motive := fun a' => ∀ (e_4 : a_1 = a'), e_4 ≍ Eq.refl a_1 → (a ≤ a_1) ≍ (a ≤ a'))
(fun e_4 h => HEq.refl (a ≤ a_1)) (Eq.symm h) e'_4)
(Eq.refl a'_1) (HEq.refl e'_4))
(Eq.symm h) e'_3)
(Eq.refl a') (HEq.refl e'_3))
ℝ≥0∞ instPartialOrder.toLE (measure (B ∩ ⋃ i, A i)) (measure (⋃ n, B ∩ A n))
(of_eq_true
(Eq.trans (congrFun' (congrArg Eq (congrArg measure (inter_iUnion B A))) (measure (⋃ i, B ∩ A i)))
(eq_self (measure (⋃ i, B ∩ A i)))))
(⨆ n, measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i)) (∑' (n : ℕ), measure (B ∩ A n))
(Eq.mpr (id (congrArg (Eq (⨆ n, measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i))) ENNReal.tsum_eq_iSup_nat))
(iSup_congr fun n => Eq.symm (isCaratheodory_sum h hd)))))
(measure_iUnion_le fun i => B ∩ A i)n:ℕ⊢ measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i) + measure (B \ ⋃ i, ⋃ (_ : i < n), A i) = measure B
induction n with
A:ℕ → Set ℝh:∀ (i : ℕ), IsCaratheodory (A i)hd:Pairwise (Disjoint on A)B:Set ℝhp:measure (B ∩ ⋃ i, A i) ≤ ⨆ n, measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i) :=
Eq.mpr
(eq_of_heq
((fun α self a a' e'_3 a_1 a'_1 e'_4 =>
Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_3 ≍ x → (a ≤ a_1) ≍ (a' ≤ a'_1)) e'_3
(fun h =>
Eq.ndrec (motive := fun a' => ∀ (e_3 : a = a'), e_3 ≍ Eq.refl a → (a ≤ a_1) ≍ (a' ≤ a'_1))
(fun e_3 h =>
Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_4 ≍ x → (a ≤ a_1) ≍ (a ≤ a'_1)) e'_4
(fun h =>
Eq.ndrec (motive := fun a' => ∀ (e_4 : a_1 = a'), e_4 ≍ Eq.refl a_1 → (a ≤ a_1) ≍ (a ≤ a'))
(fun e_4 h => HEq.refl (a ≤ a_1)) (Eq.symm h) e'_4)
(Eq.refl a'_1) (HEq.refl e'_4))
(Eq.symm h) e'_3)
(Eq.refl a') (HEq.refl e'_3))
ℝ≥0∞ instPartialOrder.toLE (measure (B ∩ ⋃ i, A i)) (measure (⋃ n, B ∩ A n))
(of_eq_true
(Eq.trans (congrFun' (congrArg Eq (congrArg measure (inter_iUnion B A))) (measure (⋃ i, B ∩ A i)))
(eq_self (measure (⋃ i, B ∩ A i)))))
(⨆ n, measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i)) (∑' (n : ℕ), measure (B ∩ A n))
(Eq.mpr (id (congrArg (Eq (⨆ n, measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i))) ENNReal.tsum_eq_iSup_nat))
(iSup_congr fun n => Eq.symm (isCaratheodory_sum h hd)))))
(measure_iUnion_le fun i => B ∩ A i)⊢ IsCaratheodory (⋃ i, ⋃ (_ : i < 0), A i) All goals completed! 🐙
A:ℕ → Set ℝh:∀ (i : ℕ), IsCaratheodory (A i)hd:Pairwise (Disjoint on A)B:Set ℝhp:measure (B ∩ ⋃ i, A i) ≤ ⨆ n, measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i) :=
Eq.mpr
(eq_of_heq
((fun α self a a' e'_3 a_1 a'_1 e'_4 =>
Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_3 ≍ x → (a ≤ a_1) ≍ (a' ≤ a'_1)) e'_3
(fun h =>
Eq.ndrec (motive := fun a' => ∀ (e_3 : a = a'), e_3 ≍ Eq.refl a → (a ≤ a_1) ≍ (a' ≤ a'_1))
(fun e_3 h =>
Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_4 ≍ x → (a ≤ a_1) ≍ (a ≤ a'_1)) e'_4
(fun h =>
Eq.ndrec (motive := fun a' => ∀ (e_4 : a_1 = a'), e_4 ≍ Eq.refl a_1 → (a ≤ a_1) ≍ (a ≤ a'))
(fun e_4 h => HEq.refl (a ≤ a_1)) (Eq.symm h) e'_4)
(Eq.refl a'_1) (HEq.refl e'_4))
(Eq.symm h) e'_3)
(Eq.refl a') (HEq.refl e'_3))
ℝ≥0∞ instPartialOrder.toLE (measure (B ∩ ⋃ i, A i)) (measure (⋃ n, B ∩ A n))
(of_eq_true
(Eq.trans (congrFun' (congrArg Eq (congrArg measure (inter_iUnion B A))) (measure (⋃ i, B ∩ A i)))
(eq_self (measure (⋃ i, B ∩ A i)))))
(⨆ n, measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i)) (∑' (n : ℕ), measure (B ∩ A n))
(Eq.mpr (id (congrArg (Eq (⨆ n, measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i))) ENNReal.tsum_eq_iSup_nat))
(iSup_congr fun n => Eq.symm (isCaratheodory_sum h hd)))))
(measure_iUnion_le fun i => B ∩ A i)n:ℕih:IsCaratheodory (⋃ i, ⋃ (_ : i < n), A i)⊢ IsCaratheodory (⋃ i, ⋃ (_ : i < n + 1), A i)
A:ℕ → Set ℝh:∀ (i : ℕ), IsCaratheodory (A i)hd:Pairwise (Disjoint on A)B:Set ℝhp:measure (B ∩ ⋃ i, A i) ≤ ⨆ n, measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i) :=
Eq.mpr
(eq_of_heq
((fun α self a a' e'_3 a_1 a'_1 e'_4 =>
Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_3 ≍ x → (a ≤ a_1) ≍ (a' ≤ a'_1)) e'_3
(fun h =>
Eq.ndrec (motive := fun a' => ∀ (e_3 : a = a'), e_3 ≍ Eq.refl a → (a ≤ a_1) ≍ (a' ≤ a'_1))
(fun e_3 h =>
Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_4 ≍ x → (a ≤ a_1) ≍ (a ≤ a'_1)) e'_4
(fun h =>
Eq.ndrec (motive := fun a' => ∀ (e_4 : a_1 = a'), e_4 ≍ Eq.refl a_1 → (a ≤ a_1) ≍ (a ≤ a'))
(fun e_4 h => HEq.refl (a ≤ a_1)) (Eq.symm h) e'_4)
(Eq.refl a'_1) (HEq.refl e'_4))
(Eq.symm h) e'_3)
(Eq.refl a') (HEq.refl e'_3))
ℝ≥0∞ instPartialOrder.toLE (measure (B ∩ ⋃ i, A i)) (measure (⋃ n, B ∩ A n))
(of_eq_true
(Eq.trans (congrFun' (congrArg Eq (congrArg measure (inter_iUnion B A))) (measure (⋃ i, B ∩ A i)))
(eq_self (measure (⋃ i, B ∩ A i)))))
(⨆ n, measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i)) (∑' (n : ℕ), measure (B ∩ A n))
(Eq.mpr (id (congrArg (Eq (⨆ n, measure (B ∩ ⋃ i, ⋃ (_ : i < n), A i))) ENNReal.tsum_eq_iSup_nat))
(iSup_congr fun n => Eq.symm (isCaratheodory_sum h hd)))))
(measure_iUnion_le fun i => B ∩ A i)n:ℕih:IsCaratheodory (⋃ i, ⋃ (_ : i < n), A i)⊢ IsCaratheodory ((⋃ k, ⋃ (_ : k < n), A k) ∪ A n)
All goals completed! 🐙
All goals completed! 🐙theorem isCaratheodory_iUnion {A : ℕ → Set ℝ} (h : ∀ i, IsCaratheodory (A i)) :
IsCaratheodory (⋃ i, A i) := A:ℕ → Set ℝh:∀ (i : ℕ), IsCaratheodory (A i)⊢ IsCaratheodory (⋃ i, A i)
A:ℕ → Set ℝh:∀ (i : ℕ), IsCaratheodory (A i)⊢ IsCaratheodory (⋃ i, disjointed A i)
All goals completed! 🐙
定理 (下からの連続性).
A_0, A_1, \dots \subset \mathbb{R} をカラテオドリ集合の単調増大列とする。
このとき
m\left( \bigcup_{n \in \mathbb{N}} A_n \right)
= \sup_{n \in \mathbb{N}} m(A_n).
が成り立つ。
Lean code
theorem measure_c_iUnion_of_monotone {A : ℕ → Set ℝ}
(hA : ∀ i, IsCaratheodory (A i)) (hA_mono : Monotone A) :
measure (⋃ i, A i) = ⨆ i, measure (A i) := A:ℕ → Set ℝhA:∀ (i : ℕ), IsCaratheodory (A i)hA_mono:Monotone A⊢ measure (⋃ i, A i) = ⨆ i, measure (A i)
A:ℕ → Set ℝhA:∀ (i : ℕ), IsCaratheodory (A i)hA_mono:Monotone A⊢ measure (⋃ i, A i) ≤ ⨆ i, measure (A i)
calc
measure (⋃ n, A n) = measure (⋃ n, disjointed A n) := A:ℕ → Set ℝhA:∀ (i : ℕ), IsCaratheodory (A i)hA_mono:Monotone A⊢ measure (⋃ n, A n) = measure (⋃ n, disjointed A n) All goals completed! 🐙
_ ≤ ∑' n, measure (disjointed A n) := measure_iUnion_le _
_ = ⨆ n, ∑ i ∈ Finset.range n, measure (disjointed A i) := ENNReal.tsum_eq_iSup_nat
_ ≤ ⨆ n, measure (A n) := iSup_mono fun n => A:ℕ → Set ℝhA:∀ (i : ℕ), IsCaratheodory (A i)hA_mono:Monotone An:ℕ⊢ ∑ i ∈ Finset.range n, measure (disjointed A i) ≤ measure (A n)
calc
∑ i ∈ Finset.range n, measure (disjointed A i) =
measure (⋃ i ∈ Finset.range n, disjointed A i) := A:ℕ → Set ℝhA:∀ (i : ℕ), IsCaratheodory (A i)hA_mono:Monotone An:ℕ⊢ ∑ i ∈ Finset.range n, measure (disjointed A i) = measure (⋃ i ∈ Finset.range n, disjointed A i)
A:ℕ → Set ℝhA:∀ (i : ℕ), IsCaratheodory (A i)hA_mono:Monotone An:ℕ⊢ measure (⋃ i, ⋃ (_ : i < n), disjointed A i) = measure (⋃ i ∈ Finset.range n, disjointed A i)
A:ℕ → Set ℝhA:∀ (i : ℕ), IsCaratheodory (A i)hA_mono:Monotone An:ℕ⊢ measure (⋃ i, ⋃ (_ : i < n), disjointed A i) ≤ measure (⋃ i ∈ Finset.range n, disjointed A i)A:ℕ → Set ℝhA:∀ (i : ℕ), IsCaratheodory (A i)hA_mono:Monotone An:ℕ⊢ measure (⋃ i ∈ Finset.range n, disjointed A i) ≤ measure (⋃ i, ⋃ (_ : i < n), disjointed A i) A:ℕ → Set ℝhA:∀ (i : ℕ), IsCaratheodory (A i)hA_mono:Monotone An:ℕ⊢ measure (⋃ i, ⋃ (_ : i < n), disjointed A i) ≤ measure (⋃ i ∈ Finset.range n, disjointed A i)A:ℕ → Set ℝhA:∀ (i : ℕ), IsCaratheodory (A i)hA_mono:Monotone An:ℕ⊢ measure (⋃ i ∈ Finset.range n, disjointed A i) ≤ measure (⋃ i, ⋃ (_ : i < n), disjointed A i) A:ℕ → Set ℝhA:∀ (i : ℕ), IsCaratheodory (A i)hA_mono:Monotone An:ℕ⊢ ⋃ i ∈ Finset.range n, disjointed A i ⊆ ⋃ i, ⋃ (_ : i < n), disjointed A i A:ℕ → Set ℝhA:∀ (i : ℕ), IsCaratheodory (A i)hA_mono:Monotone An:ℕ⊢ ⋃ i, ⋃ (_ : i < n), disjointed A i ⊆ ⋃ i ∈ Finset.range n, disjointed A iA:ℕ → Set ℝhA:∀ (i : ℕ), IsCaratheodory (A i)hA_mono:Monotone An:ℕ⊢ ⋃ i ∈ Finset.range n, disjointed A i ⊆ ⋃ i, ⋃ (_ : i < n), disjointed A i All goals completed! 🐙
_ ≤ measure (⋃ i ∈ Finset.range n, A i) :=
measure_mono (iUnion₂_mono fun n _hn => disjointed_subset _ _)
_ ≤ measure (A n) := measure_mono <| iUnion₂_subset <| A:ℕ → Set ℝhA:∀ (i : ℕ), IsCaratheodory (A i)hA_mono:Monotone An:ℕ⊢ ∀ i ∈ Finset.range n, A i ⊆ A n
intro i A:ℕ → Set ℝhA:∀ (i : ℕ), IsCaratheodory (A i)hA_mono:Monotone An:ℕi:ℕhi:i ∈ Finset.range n⊢ A i ⊆ A n
A:ℕ → Set ℝhA:∀ (i : ℕ), IsCaratheodory (A i)hA_mono:Monotone An:ℕi:ℕhi:i ∈ Finset.range n⊢ i ≤ n
All goals completed! 🐙
定理 (可算加法性).
A_0, A_1, \dots \subset \mathbb{R} を互いに交わらないカラテオドリ集合の列とする。
このとき
m\left( \bigcup_{n \in \mathbb{N}} A_n \right)
= \sum_{n \in \mathbb{N}} m(A_n).
が成り立つ。
Lean code
theorem measure_c_iUnion (A : ℕ → Set ℝ)
(hA : ∀ n, IsCaratheodory (A n)) (hdA : Pairwise (Disjoint on A)) :
measure (⋃ n, A n) = ∑' n, measure (A n) :=
calc
measure (⋃ n, A n) = measure (⋃ n, accumulate A n) := A:ℕ → Set ℝhA:∀ (n : ℕ), IsCaratheodory (A n)hdA:Pairwise (Disjoint on A)⊢ measure (⋃ n, A n) = measure (⋃ n, accumulate A n)
All goals completed! 🐙
_ = ⨆ n, measure (accumulate A n) :=
measure_c_iUnion_of_monotone (isCaratheodory_accumulate hA) monotone_accumulate
_ = ⨆ n, ∑ i ∈ Finset.range (n + 1), measure (A i) :=
iSup_congr (measure_c_accumulate hA hdA)
_ = ∑' n, measure (A n) :=
(ENNReal.tsum_eq_iSup_nat' (Filter.tendsto_add_atTop_nat 1)).symm