2.5. 可測上位集合による近似
定理.
任意の集合
A \subseteq \mathbb{R} に対して
m(A) =
\inf_{\substack{B \subseteq \mathbb{R} \\ \text{$B$ is measurable},\, A \subseteq B}} m(B).
が成り立つ。
Lean code
theorem measure_eq_iInf (A : Set ℝ) :
measure A = ⨅ B, ⨅ (_ : A ⊆ B), ⨅ (_ : MeasurableSet B), measure B := A:Set ℝ⊢ measure A = ⨅ B, ⨅ (_ : A ⊆ B), ⨅ (_ : MeasurableSet B), measure B
A:Set ℝ⊢ ⨅ B, ⨅ (_ : A ⊆ B), ⨅ (_ : MeasurableSet B), measure B ≤ measure A
A:Set ℝa:ℕ → ℝb:ℕ → ℝhab:A ⊆ ⋃ i, Ioo (a i) (b i)ε:NNRealε0:0 < εh:∑' (i : ℕ), ENNReal.ofReal (b i - a i) < ∞⊢ ⨅ B, ⨅ (_ : A ⊆ B), ⨅ (_ : MeasurableSet B), measure B ≤ ∑' (i : ℕ), ENNReal.ofReal (b i - a i) + ↑ε
A:Set ℝa:ℕ → ℝb:ℕ → ℝhab:A ⊆ ⋃ i, Ioo (a i) (b i)ε:NNRealε0:0 < εh:∑' (i : ℕ), ENNReal.ofReal (b i - a i) < ∞ε':ℕ → NNRealε'0:∀ (i : ℕ), 0 < ε' ihε:∑' (i : ℕ), ↑(ε' i) < ↑ε⊢ ⨅ B, ⨅ (_ : A ⊆ B), ⨅ (_ : MeasurableSet B), measure B ≤ ∑' (i : ℕ), ENNReal.ofReal (b i - a i) + ↑ε
grw [← hεA:Set ℝa:ℕ → ℝb:ℕ → ℝhab:A ⊆ ⋃ i, Ioo (a i) (b i)ε:NNRealε0:0 < εh:∑' (i : ℕ), ENNReal.ofReal (b i - a i) < ∞ε':ℕ → NNRealε'0:∀ (i : ℕ), 0 < ε' ihε:∑' (i : ℕ), ↑(ε' i) < ↑ε⊢ ⨅ B, ⨅ (_ : A ⊆ B), ⨅ (_ : MeasurableSet B), measure B ≤ ∑' (i : ℕ), ENNReal.ofReal (b i - a i) + ∑' (i : ℕ), ↑(ε' i)
A:Set ℝa:ℕ → ℝb:ℕ → ℝhab:A ⊆ ⋃ i, Ioo (a i) (b i)ε:NNRealε0:0 < εh:∑' (i : ℕ), ENNReal.ofReal (b i - a i) < ∞ε':ℕ → NNRealε'0:∀ (i : ℕ), 0 < ε' ihε:∑' (i : ℕ), ↑(ε' i) < ↑ε⊢ ⨅ B, ⨅ (_ : A ⊆ B), ⨅ (_ : MeasurableSet B), measure B ≤ ∑' (a_1 : ℕ), (ENNReal.ofReal (b a_1 - a a_1) + ↑(ε' a_1))
choose B hB using
show ∀ i, ∃ s, Ioo (a i) (b i) ⊆ s ∧ MeasurableSet s ∧
measure s ≤ .ofReal (b i - a i) + .ofReal (ε' i) A:Set ℝ⊢ measure A = ⨅ B, ⨅ (_ : A ⊆ B), ⨅ (_ : MeasurableSet B), measure B
A:Set ℝa:ℕ → ℝb:ℕ → ℝhab:A ⊆ ⋃ i, Ioo (a i) (b i)ε:NNRealε0:0 < εh:∑' (i : ℕ), ENNReal.ofReal (b i - a i) < ∞ε':ℕ → NNRealε'0:∀ (i : ℕ), 0 < ε' ihε:∑' (i : ℕ), ↑(ε' i) < ↑εi:ℕ⊢ ∃ s, Ioo (a i) (b i) ⊆ s ∧ MeasurableSet s ∧ measure s ≤ ENNReal.ofReal (b i - a i) + ENNReal.ofReal ↑(ε' i)
A:Set ℝa:ℕ → ℝb:ℕ → ℝhab:A ⊆ ⋃ i, Ioo (a i) (b i)ε:NNRealε0:0 < εh:∑' (i : ℕ), ENNReal.ofReal (b i - a i) < ∞ε':ℕ → NNRealε'0:∀ (i : ℕ), 0 < ε' ihε:∑' (i : ℕ), ↑(ε' i) < ↑εi:ℕhl:ENNReal.ofReal (b i - a i) < ENNReal.ofReal (b i - a i) + ↑(ε' i) := lt_add_right (LT.lt.ne (LE.le.trans_lt (ENNReal.le_tsum i) h)) (LT.lt.ne' (coe_pos.mpr (ε'0 i)))⊢ ∃ s, Ioo (a i) (b i) ⊆ s ∧ MeasurableSet s ∧ measure s ≤ ENNReal.ofReal (b i - a i) + ENNReal.ofReal ↑(ε' i)
have habε : Ioo (a i) (b i) ⊆ Ioo (a i) (b i + ε' i) := A:Set ℝ⊢ measure A = ⨅ B, ⨅ (_ : A ⊆ B), ⨅ (_ : MeasurableSet B), measure B
have : (ε' i : ℝ) > 0 := A:Set ℝ⊢ measure A = ⨅ B, ⨅ (_ : A ⊆ B), ⨅ (_ : MeasurableSet B), measure B All goals completed! 🐙
All goals completed! 🐙
A:Set ℝa:ℕ → ℝb:ℕ → ℝhab:A ⊆ ⋃ i, Ioo (a i) (b i)ε:NNRealε0:0 < εh:∑' (i : ℕ), ENNReal.ofReal (b i - a i) < ∞ε':ℕ → NNRealε'0:∀ (i : ℕ), 0 < ε' ihε:∑' (i : ℕ), ↑(ε' i) < ↑εi:ℕhl:ENNReal.ofReal (b i - a i) < ENNReal.ofReal (b i - a i) + ↑(ε' i) := lt_add_right (LT.lt.ne (LE.le.trans_lt (ENNReal.le_tsum i) h)) (LT.lt.ne' (coe_pos.mpr (ε'0 i)))habε:Ioo (a i) (b i) ⊆ Ioo (a i) (b i + ↑(ε' i)) :=
have this := of_eq_true (Eq.trans gt_iff_lt._simp_1 (Eq.trans NNReal.coe_pos._simp_1 (eq_true (ε'0 i))));
measure_eq_iInf._proof_1 a b ε' i this⊢ measure (Ioo (a i) (b i + ↑(ε' i))) ≤ ENNReal.ofReal (b i - a i) + ENNReal.ofReal ↑(ε' i)
calc measure (Ioo (a i) (b i + ε' i))
_ ≤ .ofReal ((b i + ε' i) - a i) := A:Set ℝa:ℕ → ℝb:ℕ → ℝhab:A ⊆ ⋃ i, Ioo (a i) (b i)ε:NNRealε0:0 < εh:∑' (i : ℕ), ENNReal.ofReal (b i - a i) < ∞ε':ℕ → NNRealε'0:∀ (i : ℕ), 0 < ε' ihε:∑' (i : ℕ), ↑(ε' i) < ↑εi:ℕhl:ENNReal.ofReal (b i - a i) < ENNReal.ofReal (b i - a i) + ↑(ε' i) := lt_add_right (LT.lt.ne (LE.le.trans_lt (ENNReal.le_tsum i) h)) (LT.lt.ne' (coe_pos.mpr (ε'0 i)))habε:Ioo (a i) (b i) ⊆ Ioo (a i) (b i + ↑(ε' i)) :=
have this := of_eq_true (Eq.trans gt_iff_lt._simp_1 (Eq.trans NNReal.coe_pos._simp_1 (eq_true (ε'0 i))));
measure_eq_iInf._proof_1 a b ε' i this⊢ measure (Ioo (a i) (b i + ↑(ε' i))) ≤ ENNReal.ofReal (b i + ↑(ε' i) - a i) All goals completed! 🐙
_ ≤ .ofReal (b i - a i + ε' i) := A:Set ℝa:ℕ → ℝb:ℕ → ℝhab:A ⊆ ⋃ i, Ioo (a i) (b i)ε:NNRealε0:0 < εh:∑' (i : ℕ), ENNReal.ofReal (b i - a i) < ∞ε':ℕ → NNRealε'0:∀ (i : ℕ), 0 < ε' ihε:∑' (i : ℕ), ↑(ε' i) < ↑εi:ℕhl:ENNReal.ofReal (b i - a i) < ENNReal.ofReal (b i - a i) + ↑(ε' i) := lt_add_right (LT.lt.ne (LE.le.trans_lt (ENNReal.le_tsum i) h)) (LT.lt.ne' (coe_pos.mpr (ε'0 i)))habε:Ioo (a i) (b i) ⊆ Ioo (a i) (b i + ↑(ε' i)) :=
have this := of_eq_true (Eq.trans gt_iff_lt._simp_1 (Eq.trans NNReal.coe_pos._simp_1 (eq_true (ε'0 i))));
measure_eq_iInf._proof_1 a b ε' i this⊢ ENNReal.ofReal (b i + ↑(ε' i) - a i) ≤ ENNReal.ofReal (b i - a i + ↑(ε' i)) All goals completed! 🐙
_ ≤ .ofReal (b i - a i) + .ofReal (ε' i) := A:Set ℝa:ℕ → ℝb:ℕ → ℝhab:A ⊆ ⋃ i, Ioo (a i) (b i)ε:NNRealε0:0 < εh:∑' (i : ℕ), ENNReal.ofReal (b i - a i) < ∞ε':ℕ → NNRealε'0:∀ (i : ℕ), 0 < ε' ihε:∑' (i : ℕ), ↑(ε' i) < ↑εi:ℕhl:ENNReal.ofReal (b i - a i) < ENNReal.ofReal (b i - a i) + ↑(ε' i) := lt_add_right (LT.lt.ne (LE.le.trans_lt (ENNReal.le_tsum i) h)) (LT.lt.ne' (coe_pos.mpr (ε'0 i)))habε:Ioo (a i) (b i) ⊆ Ioo (a i) (b i + ↑(ε' i)) :=
have this := of_eq_true (Eq.trans gt_iff_lt._simp_1 (Eq.trans NNReal.coe_pos._simp_1 (eq_true (ε'0 i))));
measure_eq_iInf._proof_1 a b ε' i this⊢ ENNReal.ofReal (b i - a i + ↑(ε' i)) ≤ ENNReal.ofReal (b i - a i) + ENNReal.ofReal ↑(ε' i)
A:Set ℝa:ℕ → ℝb:ℕ → ℝhab:A ⊆ ⋃ i, Ioo (a i) (b i)ε:NNRealε0:0 < εh:∑' (i : ℕ), ENNReal.ofReal (b i - a i) < ∞ε':ℕ → NNRealε'0:∀ (i : ℕ), 0 < ε' ihε:∑' (i : ℕ), ↑(ε' i) < ↑εi:ℕhl:ENNReal.ofReal (b i - a i) < ENNReal.ofReal (b i - a i) + ↑(ε' i) := lt_add_right (LT.lt.ne (LE.le.trans_lt (ENNReal.le_tsum i) h)) (LT.lt.ne' (coe_pos.mpr (ε'0 i)))habε:Ioo (a i) (b i) ⊆ Ioo (a i) (b i + ↑(ε' i)) :=
have this := of_eq_true (Eq.trans gt_iff_lt._simp_1 (Eq.trans NNReal.coe_pos._simp_1 (eq_true (ε'0 i))));
measure_eq_iInf._proof_1 a b ε' i this⊢ ENNReal.ofReal (b i - a i + ↑(ε' i)) ≤ ENNReal.ofReal (b i - a i) + ENNReal.ofReal ↑(ε' i)
All goals completed! 🐙
A:Set ℝa:ℕ → ℝb:ℕ → ℝhab:A ⊆ ⋃ i, Ioo (a i) (b i)ε:NNRealε0:0 < εh:∑' (i : ℕ), ENNReal.ofReal (b i - a i) < ∞ε':ℕ → NNRealε'0:∀ (i : ℕ), 0 < ε' ihε:∑' (i : ℕ), ↑(ε' i) < ↑εB:ℕ → Set ℝhB:∀ (i : ℕ), Ioo (a i) (b i) ⊆ B i ∧ MeasurableSet (B i) ∧ measure (B i) ≤ ENNReal.ofReal (b i - a i) + ↑(ε' i)⊢ ⨅ B, ⨅ (_ : A ⊆ B), ⨅ (_ : MeasurableSet B), measure B ≤ ∑' (a_1 : ℕ), (ENNReal.ofReal (b a_1 - a a_1) + ↑(ε' a_1))
A:Set ℝa:ℕ → ℝb:ℕ → ℝhab:A ⊆ ⋃ i, Ioo (a i) (b i)ε:NNRealε0:0 < εh:∑' (i : ℕ), ENNReal.ofReal (b i - a i) < ∞ε':ℕ → NNRealε'0:∀ (i : ℕ), 0 < ε' ihε:∑' (i : ℕ), ↑(ε' i) < ↑εB:ℕ → Set ℝhB:∀ (i : ℕ), Ioo (a i) (b i) ⊆ B i ∧ MeasurableSet (B i) ∧ measure (B i) ≤ ENNReal.ofReal (b i - a i) + ↑(ε' i)⊢ ⨅ (_ : A ⊆ iUnion B), ⨅ (_ : MeasurableSet (iUnion B)), measure (iUnion B) ≤
∑' (a_1 : ℕ), (ENNReal.ofReal (b a_1 - a a_1) + ↑(ε' a_1))
A:Set ℝa:ℕ → ℝb:ℕ → ℝhab:A ⊆ ⋃ i, Ioo (a i) (b i)ε:NNRealε0:0 < εh:∑' (i : ℕ), ENNReal.ofReal (b i - a i) < ∞ε':ℕ → NNRealε'0:∀ (i : ℕ), 0 < ε' ihε:∑' (i : ℕ), ↑(ε' i) < ↑εB:ℕ → Set ℝhB:∀ (i : ℕ), Ioo (a i) (b i) ⊆ B i ∧ MeasurableSet (B i) ∧ measure (B i) ≤ ENNReal.ofReal (b i - a i) + ↑(ε' i)⊢ ⨅ (_ : MeasurableSet (iUnion B)), measure (iUnion B) ≤ ∑' (a_1 : ℕ), (ENNReal.ofReal (b a_1 - a a_1) + ↑(ε' a_1))
A:Set ℝa:ℕ → ℝb:ℕ → ℝhab:A ⊆ ⋃ i, Ioo (a i) (b i)ε:NNRealε0:0 < εh:∑' (i : ℕ), ENNReal.ofReal (b i - a i) < ∞ε':ℕ → NNRealε'0:∀ (i : ℕ), 0 < ε' ihε:∑' (i : ℕ), ↑(ε' i) < ↑εB:ℕ → Set ℝhB:∀ (i : ℕ), Ioo (a i) (b i) ⊆ B i ∧ MeasurableSet (B i) ∧ measure (B i) ≤ ENNReal.ofReal (b i - a i) + ↑(ε' i)⊢ measure (iUnion B) ≤ ∑' (a_1 : ℕ), (ENNReal.ofReal (b a_1 - a a_1) + ↑(ε' a_1))
All goals completed! 🐙
定理.
任意の集合 A \subseteq \mathbb{R} に対して、
A \subseteq B かつ m(B) = m(A) を満たす可測集合 B \subseteq \mathbb{R} が存在する。
Lean code
theorem exists_measurable_superset_measure_eq (A : Set ℝ) :
∃ B, A ⊆ B ∧ MeasurableSet B ∧ measure B = measure A := A:Set ℝ⊢ ∃ B, A ⊆ B ∧ MeasurableSet B ∧ measure B = measure A
A:Set ℝhA:measure A = ∞⊢ ∃ B, A ⊆ B ∧ MeasurableSet B ∧ measure B = measure AA:Set ℝhA:¬measure A = ∞⊢ ∃ B, A ⊆ B ∧ MeasurableSet B ∧ measure B = measure A
A:Set ℝhA:measure A = ∞⊢ ∃ B, A ⊆ B ∧ MeasurableSet B ∧ measure B = measure A A:Set ℝhA:measure A = ∞⊢ measure univ = measure A
A:Set ℝhA:measure A = ∞⊢ measure univ = ∞
exact le_antisymm le_top (A:Set ℝhA:measure A = ∞⊢ ∞ ≤ measure univ All goals completed! 🐙)
A:Set ℝhA:¬measure A = ∞⊢ ∃ B, A ⊆ B ∧ MeasurableSet B ∧ measure B = measure A have hex :
∀ r, measure A < r → ∃ B, A ⊆ B ∧ MeasurableSet B ∧ measure B < r := A:Set ℝ⊢ ∃ B, A ⊆ B ∧ MeasurableSet B ∧ measure B = measure A
intro r A:Set ℝhA:¬measure A = ∞r:ℝ≥0∞hr:measure A < r⊢ ∃ B, A ⊆ B ∧ MeasurableSet B ∧ measure B < r
have hApprox :
(⨅ B, ⨅ (_ : A ⊆ B), ⨅ (_ : MeasurableSet B), measure B) < r := A:Set ℝ⊢ ∃ B, A ⊆ B ∧ MeasurableSet B ∧ measure B = measure A
All goals completed! 🐙
A:Set ℝhA:¬measure A = ∞r:ℝ≥0∞hr:measure A < rhApprox:⨅ B, ⨅ (_ : A ⊆ B), ⨅ (_ : MeasurableSet B), measure B < r := Eq.mp (congrFun' (congrArg LT.lt (measure_eq_iInf A)) r) hrB:Set ℝhB:⨅ (_ : A ⊆ B), ⨅ (_ : MeasurableSet B), measure B < r⊢ ∃ B, A ⊆ B ∧ MeasurableSet B ∧ measure B < r
A:Set ℝhA:¬measure A = ∞r:ℝ≥0∞hr:measure A < rhApprox:⨅ B, ⨅ (_ : A ⊆ B), ⨅ (_ : MeasurableSet B), measure B < r := Eq.mp (congrFun' (congrArg LT.lt (measure_eq_iInf A)) r) hrB:Set ℝhB✝:⨅ (_ : A ⊆ B), ⨅ (_ : MeasurableSet B), measure B < rhAB:A ⊆ BhB:⨅ (_ : MeasurableSet B), measure B < r⊢ ∃ B, A ⊆ B ∧ MeasurableSet B ∧ measure B < r
A:Set ℝhA:¬measure A = ∞r:ℝ≥0∞hr:measure A < rhApprox:⨅ B, ⨅ (_ : A ⊆ B), ⨅ (_ : MeasurableSet B), measure B < r := Eq.mp (congrFun' (congrArg LT.lt (measure_eq_iInf A)) r) hrB:Set ℝhB✝¹:⨅ (_ : A ⊆ B), ⨅ (_ : MeasurableSet B), measure B < rhAB:A ⊆ BhB✝:⨅ (_ : MeasurableSet B), measure B < rhMeas:MeasurableSet BhB:measure B < r⊢ ∃ B, A ⊆ B ∧ MeasurableSet B ∧ measure B < r
All goals completed! 🐙
have ha : ∃ a : ℕ → ℝ≥0∞, ⨅ i, a i = 0 ∧ ∀ n, a n ≠ 0 := A:Set ℝ⊢ ∃ B, A ⊆ B ∧ MeasurableSet B ∧ measure B = measure A
refine ⟨fun n ↦ 1 / (n + 1 : ℝ≥0∞), le_antisymm ?_ (zero_le _), fun n ↦ A:Set ℝhA:¬measure A = ∞hex:∀ (r : ℝ≥0∞), measure A < r → ∃ B, A ⊆ B ∧ MeasurableSet B ∧ measure B < r :=
fun r hr =>
have hApprox := Eq.mp (congrFun' (congrArg LT.lt (measure_eq_iInf A)) r) hr;
Exists.casesOn (iInf_lt_iff.mp hApprox) fun B hB =>
Exists.casesOn (iInf_lt_iff.mp hB) fun hAB hB =>
Exists.casesOn (iInf_lt_iff.mp hB) fun hMeas hB => Exists.intro B ⟨hAB, ⟨hMeas, hB⟩⟩n:ℕ⊢ (fun n => 1 / (↑n + 1)) n ≠ 0 All goals completed! 🐙⟩
A:Set ℝhA:¬measure A = ∞hex:∀ (r : ℝ≥0∞), measure A < r → ∃ B, A ⊆ B ∧ MeasurableSet B ∧ measure B < r :=
fun r hr =>
have hApprox := Eq.mp (congrFun' (congrArg LT.lt (measure_eq_iInf A)) r) hr;
Exists.casesOn (iInf_lt_iff.mp hApprox) fun B hB =>
Exists.casesOn (iInf_lt_iff.mp hB) fun hAB hB =>
Exists.casesOn (iInf_lt_iff.mp hB) fun hMeas hB => Exists.intro B ⟨hAB, ⟨hMeas, hB⟩⟩⊢ ∀ (ε : NNReal), 0 < ε → 0 < ∞ → ⨅ i, (fun n => 1 / (↑n + 1)) i ≤ 0 + ↑ε
intro ε A:Set ℝhA:¬measure A = ∞hex:∀ (r : ℝ≥0∞), measure A < r → ∃ B, A ⊆ B ∧ MeasurableSet B ∧ measure B < r :=
fun r hr =>
have hApprox := Eq.mp (congrFun' (congrArg LT.lt (measure_eq_iInf A)) r) hr;
Exists.casesOn (iInf_lt_iff.mp hApprox) fun B hB =>
Exists.casesOn (iInf_lt_iff.mp hB) fun hAB hB =>
Exists.casesOn (iInf_lt_iff.mp hB) fun hMeas hB => Exists.intro B ⟨hAB, ⟨hMeas, hB⟩⟩ε:NNRealhε:0 < ε⊢ 0 < ∞ → ⨅ i, (fun n => 1 / (↑n + 1)) i ≤ 0 + ↑ε A:Set ℝhA:¬measure A = ∞hex:∀ (r : ℝ≥0∞), measure A < r → ∃ B, A ⊆ B ∧ MeasurableSet B ∧ measure B < r :=
fun r hr =>
have hApprox := Eq.mp (congrFun' (congrArg LT.lt (measure_eq_iInf A)) r) hr;
Exists.casesOn (iInf_lt_iff.mp hApprox) fun B hB =>
Exists.casesOn (iInf_lt_iff.mp hB) fun hAB hB =>
Exists.casesOn (iInf_lt_iff.mp hB) fun hMeas hB => Exists.intro B ⟨hAB, ⟨hMeas, hB⟩⟩ε:NNRealhε:0 < εh0:0 < ∞⊢ ⨅ i, (fun n => 1 / (↑n + 1)) i ≤ 0 + ↑ε
A:Set ℝhA:¬measure A = ∞hex:∀ (r : ℝ≥0∞), measure A < r → ∃ B, A ⊆ B ∧ MeasurableSet B ∧ measure B < r :=
fun r hr =>
have hApprox := Eq.mp (congrFun' (congrArg LT.lt (measure_eq_iInf A)) r) hr;
Exists.casesOn (iInf_lt_iff.mp hApprox) fun B hB =>
Exists.casesOn (iInf_lt_iff.mp hB) fun hAB hB =>
Exists.casesOn (iInf_lt_iff.mp hB) fun hMeas hB => Exists.intro B ⟨hAB, ⟨hMeas, hB⟩⟩ε:NNRealhε:0 < εh0:0 < ∞n:ℕhn:1 / (↑n + 1) < ε⊢ ⨅ i, (fun n => 1 / (↑n + 1)) i ≤ 0 + ↑ε
have hε' : (((n : ℝ≥0∞) + 1)⁻¹) ≤ ε := A:Set ℝ⊢ ∃ B, A ⊆ B ∧ MeasurableSet B ∧ measure B = measure A
simpa [one_div, Nat.cast_add] using
(show (((1 / (n + 1 : NNReal)) : NNReal) : ℝ≥0∞) ≤ ε A:Set ℝ⊢ ∃ B, A ⊆ B ∧ MeasurableSet B ∧ measure B = measure A All goals completed! 🐙)
exact (iInf_le _ n).trans (A:Set ℝhA:¬measure A = ∞hex:∀ (r : ℝ≥0∞), measure A < r → ∃ B, A ⊆ B ∧ MeasurableSet B ∧ measure B < r :=
fun r hr =>
have hApprox := Eq.mp (congrFun' (congrArg LT.lt (measure_eq_iInf A)) r) hr;
Exists.casesOn (iInf_lt_iff.mp hApprox) fun B hB =>
Exists.casesOn (iInf_lt_iff.mp hB) fun hAB hB =>
Exists.casesOn (iInf_lt_iff.mp hB) fun hMeas hB => Exists.intro B ⟨hAB, ⟨hMeas, hB⟩⟩ε:NNRealhε:0 < εh0:0 < ∞n:ℕhn:1 / (↑n + 1) < εhε':(↑n + 1)⁻¹ ≤ ↑ε :=
Eq.mp
(congrFun'
(congrArg LE.le
(Eq.trans (congrArg ofNNReal (one_div (↑n + 1)))
(coe_inv
(of_eq_true
(Eq.trans
(congrArg Not
(Eq.trans LeftCancelMonoid.mul_eq_one._simp_3
(Eq.trans (congr (congrArg And Nat.cast_eq_zero._simp_1) one_ne_zero._simp_1) (and_false (n = 0)))))
not_false_eq_true)))))
↑ε)
(have this :=
cast
(Eq.trans
(Eq.trans
(Eq.trans
(congrFun'
(congrArg LE.le
(congr (congrArg HDiv.hDiv (Eq.symm Nat.cast_one)) (congrArg (HAdd.hAdd ↑n) (Eq.symm Nat.cast_one))))
ε)
(congrFun' (congrArg LE.le (congrArg (HDiv.hDiv ↑1) (Nat.cast_add._simp_1 n 1))) ε))
(congrFun' (congrArg LE.le (congrFun' (congrArg HDiv.hDiv Nat.cast_one) ↑(n + 1))) ε))
(Eq.symm
(Eq.trans
(Eq.trans
(congrFun'
(congrArg LE.le
(congrArg ofNNReal
(congr (congrArg HDiv.hDiv (Eq.symm Nat.cast_one))
(congrArg (HAdd.hAdd ↑n) (Eq.symm Nat.cast_one)))))
↑ε)
(Eq.trans
(congrFun' (congrArg LE.le (congrArg ofNNReal (congrArg (HDiv.hDiv ↑1) (Nat.cast_add._simp_1 n 1)))) ↑ε)
coe_le_coe._simp_1))
(congrFun' (congrArg LE.le (congrFun' (congrArg HDiv.hDiv Nat.cast_one) ↑(n + 1))) ε))))
(LT.lt.le hn);
this)⊢ (fun n => 1 / (↑n + 1)) n ≤ 0 + ↑ε All goals completed! 🐙)
A:Set ℝhA:¬measure A = ∞hex:∀ (r : ℝ≥0∞), measure A < r → ∃ B, A ⊆ B ∧ MeasurableSet B ∧ measure B < r :=
fun r hr =>
have hApprox := Eq.mp (congrFun' (congrArg LT.lt (measure_eq_iInf A)) r) hr;
Exists.casesOn (iInf_lt_iff.mp hApprox) fun B hB =>
Exists.casesOn (iInf_lt_iff.mp hB) fun hAB hB =>
Exists.casesOn (iInf_lt_iff.mp hB) fun hMeas hB => Exists.intro B ⟨hAB, ⟨hMeas, hB⟩⟩a:ℕ → ℝ≥0∞ha0:⨅ i, a i = 0hane:∀ (n : ℕ), a n ≠ 0⊢ ∃ B, A ⊆ B ∧ MeasurableSet B ∧ measure B = measure A
have hBa : ∀ n : ℕ, ∃ B, A ⊆ B ∧ MeasurableSet B ∧ measure B < measure A + a n :=
fun n ↦ hex _ (ENNReal.lt_add_right hA (A:Set ℝhA:¬measure A = ∞hex:∀ (r : ℝ≥0∞), measure A < r → ∃ B, A ⊆ B ∧ MeasurableSet B ∧ measure B < r :=
fun r hr =>
have hApprox := Eq.mp (congrFun' (congrArg LT.lt (measure_eq_iInf A)) r) hr;
Exists.casesOn (iInf_lt_iff.mp hApprox) fun B hB =>
Exists.casesOn (iInf_lt_iff.mp hB) fun hAB hB =>
Exists.casesOn (iInf_lt_iff.mp hB) fun hMeas hB => Exists.intro B ⟨hAB, ⟨hMeas, hB⟩⟩a:ℕ → ℝ≥0∞ha0:⨅ i, a i = 0hane:∀ (n : ℕ), a n ≠ 0n:ℕ⊢ a n ≠ 0 All goals completed! 🐙))
A:Set ℝhA:¬measure A = ∞hex:∀ (r : ℝ≥0∞), measure A < r → ∃ B, A ⊆ B ∧ MeasurableSet B ∧ measure B < r :=
fun r hr =>
have hApprox := Eq.mp (congrFun' (congrArg LT.lt (measure_eq_iInf A)) r) hr;
Exists.casesOn (iInf_lt_iff.mp hApprox) fun B hB =>
Exists.casesOn (iInf_lt_iff.mp hB) fun hAB hB =>
Exists.casesOn (iInf_lt_iff.mp hB) fun hMeas hB => Exists.intro B ⟨hAB, ⟨hMeas, hB⟩⟩a:ℕ → ℝ≥0∞ha0:⨅ i, a i = 0hane:∀ (n : ℕ), a n ≠ 0B:ℕ → Set ℝhAB:∀ (n : ℕ), A ⊆ B nhBMeas:∀ (n : ℕ), MeasurableSet (B n)hBlt:∀ (n : ℕ), measure (B n) < measure A + a n⊢ ∃ B, A ⊆ B ∧ MeasurableSet B ∧ measure B = measure A
A:Set ℝhA:¬measure A = ∞hex:∀ (r : ℝ≥0∞), measure A < r → ∃ B, A ⊆ B ∧ MeasurableSet B ∧ measure B < r :=
fun r hr =>
have hApprox := Eq.mp (congrFun' (congrArg LT.lt (measure_eq_iInf A)) r) hr;
Exists.casesOn (iInf_lt_iff.mp hApprox) fun B hB =>
Exists.casesOn (iInf_lt_iff.mp hB) fun hAB hB =>
Exists.casesOn (iInf_lt_iff.mp hB) fun hMeas hB => Exists.intro B ⟨hAB, ⟨hMeas, hB⟩⟩a:ℕ → ℝ≥0∞ha0:⨅ i, a i = 0hane:∀ (n : ℕ), a n ≠ 0B:ℕ → Set ℝhAB:∀ (n : ℕ), A ⊆ B nhBMeas:∀ (n : ℕ), MeasurableSet (B n)hBlt:∀ (n : ℕ), measure (B n) < measure A + a n⊢ measure (⋂ n, B n) ≤ measure AA:Set ℝhA:¬measure A = ∞hex:∀ (r : ℝ≥0∞), measure A < r → ∃ B, A ⊆ B ∧ MeasurableSet B ∧ measure B < r :=
fun r hr =>
have hApprox := Eq.mp (congrFun' (congrArg LT.lt (measure_eq_iInf A)) r) hr;
Exists.casesOn (iInf_lt_iff.mp hApprox) fun B hB =>
Exists.casesOn (iInf_lt_iff.mp hB) fun hAB hB =>
Exists.casesOn (iInf_lt_iff.mp hB) fun hMeas hB => Exists.intro B ⟨hAB, ⟨hMeas, hB⟩⟩a:ℕ → ℝ≥0∞ha0:⨅ i, a i = 0hane:∀ (n : ℕ), a n ≠ 0B:ℕ → Set ℝhAB:∀ (n : ℕ), A ⊆ B nhBMeas:∀ (n : ℕ), MeasurableSet (B n)hBlt:∀ (n : ℕ), measure (B n) < measure A + a n⊢ measure A ≤ measure (⋂ n, B n)
A:Set ℝhA:¬measure A = ∞hex:∀ (r : ℝ≥0∞), measure A < r → ∃ B, A ⊆ B ∧ MeasurableSet B ∧ measure B < r :=
fun r hr =>
have hApprox := Eq.mp (congrFun' (congrArg LT.lt (measure_eq_iInf A)) r) hr;
Exists.casesOn (iInf_lt_iff.mp hApprox) fun B hB =>
Exists.casesOn (iInf_lt_iff.mp hB) fun hAB hB =>
Exists.casesOn (iInf_lt_iff.mp hB) fun hMeas hB => Exists.intro B ⟨hAB, ⟨hMeas, hB⟩⟩a:ℕ → ℝ≥0∞ha0:⨅ i, a i = 0hane:∀ (n : ℕ), a n ≠ 0B:ℕ → Set ℝhAB:∀ (n : ℕ), A ⊆ B nhBMeas:∀ (n : ℕ), MeasurableSet (B n)hBlt:∀ (n : ℕ), measure (B n) < measure A + a n⊢ measure (⋂ n, B n) ≤ measure A calc
measure (⋂ n, B n) ≤ ⨅ n, measure (B n) :=
le_iInf fun n ↦ measure_mono (Set.iInter_subset (fun i ↦ B i) n)
_ ≤ ⨅ n, (measure A + a n) := iInf_mono fun n ↦ (hBlt n).le
_ = measure A + ⨅ n, a n := A:Set ℝhA:¬measure A = ∞hex:∀ (r : ℝ≥0∞), measure A < r → ∃ B, A ⊆ B ∧ MeasurableSet B ∧ measure B < r :=
fun r hr =>
have hApprox := Eq.mp (congrFun' (congrArg LT.lt (measure_eq_iInf A)) r) hr;
Exists.casesOn (iInf_lt_iff.mp hApprox) fun B hB =>
Exists.casesOn (iInf_lt_iff.mp hB) fun hAB hB =>
Exists.casesOn (iInf_lt_iff.mp hB) fun hMeas hB => Exists.intro B ⟨hAB, ⟨hMeas, hB⟩⟩a:ℕ → ℝ≥0∞ha0:⨅ i, a i = 0hane:∀ (n : ℕ), a n ≠ 0B:ℕ → Set ℝhAB:∀ (n : ℕ), A ⊆ B nhBMeas:∀ (n : ℕ), MeasurableSet (B n)hBlt:∀ (n : ℕ), measure (B n) < measure A + a n⊢ ⨅ n, measure A + a n = measure A + ⨅ n, a n All goals completed! 🐙
_ = measure A := A:Set ℝhA:¬measure A = ∞hex:∀ (r : ℝ≥0∞), measure A < r → ∃ B, A ⊆ B ∧ MeasurableSet B ∧ measure B < r :=
fun r hr =>
have hApprox := Eq.mp (congrFun' (congrArg LT.lt (measure_eq_iInf A)) r) hr;
Exists.casesOn (iInf_lt_iff.mp hApprox) fun B hB =>
Exists.casesOn (iInf_lt_iff.mp hB) fun hAB hB =>
Exists.casesOn (iInf_lt_iff.mp hB) fun hMeas hB => Exists.intro B ⟨hAB, ⟨hMeas, hB⟩⟩a:ℕ → ℝ≥0∞ha0:⨅ i, a i = 0hane:∀ (n : ℕ), a n ≠ 0B:ℕ → Set ℝhAB:∀ (n : ℕ), A ⊆ B nhBMeas:∀ (n : ℕ), MeasurableSet (B n)hBlt:∀ (n : ℕ), measure (B n) < measure A + a n⊢ measure A + ⨅ n, a n = measure A All goals completed! 🐙
A:Set ℝhA:¬measure A = ∞hex:∀ (r : ℝ≥0∞), measure A < r → ∃ B, A ⊆ B ∧ MeasurableSet B ∧ measure B < r :=
fun r hr =>
have hApprox := Eq.mp (congrFun' (congrArg LT.lt (measure_eq_iInf A)) r) hr;
Exists.casesOn (iInf_lt_iff.mp hApprox) fun B hB =>
Exists.casesOn (iInf_lt_iff.mp hB) fun hAB hB =>
Exists.casesOn (iInf_lt_iff.mp hB) fun hMeas hB => Exists.intro B ⟨hAB, ⟨hMeas, hB⟩⟩a:ℕ → ℝ≥0∞ha0:⨅ i, a i = 0hane:∀ (n : ℕ), a n ≠ 0B:ℕ → Set ℝhAB:∀ (n : ℕ), A ⊆ B nhBMeas:∀ (n : ℕ), MeasurableSet (B n)hBlt:∀ (n : ℕ), measure (B n) < measure A + a n⊢ measure A ≤ measure (⋂ n, B n) All goals completed! 🐙