feat(measure_theory): use more [(pseudo_)metrizable_space] (#14232)

* Use `[metrizable_space α]` or `[pseudo_metrizable_space α]` assumptions in some lemmas, replace `tendsto_metric` with `tendsto_metrizable` in the names of these lemmas.
* Drop `measurable_of_tendsto_metric'` and `measurable_of_tendsto_metric` in favor of `measurable_of_tendsto_metrizable'` and `measurable_of_tendsto_metrizable`.

Author: urkud

src/measure_theory/constructions/borel_space.lean

@@ -1364,9 +1364,9 @@ begin
   rw [A, B, C, add_assoc],
 end
 
-section metric_space
+section pseudo_metric_space
 
-variables [metric_space α] [measurable_space α] [opens_measurable_space α]
+variables [pseudo_metric_space α] [measurable_space α] [opens_measurable_space α]
 variables [measurable_space β] {x : α} {ε : ℝ}
 
 open metric
@@ -1448,19 +1448,20 @@ begin
   exact h's.closure_eq.symm
 end
 
+end pseudo_metric_space
+
 /-- Given a compact set in a proper space, the measure of its `r`-closed thickenings converges to
 its measure as `r` tends to `0`. -/
-lemma tendsto_measure_cthickening_of_is_compact [proper_space α] {μ : measure α}
+lemma tendsto_measure_cthickening_of_is_compact [metric_space α] [measurable_space α]
+  [opens_measurable_space α] [proper_space α] {μ : measure α}
   [is_finite_measure_on_compacts μ] {s : set α} (hs : is_compact s) :
-  tendsto (λ r, μ (cthickening r s)) (𝓝 0) (𝓝 (μ s)) :=
+  tendsto (λ r, μ (metric.cthickening r s)) (𝓝 0) (𝓝 (μ s)) :=
 tendsto_measure_cthickening_of_is_closed
-  ⟨1, zero_lt_one, (bounded.measure_lt_top hs.bounded.cthickening).ne⟩ hs.is_closed
+  ⟨1, zero_lt_one, hs.bounded.cthickening.measure_lt_top.ne⟩ hs.is_closed
 
-end metric_space
+section pseudo_emetric_space
 
-section emetric_space
-
-variables [emetric_space α] [measurable_space α] [opens_measurable_space α]
+variables [pseudo_emetric_space α] [measurable_space α] [opens_measurable_space α]
 variables [measurable_space β] {x : α} {ε : ℝ≥0∞}
 
 open emetric
@@ -1502,7 +1503,7 @@ lemma ae_measurable.edist {f g : β → α} {μ : measure β}
   (hf : ae_measurable f μ) (hg : ae_measurable g μ) : ae_measurable (λ a, edist (f a) (g a)) μ :=
 (@continuous_edist α _).ae_measurable2 hf hg
 
-end emetric_space
+end pseudo_emetric_space
 
 namespace real
 open measurable_space measure_theory
@@ -1846,7 +1847,7 @@ end normed_group
 
 section limits
 
-variables [measurable_space β] [metric_space β] [borel_space β]
+variables [topological_space β] [pseudo_metrizable_space β] [measurable_space β] [borel_space β]
 
 open metric
 
@@ -1885,13 +1886,14 @@ lemma measurable_of_tendsto_nnreal {f : ℕ → α → ℝ≥0} {g : α → ℝ
   (hf : ∀ i, measurable (f i)) (lim : tendsto f at_top (𝓝 g)) : measurable g :=
 measurable_of_tendsto_nnreal' at_top hf lim
 
-/-- A limit (over a general filter) of measurable functions valued in a metric space is measurable.
--/
-lemma measurable_of_tendsto_metric' {ι} {f : ι → α → β} {g : α → β}
+/-- A limit (over a general filter) of measurable functions valued in a (pseudo) metrizable space is
+measurable. -/
+lemma measurable_of_tendsto_metrizable' {ι} {f : ι → α → β} {g : α → β}
   (u : filter ι) [ne_bot u] [is_countably_generated u]
   (hf : ∀ i, measurable (f i)) (lim : tendsto f u (𝓝 g)) :
   measurable g :=
 begin
+  letI : pseudo_metric_space β := pseudo_metrizable_space_pseudo_metric β,
   apply measurable_of_is_closed', intros s h1s h2s h3s,
   have : measurable (λ x, inf_nndist (g x) s),
   { suffices : tendsto (λ i x, inf_nndist (f i x) s) u (𝓝 (λ x, inf_nndist (g x) s)),
@@ -1903,33 +1905,14 @@ begin
   rw [h4s], exact this (measurable_set_singleton 0),
 end
 
-/-- A sequential limit of measurable functions valued in a metric space is measurable. -/
-lemma measurable_of_tendsto_metric {f : ℕ → α → β} {g : α → β}
-  (hf : ∀ i, measurable (f i)) (lim : tendsto f at_top (𝓝 g)) :
-  measurable g :=
-measurable_of_tendsto_metric' at_top hf lim
-
-/-- A limit (over a general filter) of measurable functions valued in a metrizable space is
+/-- A sequential limit of measurable functions valued in a (pseudo) metrizable space is
 measurable. -/
-lemma measurable_of_tendsto_metrizable'
-  {β : Type*} [topological_space β] [metrizable_space β]
-  [measurable_space β] [borel_space β] {ι} {f : ι → α → β} {g : α → β}
-  (u : filter ι) [ne_bot u] [is_countably_generated u]
-  (hf : ∀ i, measurable (f i)) (lim : tendsto f u (𝓝 g)) :
-  measurable g :=
-begin
-  letI : metric_space β := metrizable_space_metric β,
-  exact measurable_of_tendsto_metric' u hf lim
-end
-
-/-- A sequential limit of measurable functions valued in a metrizable space is measurable. -/
-lemma measurable_of_tendsto_metrizable {β : Type*} [topological_space β] [metrizable_space β]
-  [measurable_space β] [borel_space β] {f : ℕ → α → β} {g : α → β}
+lemma measurable_of_tendsto_metrizable {f : ℕ → α → β} {g : α → β}
   (hf : ∀ i, measurable (f i)) (lim : tendsto f at_top (𝓝 g)) :
   measurable g :=
 measurable_of_tendsto_metrizable' at_top hf lim
 
-lemma ae_measurable_of_tendsto_metric_ae {ι : Type*}
+lemma ae_measurable_of_tendsto_metrizable_ae {ι : Type*}
   {μ : measure α} {f : ι → α → β} {g : α → β}
   (u : filter ι) [hu : ne_bot u] [is_countably_generated u]
   (hf : ∀ n, ae_measurable (f n) μ) (h_tendsto : ∀ᵐ x ∂μ, tendsto (λ n, f n x) u (𝓝 (g x))) :
@@ -1941,8 +1924,7 @@ begin
   have hp : ∀ᵐ x ∂μ, p x (λ n, f (v n) x),
     by filter_upwards [h_tendsto] with x hx using hx.comp hv,
   set ae_seq_lim := λ x, ite (x ∈ ae_seq_set h'f p) (g x) (⟨f (v 0) x⟩ : nonempty β).some with hs,
-  refine ⟨ae_seq_lim,
-    measurable_of_tendsto_metric' at_top (@ae_seq.measurable α β _ _ _ (λ n x, f (v n) x) μ h'f p)
+  refine ⟨ae_seq_lim, measurable_of_tendsto_metrizable' at_top (ae_seq.measurable h'f p)
     (tendsto_pi_nhds.mpr (λ x, _)), _⟩,
   { simp_rw [ae_seq, ae_seq_lim],
     split_ifs with hx,
@@ -1953,13 +1935,14 @@ begin
       (ae_seq_set h'f p) (ae_seq.measure_compl_ae_seq_set_eq_zero h'f hp)).symm },
 end
 
-lemma ae_measurable_of_tendsto_metric_ae' {μ : measure α} {f : ℕ → α → β} {g : α → β}
+lemma ae_measurable_of_tendsto_metrizable_ae' {μ : measure α} {f : ℕ → α → β} {g : α → β}
   (hf : ∀ n, ae_measurable (f n) μ)
   (h_ae_tendsto : ∀ᵐ x ∂μ, tendsto (λ n, f n x) at_top (𝓝 (g x))) :
   ae_measurable g μ :=
-ae_measurable_of_tendsto_metric_ae at_top hf h_ae_tendsto
+ae_measurable_of_tendsto_metrizable_ae at_top hf h_ae_tendsto
 
-lemma ae_measurable_of_unif_approx {μ : measure α} {g : α → β}
+lemma ae_measurable_of_unif_approx {β} [measurable_space β] [pseudo_metric_space β] [borel_space β]
+  {μ : measure α} {g : α → β}
   (hf : ∀ ε > (0 : ℝ), ∃ (f : α → β), ae_measurable f μ ∧ ∀ᵐ x ∂μ, dist (f x) (g x) ≤ ε) :
   ae_measurable g μ :=
 begin
@@ -1973,17 +1956,17 @@ begin
     assume x hx,
     rw tendsto_iff_dist_tendsto_zero,
     exact squeeze_zero (λ n, dist_nonneg) hx u_lim },
-  exact ae_measurable_of_tendsto_metric_ae' (λ n, (Hf n).1) this,
+  exact ae_measurable_of_tendsto_metrizable_ae' (λ n, (Hf n).1) this,
 end
 
-lemma measurable_of_tendsto_metric_ae {μ : measure α} [μ.is_complete] {f : ℕ → α → β} {g : α → β}
-  (hf : ∀ n, measurable (f n))
+lemma measurable_of_tendsto_metrizable_ae {μ : measure α} [μ.is_complete] {f : ℕ → α → β}
+  {g : α → β} (hf : ∀ n, measurable (f n))
   (h_ae_tendsto : ∀ᵐ x ∂μ, tendsto (λ n, f n x) at_top (𝓝 (g x))) :
   measurable g :=
 ae_measurable_iff_measurable.mp
-  (ae_measurable_of_tendsto_metric_ae' (λ i, (hf i).ae_measurable) h_ae_tendsto)
+  (ae_measurable_of_tendsto_metrizable_ae' (λ i, (hf i).ae_measurable) h_ae_tendsto)
 
-lemma measurable_limit_of_tendsto_metric_ae {ι} [encodable ι] [nonempty ι] {μ : measure α}
+lemma measurable_limit_of_tendsto_metrizable_ae {ι} [encodable ι] [nonempty ι] {μ : measure α}
   {f : ι → α → β} {L : filter ι} [L.is_countably_generated] (hf : ∀ n, ae_measurable (f n) μ)
   (h_ae_tendsto : ∀ᵐ x ∂μ, ∃ l : β, tendsto (λ n, f n x) L (𝓝 l)) :
   ∃ (f_lim : α → β) (hf_lim_meas : measurable f_lim),
@@ -2011,7 +1994,7 @@ begin
   have h_ae_tendsto_f_lim : ∀ᵐ x ∂μ, tendsto (λ n, f n x) L (𝓝 (f_lim x)),
     from h_ae_eq.mono (λ x hx, (hf_lim x).congr hx),
   have h_f_lim_meas : measurable f_lim,
-    from measurable_of_tendsto_metric' L (ae_seq.measurable hf p)
+    from measurable_of_tendsto_metrizable' L (ae_seq.measurable hf p)
       (tendsto_pi_nhds.mpr (λ x, hf_lim x)),
   exact ⟨f_lim, h_f_lim_meas, h_ae_tendsto_f_lim⟩,
 end

src/measure_theory/function/convergence_in_measure.lean

@@ -268,7 +268,7 @@ lemma tendsto_in_measure.ae_measurable
   ae_measurable g μ :=
 begin
   obtain ⟨ns, hns⟩ := h_tendsto.exists_seq_tendsto_ae',
-  exact ae_measurable_of_tendsto_metric_ae at_top (λ n, hf (ns n)) hns,
+  exact ae_measurable_of_tendsto_metrizable_ae at_top (λ n, hf (ns n)) hns,
 end
 
 end ae_measurable_of

src/measure_theory/function/strongly_measurable.lean

@@ -1363,10 +1363,9 @@ lemma _root_.ae_strongly_measurable_of_tendsto_ae {ι : Type*}
   (lim : ∀ᵐ x ∂μ, tendsto (λ n, f n x) u (𝓝 (g x))) :
   ae_strongly_measurable g μ :=
 begin
-  letI := metrizable_space_metric β,
   borelize β,
   refine ae_strongly_measurable_iff_ae_measurable_separable.2 ⟨_, _⟩,
-  { exact ae_measurable_of_tendsto_metric_ae _ (λ n, (hf n).ae_measurable) lim },
+  { exact ae_measurable_of_tendsto_metrizable_ae _ (λ n, (hf n).ae_measurable) lim },
   { rcases u.exists_seq_tendsto with ⟨v, hv⟩,
     have : ∀ (n : ℕ), ∃ (t : set β), is_separable t ∧ f (v n) ⁻¹' t ∈ μ.ae :=
       λ n, (ae_strongly_measurable_iff_ae_measurable_separable.1 (hf (v n))).2,
@@ -1388,10 +1387,9 @@ lemma _root_.exists_strongly_measurable_limit_of_tendsto_ae [metrizable_space β
     ∀ᵐ x ∂μ, tendsto (λ n, f n x) at_top (𝓝 (f_lim x)) :=
 begin
   borelize β,
-  letI := metrizable_space_metric β,
   obtain ⟨g, g_meas, hg⟩ : ∃ (g : α → β) (g_meas : measurable g),
       ∀ᵐ x ∂μ, tendsto (λ n, f n x) at_top (𝓝 (g x)) :=
-    measurable_limit_of_tendsto_metric_ae (λ n, (hf n).ae_measurable) h_ae_tendsto,
+    measurable_limit_of_tendsto_metrizable_ae (λ n, (hf n).ae_measurable) h_ae_tendsto,
   have Hg : ae_strongly_measurable g μ := ae_strongly_measurable_of_tendsto_ae _ hf hg,
   refine ⟨Hg.mk g, Hg.strongly_measurable_mk, _⟩,
   filter_upwards [hg, Hg.ae_eq_mk] with x hx h'x,
@@ -1674,7 +1672,6 @@ lemma measurable_uncurry_of_continuous_of_measurable {α β ι : Type*} [topolog
   (hu_cont : ∀ x, continuous (λ i, u i x)) (h : ∀ i, measurable (u i)) :
   measurable (function.uncurry u) :=
 begin
-  letI := metrizable_space_metric β,
   obtain ⟨t_sf, ht_sf⟩ : ∃ t : ℕ → simple_func ι ι, ∀ j x,
     tendsto (λ n, u (t n j) x) at_top (𝓝 $ u j x),
   { have h_str_meas : strongly_measurable (id : ι → ι), from strongly_measurable_id,
@@ -1684,7 +1681,7 @@ begin
   have h_tendsto : tendsto U at_top (𝓝 (λ p, u p.fst p.snd)),
   { rw tendsto_pi_nhds,
     exact λ p, ht_sf p.fst p.snd, },
-  refine measurable_of_tendsto_metric (λ n, _) h_tendsto,
+  refine measurable_of_tendsto_metrizable (λ n, _) h_tendsto,
   haveI : encodable (t_sf n).range, from fintype.to_encodable ↥(t_sf n).range,
   have h_meas : measurable (λ (p : (t_sf n).range × α), u ↑p.fst p.snd),
   { have : (λ (p : ↥((t_sf n).range) × α), u ↑(p.fst) p.snd)