chore(ProperSpace): rename constructors (#10138)

Rename `properSpace_of_*` to `ProperSpace.of_*`,
restore old names as deprecated aliases.
This affects:

- `properSpace_of_locallyCompactSpace` -> `ProperSpace.of_locallyCompactSpace`,
  also golf using new `ProperSpace.of_seq_closedBall`;
- `properSpace_of_locallyCompact_module` -> `ProperSpace.of_locallyCompact_module`;
- `properSpace_of_compact_closedBall_of_le` ->
  `ProperSpace.of_isCompact_closedBall_of_le`,
  also changed `compact` -> `isCompact` in the name.

Author: urkud

Mathlib/Analysis/Calculus/FDeriv/Measurable.lean

@@ -849,7 +849,7 @@ open Uniformity
 
 lemma isOpen_A_with_param {r s : ℝ} (hf : Continuous f.uncurry) (L : E →L[𝕜] F) :
     IsOpen {p : α × E | p.2 ∈ A (f p.1) L r s} := by
-  have : ProperSpace E := properSpace_of_locallyCompactSpace 𝕜
+  have : ProperSpace E := .of_locallyCompactSpace 𝕜
   simp only [A, half_lt_self_iff, not_lt, mem_Ioc, mem_ball, map_sub, mem_setOf_eq]
   apply isOpen_iff_mem_nhds.2
   rintro ⟨a, x⟩ ⟨r', ⟨Irr', Ir'r⟩, hr⟩
@@ -945,7 +945,7 @@ theorem measurableSet_of_differentiableAt_of_isComplete_with_param
   refine MeasurableSet.iInter (fun _ ↦ ?_)
   refine MeasurableSet.iInter (fun _ ↦ ?_)
   refine MeasurableSet.iInter (fun _ ↦ ?_)
-  have : ProperSpace E := properSpace_of_locallyCompactSpace 𝕜
+  have : ProperSpace E := .of_locallyCompactSpace 𝕜
   exact (isOpen_B_with_param hf K).measurableSet
 
 variable (𝕜)
@@ -991,7 +991,7 @@ theorem stronglyMeasurable_deriv_with_param [LocallyCompactSpace 𝕜] [Measurab
     StronglyMeasurable (fun (p : α × 𝕜) ↦ deriv (f p.1) p.2) := by
   borelize F
   rcases h.out with hα|hF
-  · have : ProperSpace 𝕜 := properSpace_of_locallyCompactSpace 𝕜
+  · have : ProperSpace 𝕜 := .of_locallyCompactSpace 𝕜
     apply stronglyMeasurable_iff_measurable_separable.2 ⟨measurable_deriv_with_param hf, ?_⟩
     have : range (fun (p : α × 𝕜) ↦ deriv (f p.1) p.2)
         ⊆ closure (Submodule.span 𝕜 (range f.uncurry)) := by

Mathlib/Analysis/NormedSpace/FiniteDimension.lean

@@ -8,6 +8,7 @@ import Mathlib.Analysis.NormedSpace.AddTorsor
 import Mathlib.Analysis.NormedSpace.AffineIsometry
 import Mathlib.Analysis.NormedSpace.OperatorNorm
 import Mathlib.Analysis.NormedSpace.RieszLemma
+import Mathlib.Analysis.NormedSpace.Pointwise
 import Mathlib.Topology.Algebra.Module.FiniteDimension
 import Mathlib.Topology.Algebra.InfiniteSum.Module
 import Mathlib.Topology.Instances.Matrix
@@ -494,39 +495,33 @@ theorem HasCompactMulSupport.eq_one_or_finiteDimensional {X : Type*} [Topologica
 #align has_compact_support.eq_zero_or_finite_dimensional HasCompactSupport.eq_zero_or_finiteDimensional
 
 /-- A locally compact normed vector space is proper. -/
-lemma properSpace_of_locallyCompactSpace (𝕜 : Type*) [NontriviallyNormedField 𝕜]
-    {E : Type*} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
-    [LocallyCompactSpace E] : ProperSpace E := by
+lemma ProperSpace.of_locallyCompactSpace (𝕜 : Type*) [NontriviallyNormedField 𝕜]
+    {E : Type*} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [LocallyCompactSpace E] :
+    ProperSpace E := by
   rcases exists_isCompact_closedBall (0 : E) with ⟨r, rpos, hr⟩
   rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩
-  have M : ∀ n (x : E), IsCompact (closedBall x (‖c‖^n * r)) := by
-    intro n x
-    let f : E → E := fun y ↦ c^n • y + x
-    have Cf : Continuous f := (continuous_id.const_smul _).add continuous_const
-    have A : closedBall x (‖c‖^n * r) ⊆ f '' (closedBall 0 r) := by
-      rintro y hy
-      refine ⟨(c^n)⁻¹ • (y - x), ?_, ?_⟩
-      · simpa [dist_eq_norm, norm_smul, inv_mul_le_iff (pow_pos (zero_lt_one.trans hc) _)] using hy
-      · have : c^n ≠ 0 := pow_ne_zero _ (norm_pos_iff.1 (zero_lt_one.trans hc))
-        simp [smul_smul, mul_inv_cancel this]
-    exact (hr.image Cf).of_isClosed_subset isClosed_ball A
-  refine ⟨fun x s ↦ ?_⟩
-  have L : ∀ᶠ n in (atTop : Filter ℕ), s ≤ ‖c‖^n * r := by
-    have : Tendsto (fun n ↦ ‖c‖^n * r) atTop atTop :=
-      Tendsto.atTop_mul_const rpos (tendsto_pow_atTop_atTop_of_one_lt hc)
-    exact Tendsto.eventually_ge_atTop this s
-  rcases L.exists with ⟨n, hn⟩
-  exact (M n x).of_isClosed_subset isClosed_ball (closedBall_subset_closedBall hn)
+  have hC : ∀ n, IsCompact (closedBall (0 : E) (‖c‖^n * r)) := fun n ↦ by
+    have : c ^ n ≠ 0 := pow_ne_zero _ <| fun h ↦ by simp [h, zero_le_one.not_lt] at hc
+    simpa [_root_.smul_closedBall' this] using hr.smul (c ^ n)
+  have hTop : Tendsto (fun n ↦ ‖c‖^n * r) atTop atTop :=
+    Tendsto.atTop_mul_const rpos (tendsto_pow_atTop_atTop_of_one_lt hc)
+  exact .of_seq_closedBall hTop (eventually_of_forall hC)
+
+@[deprecated] -- Since 2024/01/31
+alias properSpace_of_locallyCompactSpace := ProperSpace.of_locallyCompactSpace
 
 variable (E)
-lemma properSpace_of_locallyCompact_module [Nontrivial E] [LocallyCompactSpace E] :
-    ProperSpace 𝕜 := by
+lemma ProperSpace.of_locallyCompact_module [Nontrivial E] [LocallyCompactSpace E] :
+    ProperSpace 𝕜 :=
   have : LocallyCompactSpace 𝕜 := by
     obtain ⟨v, hv⟩ : ∃ v : E, v ≠ 0 := exists_ne 0
     let L : 𝕜 → E := fun t ↦ t • v
     have : ClosedEmbedding L := closedEmbedding_smul_left hv
     apply ClosedEmbedding.locallyCompactSpace this
-  exact properSpace_of_locallyCompactSpace 𝕜
+  .of_locallyCompactSpace 𝕜
+
+@[deprecated] -- Since 2024/01/31
+alias properSpace_of_locallyCompact_module := ProperSpace.of_locallyCompact_module
 
 end Riesz
 
@@ -589,7 +584,7 @@ We do not register this as an instance to avoid an instance loop when trying to
 properness of `𝕜`, and the search for `𝕜` as an unknown metavariable. Declare the instance
 explicitly when needed. -/
 theorem FiniteDimensional.proper [FiniteDimensional 𝕜 E] : ProperSpace E := by
-  have : ProperSpace 𝕜 := properSpace_of_locallyCompactSpace 𝕜
+  have : ProperSpace 𝕜 := .of_locallyCompactSpace 𝕜
   set e := ContinuousLinearEquiv.ofFinrankEq (@finrank_fin_fun 𝕜 _ _ (finrank 𝕜 E)).symm
   exact e.symm.antilipschitz.properSpace e.symm.continuous e.symm.surjective
 #align finite_dimensional.proper FiniteDimensional.proper
@@ -609,7 +604,7 @@ instance {𝕜 E : Type*} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
     [NormedAddCommGroup E] [NormedSpace 𝕜 E] [LocallyCompactSpace E] (S : Submodule 𝕜 E) :
     ProperSpace S := by
   nontriviality E
-  have : ProperSpace 𝕜 := properSpace_of_locallyCompact_module 𝕜 E
+  have : ProperSpace 𝕜 := .of_locallyCompact_module 𝕜 E
   have : FiniteDimensional 𝕜 E := finiteDimensional_of_locallyCompactSpace 𝕜
   exact FiniteDimensional.proper 𝕜 S
 

Mathlib/MeasureTheory/Measure/Haar/Disintegration.lean

@@ -47,13 +47,13 @@ theorem LinearMap.exists_map_addHaar_eq_smul_addHaar' (h : Function.Surjective L
   is also true for linear equivalences, as they map Haar measure to Haar measure. The general case
   follows from these two and linear algebra, as `L` can be interpreted as the composition of the
   projection `P` on a complement `T` to its kernel `S`, together with a linear equivalence. -/
-  have : ProperSpace E := properSpace_of_locallyCompactSpace 𝕜
+  have : ProperSpace E := .of_locallyCompactSpace 𝕜
   have : FiniteDimensional 𝕜 E := finiteDimensional_of_locallyCompactSpace 𝕜
   have : ProperSpace F := by
     rcases subsingleton_or_nontrivial E with hE|hE
     · have : Subsingleton F := Function.Surjective.subsingleton h
       infer_instance
-    · have : ProperSpace 𝕜 := properSpace_of_locallyCompact_module 𝕜 E
+    · have : ProperSpace 𝕜 := .of_locallyCompact_module 𝕜 E
       have : FiniteDimensional 𝕜 F := Module.Finite.of_surjective L h
       exact FiniteDimensional.proper 𝕜 F
   let S : Submodule 𝕜 E := LinearMap.ker L
@@ -129,8 +129,8 @@ lemma ae_ae_add_linearMap_mem_iff [LocallyCompactSpace F] {s : Set F} (hs : Meas
     (∀ᵐ y ∂ν, ∀ᵐ x ∂μ, y + L x ∈ s) ↔ ∀ᵐ y ∂ν, y ∈ s := by
   have : FiniteDimensional 𝕜 E := finiteDimensional_of_locallyCompactSpace 𝕜
   have : FiniteDimensional 𝕜 F := finiteDimensional_of_locallyCompactSpace 𝕜
-  have : ProperSpace E := properSpace_of_locallyCompactSpace 𝕜
-  have : ProperSpace F := properSpace_of_locallyCompactSpace 𝕜
+  have : ProperSpace E := .of_locallyCompactSpace 𝕜
+  have : ProperSpace F := .of_locallyCompactSpace 𝕜
   let M : F × E →ₗ[𝕜] F := LinearMap.id.coprod L
   have M_cont : Continuous M := M.continuous_of_finiteDimensional
   have hM : Function.Surjective M := by simp [← LinearMap.range_eq_top, LinearMap.range_coprod]

Mathlib/Topology/MetricSpace/ProperSpace.lean

@@ -62,11 +62,23 @@ instance (priority := 100) secondCountable_of_proper [ProperSpace α] :
 
 /-- If all closed balls of large enough radius are compact, then the space is proper. Especially
 useful when the lower bound for the radius is 0. -/
-theorem properSpace_of_compact_closedBall_of_le (R : ℝ)
+theorem ProperSpace.of_isCompact_closedBall_of_le (R : ℝ)
     (h : ∀ x : α, ∀ r, R ≤ r → IsCompact (closedBall x r)) : ProperSpace α :=
   ⟨fun x r => IsCompact.of_isClosed_subset (h x (max r R) (le_max_right _ _)) isClosed_ball
     (closedBall_subset_closedBall <| le_max_left _ _)⟩
-#align proper_space_of_compact_closed_ball_of_le properSpace_of_compact_closedBall_of_le
+#align proper_space_of_compact_closed_ball_of_le ProperSpace.of_isCompact_closedBall_of_le
+
+@[deprecated] -- Since 2024/01/31
+alias properSpace_of_compact_closedBall_of_le := ProperSpace.of_isCompact_closedBall_of_le
+
+/-- If there exists a sequence of compact closed balls with the same center
+such that the radii tend to infinity, then the space is proper. -/
+theorem ProperSpace.of_seq_closedBall {β : Type*} {l : Filter β} [NeBot l] {x : α} {r : β → ℝ}
+    (hr : Tendsto r l atTop) (hc : ∀ᶠ i in l, IsCompact (closedBall x (r i))) :
+    ProperSpace α where
+  isCompact_closedBall a r :=
+    let ⟨_i, hci, hir⟩ := (hc.and <| hr.eventually_ge_atTop <| r + dist a x).exists
+    hci.of_isClosed_subset isClosed_ball <| closedBall_subset_closedBall' hir
 
 -- A compact pseudometric space is proper
 -- see Note [lower instance priority]
@@ -109,7 +121,7 @@ instance prod_properSpace {α : Type*} {β : Type*} [PseudoMetricSpace α] [Pseu
 /-- A finite product of proper spaces is proper. -/
 instance pi_properSpace {π : β → Type*} [Fintype β] [∀ b, PseudoMetricSpace (π b)]
     [h : ∀ b, ProperSpace (π b)] : ProperSpace (∀ b, π b) := by
-  refine' properSpace_of_compact_closedBall_of_le 0 fun x r hr => _
+  refine .of_isCompact_closedBall_of_le 0 fun x r hr => ?_
   rw [closedBall_pi _ hr]
   exact isCompact_univ_pi fun _ => isCompact_closedBall _ _
 #align pi_proper_space pi_properSpace