chore(measure_theory/measure/outer_measure): lemmas about zero and top (#18983)

eric-wieser · eric-wieser · commit 343e80208d29 · 2023-05-12T08:46:28.000Z
diff --git a/src/measure_theory/measure/hausdorff.lean b/src/measure_theory/measure/hausdorff.lean
@@ -358,6 +358,14 @@ begin
   { simp [h0] }
 end
 
+@[simp] lemma mk_metric_top : (mk_metric (λ _, ∞ : ℝ≥0∞ → ℝ≥0∞) : outer_measure X) = ⊤ :=
+begin
+  simp_rw [mk_metric, mk_metric', mk_metric'.pre, extend_top, bounded_by_top, eq_top_iff],
+  rw le_supr_iff,
+  intros b hb,
+  simpa using hb ⊤,
+end
+
 /-- If `m₁ d ≤ m₂ d` for `d < ε` for some `ε > 0` (we use `≤ᶠ[𝓝[≥] 0]` to state this), then
 `mk_metric m₁ hm₁ ≤ mk_metric m₂ hm₂`-/
 lemma mk_metric_mono {m₁ m₂ : ℝ≥0∞ → ℝ≥0∞} (hle : m₁ ≤ᶠ[𝓝[≥] 0] m₂) :
@@ -465,6 +473,12 @@ begin
   exact outer_measure.mk_metric_mono_smul hc h0 hle s
 end
 
+@[simp] lemma mk_metric_top : (mk_metric (λ _, ∞ : ℝ≥0∞ → ℝ≥0∞) : measure X) = ⊤ :=
+begin
+  apply to_outer_measure_injective,
+  rw [mk_metric_to_outer_measure, outer_measure.mk_metric_top, to_outer_measure_top],
+end
+
 /-- If `m₁ d ≤ m₂ d` for `d < ε` for some `ε > 0` (we use `≤ᶠ[𝓝[≥] 0]` to state this), then
 `mk_metric m₁ hm₁ ≤ mk_metric m₂ hm₂`-/
 lemma mk_metric_mono {m₁ m₂ : ℝ≥0∞ → ℝ≥0∞} (hle : m₁ ≤ᶠ[𝓝[≥] 0] m₂) :
diff --git a/src/measure_theory/measure/measure_space.lean b/src/measure_theory/measure/measure_space.lean
@@ -938,6 +938,17 @@ instance [measurable_space α] : complete_lattice (measure α) :=
 
 end Inf
 
+@[simp] lemma _root_.measure_theory.outer_measure.to_measure_top [measurable_space α] :
+  (⊤ : outer_measure α).to_measure (by rw [outer_measure.top_caratheodory]; exact le_top)
+    = (⊤ : measure α) :=
+top_unique $ λ s hs,
+    by cases s.eq_empty_or_nonempty with h h;
+      simp [h, to_measure_apply ⊤ _ hs, outer_measure.top_apply]
+
+@[simp] lemma to_outer_measure_top [measurable_space α] :
+  (⊤ : measure α).to_outer_measure = (⊤ : outer_measure α) :=
+by rw [←outer_measure.to_measure_top, to_measure_to_outer_measure, outer_measure.trim_top]
+
 @[simp] lemma top_add : ⊤ + μ = ⊤ := top_unique $ measure.le_add_right le_rfl
 @[simp] lemma add_top : μ + ⊤ = ⊤ := top_unique $ measure.le_add_left le_rfl
 
diff --git a/src/measure_theory/measure/outer_measure.lean b/src/measure_theory/measure/outer_measure.lean
@@ -704,6 +704,20 @@ theorem le_bounded_by' {μ : outer_measure α} :
   μ ≤ bounded_by m ↔ ∀ s : set α, s.nonempty → μ s ≤ m s :=
 by { rw [le_bounded_by, forall_congr], intro s, cases s.eq_empty_or_nonempty with h h; simp [h] }
 
+@[simp] lemma bounded_by_top : bounded_by (⊤ : set α → ℝ≥0∞) = ⊤ :=
+begin
+  rw [eq_top_iff, le_bounded_by'],
+  intros s hs,
+  rw top_apply hs,
+  exact le_rfl,
+end
+
+@[simp] lemma bounded_by_zero : bounded_by (0 : set α → ℝ≥0∞) = 0 :=
+begin
+  rw [←coe_bot, eq_bot_iff],
+  apply bounded_by_le,
+end
+
 lemma smul_bounded_by {c : ℝ≥0∞} (hc : c ≠ ∞) : c • bounded_by m = bounded_by (c • m) :=
 begin
   simp only [bounded_by, smul_of_function hc],
@@ -1094,6 +1108,10 @@ lemma extend_congr {β : Type*} {Pb : β → Prop} {mb : Π s : β, Pb s → ℝ
   extend m sa = extend mb sb :=
 infi_congr_Prop hP (λ h, hm _ _)
 
+@[simp] lemma extend_top {α : Type*} {P : α → Prop} :
+  extend (λ s h, ∞ : Π (s : α), P s → ℝ≥0∞) = ⊤ :=
+funext $ λ x, infi_eq_top.mpr $ λ i, rfl
+
 end extend
 
 section extend_set
@@ -1337,6 +1355,8 @@ by simp [infi_subtype, infi_and, trim_eq_infi]
 theorem trim_trim (m : outer_measure α) : m.trim.trim = m.trim :=
 trim_eq_trim_iff.2 $ λ s, m.trim_eq
 
+@[simp] theorem trim_top : (⊤ : outer_measure α).trim = ⊤ := eq_top_iff.2 $ le_trim _
+
 @[simp] theorem trim_zero : (0 : outer_measure α).trim = 0 :=
 ext $ λ s, le_antisymm
   (le_trans ((trim 0).mono (subset_univ s)) $
