chore(measure_theory): use ∞ notation for (⊤ : ℝ≥0∞) (#6080)

src/measure_theory/bochner_integration.lean

@@ -191,9 +191,9 @@ variables {μ : measure α}
     finite volume support. -/
 lemma integrable_iff_fin_meas_supp {f : α →ₛ E} {μ : measure α} :
   integrable f μ ↔ f.fin_meas_supp μ :=
-calc integrable f μ ↔ ∫⁻ x, f.map (coe ∘ nnnorm : E → ℝ≥0∞) x ∂μ < ⊤ :
+calc integrable f μ ↔ ∫⁻ x, f.map (coe ∘ nnnorm : E → ℝ≥0∞) x ∂μ < ∞ :
   and_iff_right f.ae_measurable
-... ↔ (f.map (coe ∘ nnnorm : E → ℝ≥0∞)).lintegral μ < ⊤ : by rw lintegral_eq_lintegral
+... ↔ (f.map (coe ∘ nnnorm : E → ℝ≥0∞)).lintegral μ < ∞ : by rw lintegral_eq_lintegral
 ... ↔ (f.map (coe ∘ nnnorm : E → ℝ≥0∞)).fin_meas_supp μ : iff.symm $
   fin_meas_supp.iff_lintegral_lt_top $ eventually_of_forall $ λ x, coe_lt_top
 ... ↔ _ : fin_meas_supp.map_iff $ λ b, coe_eq_zero.trans nnnorm_eq_zero
@@ -256,7 +256,7 @@ end
     `α →ₛ ℝ≥0∞`. But since `ℝ≥0∞` is not a `normed_space`, we need some form of coercion.
     See `integral_eq_lintegral` for a simpler version. -/
 lemma integral_eq_lintegral' {f : α →ₛ E} {g : E → ℝ≥0∞} (hf : integrable f μ) (hg0 : g 0 = 0)
-  (hgt : ∀b, g b < ⊤):
+  (hgt : ∀b, g b < ∞):
   (f.map (ennreal.to_real ∘ g)).integral μ = ennreal.to_real (∫⁻ a, g (f a) ∂μ) :=
 begin
   have hf' : f.fin_meas_supp μ := integrable_iff_fin_meas_supp.1 hf,
@@ -630,7 +630,7 @@ begin
 end
 
 lemma lintegral_edist_to_simple_func_lt_top (f g : α →₁ₛ[μ] E) :
-  ∫⁻ (x : α), edist ((to_simple_func f) x) ((to_simple_func g) x) ∂μ < ⊤ :=
+  ∫⁻ (x : α), edist ((to_simple_func f) x) ((to_simple_func g) x) ∂μ < ∞ :=
 begin
   rw lintegral_rw₂ (to_simple_func_eq_to_fun f) (to_simple_func_eq_to_fun g),
   exact lintegral_edist_to_fun_lt_top _ _
@@ -1255,7 +1255,7 @@ begin
   rw [← lt_top_iff_ne_top], convert hfi.has_finite_integral, ext1 x, rw [real.nnnorm_coe_eq_self]
 end
 
-lemma integral_to_real {f : α → ℝ≥0∞} (hfm : ae_measurable f μ) (hf : ∀ᵐ x ∂μ, f x < ⊤) :
+lemma integral_to_real {f : α → ℝ≥0∞} (hfm : ae_measurable f μ) (hf : ∀ᵐ x ∂μ, f x < ∞) :
   ∫ a, (f a).to_real ∂μ = (∫⁻ a, f a ∂μ).to_real :=
 begin
   rw [integral_eq_lintegral_of_nonneg_ae _ hfm.to_real],
@@ -1378,7 +1378,7 @@ end
 
 @[simp] lemma integral_const (c : E) : ∫ x : α, c ∂μ = (μ univ).to_real • c :=
 begin
-  by_cases hμ : μ univ < ⊤,
+  by_cases hμ : μ univ < ∞,
   { haveI : finite_measure μ := ⟨hμ⟩,
     calc ∫ x : α, c ∂μ = (simple_func.const α c).integral μ :
       ((simple_func.const α c).integral_eq_integral (integrable_const _)).symm
@@ -1449,7 +1449,7 @@ end
 norm_le_zero_iff.1 $ le_trans (norm_integral_le_lintegral_norm f) $ by simp
 
 private lemma integral_smul_measure_aux {f : α → E} {c : ℝ≥0∞}
-  (h0 : 0 < c) (hc : c < ⊤) (fmeas : measurable f) (hfi : integrable f μ) :
+  (h0 : 0 < c) (hc : c < ∞) (fmeas : measurable f) (hfi : integrable f μ) :
   ∫ x, f x ∂(c • μ) = c.to_real • ∫ x, f x ∂μ :=
 begin
   refine tendsto_nhds_unique _
@@ -1469,26 +1469,26 @@ begin
   by_cases hfm : ae_measurable f μ, swap,
   { have : ¬ (ae_measurable f (c • μ)), by simpa [ne_of_gt h0] using hfm,
     simp [integral_non_ae_measurable, hfm, this] },
-  -- `c = ⊤`
-  rcases (le_top : c ≤ ⊤).eq_or_lt with rfl|hc,
+  -- `c = ∞`
+  rcases (le_top : c ≤ ∞).eq_or_lt with rfl|hc,
   { rw [ennreal.top_to_real, zero_smul],
     by_cases hf : f =ᵐ[μ] 0,
-    { have : f =ᵐ[⊤ • μ] 0 := ae_smul_measure hf ⊤,
+    { have : f =ᵐ[∞ • μ] 0 := ae_smul_measure hf ∞,
       exact integral_eq_zero_of_ae this },
     { apply integral_undef,
-      rw [integrable, has_finite_integral, iff_true_intro (hfm.smul_measure ⊤), true_and,
+      rw [integrable, has_finite_integral, iff_true_intro (hfm.smul_measure ∞), true_and,
           lintegral_smul_measure, top_mul, if_neg],
       { apply lt_irrefl },
       { rw [lintegral_eq_zero_iff' hfm.ennnorm],
         refine λ h, hf (h.mono $ λ x, _),
         simp } } },
-  -- `f` is not integrable and `0 < c < ⊤`
+  -- `f` is not integrable and `0 < c < ∞`
   by_cases hfi : integrable f μ, swap,
   { rw [integral_undef hfi, smul_zero],
     refine integral_undef (mt (λ h, _) hfi),
     convert h.smul_measure (ennreal.inv_lt_top.2 h0),
     rw [smul_smul, ennreal.inv_mul_cancel (ne_of_gt h0) (ne_of_lt hc), one_smul] },
-  -- Main case: `0 < c < ⊤`, `f` is almost everywhere measurable and integrable
+  -- Main case: `0 < c < ∞`, `f` is almost everywhere measurable and integrable
   let g := hfm.mk f,
   calc ∫ x, f x ∂(c • μ) = ∫ x, g x ∂(c • μ) : integral_congr_ae $ ae_smul_measure hfm.ae_eq_mk c
   ... = c.to_real • ∫ x, g x ∂μ :

src/measure_theory/borel_space.lean

@@ -1089,7 +1089,7 @@ lemma measurable.ennreal_of_real {f : α → ℝ} (hf : measurable f) :
 ennreal.continuous_of_real.measurable.comp hf
 
 /-- The set of finite `ℝ≥0∞` numbers is `measurable_equiv` to `ℝ≥0`. -/
-def measurable_equiv.ennreal_equiv_nnreal : {r : ℝ≥0∞ | r ≠ ⊤} ≃ᵐ ℝ≥0 :=
+def measurable_equiv.ennreal_equiv_nnreal : {r : ℝ≥0∞ | r ≠ ∞} ≃ᵐ ℝ≥0 :=
 ennreal.ne_top_homeomorph_nnreal.to_measurable_equiv
 
 namespace ennreal
@@ -1099,20 +1099,20 @@ measurable_id.ennreal_coe
 
 lemma measurable_of_measurable_nnreal {f : ℝ≥0∞ → α}
   (h : measurable (λ p : ℝ≥0, f p)) : measurable f :=
-measurable_of_measurable_on_compl_singleton ⊤
+measurable_of_measurable_on_compl_singleton ∞
   (measurable_equiv.ennreal_equiv_nnreal.symm.measurable_coe_iff.1 h)
 
 /-- `ℝ≥0∞` is `measurable_equiv` to `ℝ≥0 ⊕ unit`. -/
 def ennreal_equiv_sum : ℝ≥0∞ ≃ᵐ ℝ≥0 ⊕ unit :=
 { measurable_to_fun  := measurable_of_measurable_nnreal measurable_inl,
-  measurable_inv_fun := measurable_sum measurable_coe (@measurable_const ℝ≥0∞ unit _ _ ⊤),
+  measurable_inv_fun := measurable_sum measurable_coe (@measurable_const ℝ≥0∞ unit _ _ ∞),
   .. equiv.option_equiv_sum_punit ℝ≥0 }
 
 open function (uncurry)
 
 lemma measurable_of_measurable_nnreal_prod [measurable_space β] [measurable_space γ]
   {f : ℝ≥0∞ × β → γ} (H₁ : measurable (λ p : ℝ≥0 × β, f (p.1, p.2)))
-  (H₂ : measurable (λ x, f (⊤, x))) :
+  (H₂ : measurable (λ x, f (∞, x))) :
   measurable f :=
 let e : ℝ≥0∞ × β ≃ᵐ ℝ≥0 × β ⊕ unit × β :=
   (ennreal_equiv_sum.prod_congr (measurable_equiv.refl β)).trans
@@ -1121,7 +1121,7 @@ e.symm.measurable_coe_iff.1 $ measurable_sum H₁ (H₂.comp measurable_id.snd)
 
 lemma measurable_of_measurable_nnreal_nnreal [measurable_space β]
   {f : ℝ≥0∞ × ℝ≥0∞ → β} (h₁ : measurable (λ p : ℝ≥0 × ℝ≥0, f (p.1, p.2)))
-  (h₂ : measurable (λ r : ℝ≥0, f (⊤, r))) (h₃ : measurable (λ r : ℝ≥0, f (r, ⊤))) :
+  (h₂ : measurable (λ r : ℝ≥0, f (∞, r))) (h₃ : measurable (λ r : ℝ≥0, f (r, ∞))) :
   measurable f :=
 measurable_of_measurable_nnreal_prod
   (measurable_swap_iff.1 $ measurable_of_measurable_nnreal_prod (h₁.comp measurable_swap) h₃)
@@ -1386,7 +1386,7 @@ variables [topological_space α] {μ : measure α}
   - it is outer regular: `μ(A) = inf { μ(U) | A ⊆ U open }` for `A` measurable;
   - it is inner regular: `μ(U) = sup { μ(K) | K ⊆ U compact }` for `U` open. -/
 structure regular (μ : measure α) : Prop :=
-(lt_top_of_is_compact : ∀ {{K : set α}}, is_compact K → μ K < ⊤)
+(lt_top_of_is_compact : ∀ {{K : set α}}, is_compact K → μ K < ∞)
 (outer_regular : ∀ {{A : set α}}, measurable_set A →
   (⨅ (U : set α) (h : is_open U) (h2 : A ⊆ U), μ U) ≤ μ A)
 (inner_regular : ∀ {{U : set α}}, is_open U →
@@ -1429,7 +1429,7 @@ begin
     rw [map_apply hf hK.measurable_set] }
 end
 
-protected lemma smul (hμ : μ.regular) {x : ℝ≥0∞} (hx : x < ⊤) :
+protected lemma smul (hμ : μ.regular) {x : ℝ≥0∞} (hx : x < ∞) :
   (x • μ).regular :=
 begin
   split,
@@ -1460,11 +1460,11 @@ end measure_theory
 
 lemma is_compact.measure_lt_top_of_nhds_within [topological_space α]
   {s : set α} {μ : measure α} (h : is_compact s) (hμ : ∀ x ∈ s, μ.finite_at_filter (𝓝[s] x)) :
-  μ s < ⊤ :=
+  μ s < ∞ :=
 is_compact.induction_on h (by simp) (λ s t hst ht, (measure_mono hst).trans_lt ht)
   (λ s t hs ht, (measure_union_le s t).trans_lt (ennreal.add_lt_top.2 ⟨hs, ht⟩)) hμ
 
 lemma is_compact.measure_lt_top [topological_space α] {s : set α} {μ : measure α}
   [locally_finite_measure μ] (h : is_compact s) :
-  μ s < ⊤ :=
+  μ s < ∞ :=
 h.measure_lt_top_of_nhds_within $ λ x hx, μ.finite_at_nhds_within _ _

src/measure_theory/content.lean

@@ -84,7 +84,7 @@ lemma inner_content_mono {μ : compacts G → ℝ≥0∞} ⦃U V : set G⦄ (hU
 supr_le_supr $ λ K, supr_le_supr_const $ λ hK, subset.trans hK h2
 
 lemma inner_content_exists_compact {μ : compacts G → ℝ≥0∞} {U : opens G}
-  (hU : inner_content μ U < ⊤) {ε : ℝ≥0} (hε : 0 < ε) :
+  (hU : inner_content μ U < ∞) {ε : ℝ≥0} (hε : 0 < ε) :
   ∃ K : compacts G, K.1 ⊆ U ∧ inner_content μ U ≤ μ K + ε :=
 begin
   have h'ε := ennreal.zero_lt_coe_iff.2 hε,
@@ -208,15 +208,15 @@ lemma of_content_interior_compacts (h3 : ∀ (K₁ K₂ : compacts G), K₁.1 
 le_trans (le_of_eq $ of_content_opens h2 (opens.interior K.1))
          (inner_content_le h3 _ _ interior_subset)
 
-lemma of_content_exists_compact {U : opens G} (hU : of_content μ h1 U < ⊤) {ε : ℝ≥0}
+lemma of_content_exists_compact {U : opens G} (hU : of_content μ h1 U < ∞) {ε : ℝ≥0}
   (hε : 0 < ε) : ∃ K : compacts G, K.1 ⊆ U ∧ of_content μ h1 U ≤ of_content μ h1 K.1 + ε :=
 begin
   rw [of_content_opens h2] at hU ⊢,
   rcases inner_content_exists_compact hU hε with ⟨K, h1K, h2K⟩,
   exact ⟨K, h1K, le_trans h2K $ add_le_add_right (le_of_content_compacts h2 K) _⟩,
 end
 
-lemma of_content_exists_open {A : set G} (hA : of_content μ h1 A < ⊤) {ε : ℝ≥0} (hε : 0 < ε) :
+lemma of_content_exists_open {A : set G} (hA : of_content μ h1 A < ∞) {ε : ℝ≥0} (hε : 0 < ε) :
   ∃ U : opens G, A ⊆ U ∧ of_content μ h1 U ≤ of_content μ h1 A + ε :=
 begin
   rcases induced_outer_measure_exists_set _ _ inner_content_mono hA hε with ⟨U, hU, h2U, h3U⟩,

src/measure_theory/decomposition.lean

@@ -23,7 +23,7 @@ private lemma aux {m : ℕ} {γ d : ℝ} (h : γ - (1 / 2) ^ m < d) :
   γ - 2 * (1 / 2) ^ m + (1 / 2) ^ m ≤ d :=
 by linarith
 
-lemma hahn_decomposition (hμ : μ univ < ⊤) (hν : ν univ < ⊤) :
+lemma hahn_decomposition (hμ : μ univ < ∞) (hν : ν univ < ∞) :
   ∃s, measurable_set s ∧
     (∀t, measurable_set t → t ⊆ s → ν t ≤ μ t) ∧
     (∀t, measurable_set t → t ⊆ sᶜ → μ t ≤ ν t) :=
@@ -32,8 +32,8 @@ begin
   let c : set ℝ := d '' {s | measurable_set s },
   let γ : ℝ := Sup c,
 
-  have hμ : ∀s, μ s < ⊤ := assume s, lt_of_le_of_lt (measure_mono $ subset_univ _) hμ,
-  have hν : ∀s, ν s < ⊤ := assume s, lt_of_le_of_lt (measure_mono $ subset_univ _) hν,
+  have hμ : ∀s, μ s < ∞ := assume s, lt_of_le_of_lt (measure_mono $ subset_univ _) hμ,
+  have hν : ∀s, ν s < ∞ := assume s, lt_of_le_of_lt (measure_mono $ subset_univ _) hν,
   have to_nnreal_μ : ∀s, ((μ s).to_nnreal : ℝ≥0∞) = μ s :=
     (assume s, ennreal.coe_to_nnreal $ ne_top_of_lt $ hμ _),
   have to_nnreal_ν : ∀s, ((ν s).to_nnreal : ℝ≥0∞) = ν s :=
@@ -56,7 +56,7 @@ begin
   { assume s hs hm,
     refine tendsto.sub _ _;
       refine (nnreal.tendsto_coe.2 $
-        (ennreal.tendsto_to_nnreal $ @ne_top_of_lt _ _ _ ⊤ _).comp $ tendsto_measure_Union hs hm),
+        (ennreal.tendsto_to_nnreal $ @ne_top_of_lt _ _ _ ∞ _).comp $ tendsto_measure_Union hs hm),
     exact hμ _,
     exact hν _ },
 
@@ -65,7 +65,7 @@ begin
   { assume s hs hm,
     refine tendsto.sub _ _;
       refine (nnreal.tendsto_coe.2 $
-        (ennreal.tendsto_to_nnreal $ @ne_top_of_lt _ _ _ ⊤ _).comp $ tendsto_measure_Inter hs hm _),
+        (ennreal.tendsto_to_nnreal $ @ne_top_of_lt _ _ _ ∞ _).comp $ tendsto_measure_Inter hs hm _),
     exact hμ _,
     exact ⟨0, hμ _⟩,
     exact hν _,

src/measure_theory/haar_measure.lean

@@ -470,12 +470,12 @@ lemma haar_outer_measure_le_echaar {K₀ : positive_compacts G} {U : set G} (hU
 (outer_measure.of_content_le echaar_sup_le echaar_mono ⟨U, hU⟩ K h : _)
 
 lemma haar_outer_measure_exists_open {K₀ : positive_compacts G} {A : set G}
-  (hA : haar_outer_measure K₀ A < ⊤) {ε : ℝ≥0} (hε : 0 < ε) :
+  (hA : haar_outer_measure K₀ A < ∞) {ε : ℝ≥0} (hε : 0 < ε) :
   ∃ U : opens G, A ⊆ U ∧ haar_outer_measure K₀ U ≤ haar_outer_measure K₀ A + ε :=
 outer_measure.of_content_exists_open echaar_sup_le hA hε
 
 lemma haar_outer_measure_exists_compact {K₀ : positive_compacts G} {U : opens G}
-  (hU : haar_outer_measure K₀ U < ⊤) {ε : ℝ≥0} (hε : 0 < ε) :
+  (hU : haar_outer_measure K₀ U < ∞) {ε : ℝ≥0} (hε : 0 < ε) :
   ∃ K : compacts G, K.1 ⊆ U ∧ haar_outer_measure K₀ U ≤ haar_outer_measure K₀ K.1 + ε :=
 outer_measure.of_content_exists_compact echaar_sup_le hU hε
 
@@ -502,7 +502,7 @@ lemma haar_outer_measure_self_pos {K₀ : positive_compacts G} :
   ((haar_outer_measure K₀).mono interior_subset)
 
 lemma haar_outer_measure_lt_top_of_is_compact [locally_compact_space G] {K₀ : positive_compacts G}
-  {K : set G} (hK : is_compact K) : haar_outer_measure K₀ K < ⊤ :=
+  {K : set G} (hK : is_compact K) : haar_outer_measure K₀ K < ∞ :=
 begin
   rcases exists_compact_superset hK with ⟨F, h1F, h2F⟩,
   refine ((haar_outer_measure K₀).mono h2F).trans_lt _,
@@ -612,7 +612,7 @@ begin
 end
 
 theorem regular_of_left_invariant (hμ : is_mul_left_invariant μ) {K} (hK : is_compact K)
-  (h2K : (interior K).nonempty) (hμK : μ K < ⊤) : regular μ :=
+  (h2K : (interior K).nonempty) (hμK : μ K < ∞) : regular μ :=
 begin
   rw [haar_measure_unique hμ ⟨K, hK, h2K⟩],
   exact regular.smul regular_haar_measure hμK