feat(measure_theory): generalize some lemmas to outer_measure (#11501)

src/measure_theory/measure/measure_space_def.lean

@@ -223,38 +223,42 @@ lemma measure_Union_null [encodable β] {s : β → set α} :
 
 @[simp] lemma measure_Union_null_iff [encodable ι] {s : ι → set α} :
   μ (⋃ i, s i) = 0 ↔ ∀ i, μ (s i) = 0 :=
-⟨λ h i, measure_mono_null (subset_Union _ _) h, measure_Union_null⟩
+μ.to_outer_measure.Union_null_iff
 
 lemma measure_bUnion_null_iff {s : set ι} (hs : countable s) {t : ι → set α} :
   μ (⋃ i ∈ s, t i) = 0 ↔ ∀ i ∈ s, μ (t i) = 0 :=
-by { haveI := hs.to_encodable, rw [bUnion_eq_Union, measure_Union_null_iff, set_coe.forall], refl }
+μ.to_outer_measure.bUnion_null_iff hs
 
 lemma measure_sUnion_null_iff {S : set (set α)} (hS : countable S) :
   μ (⋃₀ S) = 0 ↔ ∀ s ∈ S, μ s = 0 :=
-by rw [sUnion_eq_bUnion, measure_bUnion_null_iff hS]
+μ.to_outer_measure.sUnion_null_iff hS
 
 theorem measure_union_le (s₁ s₂ : set α) : μ (s₁ ∪ s₂) ≤ μ s₁ + μ s₂ :=
 μ.to_outer_measure.union _ _
 
 lemma measure_union_null : μ s₁ = 0 → μ s₂ = 0 → μ (s₁ ∪ s₂) = 0 :=
 μ.to_outer_measure.union_null
 
-lemma measure_union_null_iff : μ (s₁ ∪ s₂) = 0 ↔ μ s₁ = 0 ∧ μ s₂ = 0:=
+@[simp] lemma measure_union_null_iff : μ (s₁ ∪ s₂) = 0 ↔ μ s₁ = 0 ∧ μ s₂ = 0:=
 ⟨λ h, ⟨measure_mono_null (subset_union_left _ _) h, measure_mono_null (subset_union_right _ _) h⟩,
   λ h, measure_union_null h.1 h.2⟩
 
 lemma measure_union_lt_top (hs : μ s < ∞) (ht : μ t < ∞) : μ (s ∪ t) < ∞ :=
 (measure_union_le s t).trans_lt (ennreal.add_lt_top.mpr ⟨hs, ht⟩)
 
-lemma measure_union_lt_top_iff : μ (s ∪ t) < ∞ ↔ μ s < ∞ ∧ μ t < ∞ :=
+@[simp] lemma measure_union_lt_top_iff : μ (s ∪ t) < ∞ ↔ μ s < ∞ ∧ μ t < ∞ :=
 begin
   refine ⟨λ h, ⟨_, _⟩, λ h, measure_union_lt_top h.1 h.2⟩,
   { exact (measure_mono (set.subset_union_left s t)).trans_lt h, },
   { exact (measure_mono (set.subset_union_right s t)).trans_lt h, },
 end
 
 lemma measure_union_ne_top (hs : μ s ≠ ∞) (ht : μ t ≠ ∞) : μ (s ∪ t) ≠ ∞ :=
-((measure_union_le s t).trans_lt (lt_top_iff_ne_top.mpr (ennreal.add_ne_top.mpr ⟨hs, ht⟩))).ne
+(measure_union_lt_top hs.lt_top ht.lt_top).ne
+
+@[simp] lemma measure_union_eq_top_iff : μ (s ∪ t) = ∞ ↔ μ s = ∞ ∨ μ t = ∞ :=
+not_iff_not.1 $ by simp only [← lt_top_iff_ne_top, ← ne.def, not_or_distrib,
+  measure_union_lt_top_iff]
 
 lemma exists_measure_pos_of_not_measure_Union_null [encodable β] {s : β → set α}
   (hs : μ (⋃ n, s n) ≠ 0) : ∃ n, 0 < μ (s n) :=

src/measure_theory/measure/outer_measure.lean

@@ -79,15 +79,30 @@ instance : has_coe_to_fun (outer_measure α) (λ _, set α → ℝ≥0∞) := 
 theorem mono' (m : outer_measure α) {s₁ s₂}
   (h : s₁ ⊆ s₂) : m s₁ ≤ m s₂ := m.mono h
 
+theorem mono_null (m : outer_measure α) {s t} (h : s ⊆ t) (ht : m t = 0) : m s = 0 :=
+nonpos_iff_eq_zero.mp $ ht ▸ m.mono' h
+
 protected theorem Union (m : outer_measure α)
   {β} [encodable β] (s : β → set α) :
-  m (⋃i, s i) ≤ ∑'i, m (s i) :=
+  m (⋃ i, s i) ≤ ∑' i, m (s i) :=
 rel_supr_tsum m m.empty (≤) m.Union_nat s
 
-lemma Union_null (m : outer_measure α)
-  {β} [encodable β] {s : β → set α} (h : ∀ i, m (s i) = 0) : m (⋃i, s i) = 0 :=
+lemma Union_null [encodable β] (m : outer_measure α) {s : β → set α} (h : ∀ i, m (s i) = 0) :
+  m (⋃ i, s i) = 0 :=
 by simpa [h] using m.Union s
 
+@[simp] lemma Union_null_iff [encodable β] (m : outer_measure α) {s : β → set α} :
+  m (⋃ i, s i) = 0 ↔ ∀ i, m (s i) = 0 :=
+⟨λ h i, m.mono_null (subset_Union _ _) h, m.Union_null⟩
+
+lemma bUnion_null_iff (m : outer_measure α) {s : set β} (hs : countable s) {t : β → set α} :
+  m (⋃ i ∈ s, t i) = 0 ↔ ∀ i ∈ s, m (t i) = 0 :=
+by { haveI := hs.to_encodable, rw [bUnion_eq_Union, Union_null_iff, set_coe.forall'] }
+
+lemma sUnion_null_iff (m : outer_measure α) {S : set (set α)} (hS : countable S) :
+  m (⋃₀ S) = 0 ↔ ∀ s ∈ S, m s = 0 :=
+by rw [sUnion_eq_bUnion, m.bUnion_null_iff hS]
+
 protected lemma Union_finset (m : outer_measure α) (s : β → set α) (t : finset β) :
   m (⋃i ∈ t, s i) ≤ ∑ i in t, m (s i) :=
 rel_supr_sum m m.empty (≤) m.Union_nat s t
@@ -97,7 +112,7 @@ protected lemma union (m : outer_measure α) (s₁ s₂ : set α) :
 rel_sup_add m m.empty (≤) m.Union_nat s₁ s₂
 
 /-- If `s : ι → set α` is a sequence of sets, `S = ⋃ n, s n`, and `m (S \ s n)` tends to zero along
-some nontrivial filter (usually `at_top` on `α = ℕ`), then `m S = ⨆ n, m (s n)`. -/
+some nontrivial filter (usually `at_top` on `ι = ℕ`), then `m S = ⨆ n, m (s n)`. -/
 lemma Union_of_tendsto_zero {ι} (m : outer_measure α) {s : ι → set α}
   (l : filter ι) [ne_bot l] (h0 : tendsto (λ k, m ((⋃ n, s n) \ s k)) l (𝓝 0)) :
   m (⋃ n, s n) = ⨆ n, m (s n) :=
@@ -227,6 +242,9 @@ instance outer_measure.order_bot : order_bot (outer_measure α) :=
 { bot_le      := assume a s, by simp only [coe_zero, pi.zero_apply, coe_bot, zero_le],
   ..outer_measure.has_bot }
 
+lemma univ_eq_zero_iff (m : outer_measure α) : m univ = 0 ↔ m = 0 :=
+⟨λ h, bot_unique $ λ s, (m.mono' $ subset_univ s).trans_eq h, λ h, h.symm ▸ rfl⟩
+
 section supremum
 
 instance : has_Sup (outer_measure α) :=