feat: define weakly locally compact spaces (#6770)

Mathlib/MeasureTheory/Function/ContinuousMapDense.lean

@@ -137,8 +137,8 @@ theorem exists_continuous_snorm_sub_le_of_closed [μ.OuterRegular] (hp : p ≠ 
 
 /-- In a locally compact space, any function in `ℒp` can be approximated by compactly supported
 continuous functions when `p < ∞`, version in terms of `snorm`. -/
-theorem Memℒp.exists_hasCompactSupport_snorm_sub_le [LocallyCompactSpace α] [μ.Regular] (hp : p ≠ ∞)
-    {f : α → E} (hf : Memℒp f p μ) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
+theorem Memℒp.exists_hasCompactSupport_snorm_sub_le [WeaklyLocallyCompactSpace α] [μ.Regular]
+    (hp : p ≠ ∞) {f : α → E} (hf : Memℒp f p μ) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
     ∃ g : α → E, HasCompactSupport g ∧ snorm (f - g) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p μ := by
   suffices H :
     ∃ g : α → E, snorm (f - g) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p μ ∧ HasCompactSupport g
@@ -191,7 +191,8 @@ theorem Memℒp.exists_hasCompactSupport_snorm_sub_le [LocallyCompactSpace α] [
 
 /-- In a locally compact space, any function in `ℒp` can be approximated by compactly supported
 continuous functions when `0 < p < ∞`, version in terms of `∫`. -/
-theorem Memℒp.exists_hasCompactSupport_integral_rpow_sub_le [LocallyCompactSpace α] [μ.Regular]
+theorem Memℒp.exists_hasCompactSupport_integral_rpow_sub_le
+    [WeaklyLocallyCompactSpace α] [μ.Regular]
     {p : ℝ} (hp : 0 < p) {f : α → E} (hf : Memℒp f (ENNReal.ofReal p) μ) {ε : ℝ} (hε : 0 < ε) :
     ∃ g : α → E,
       HasCompactSupport g ∧
@@ -212,7 +213,8 @@ theorem Memℒp.exists_hasCompactSupport_integral_rpow_sub_le [LocallyCompactSpa
 
 /-- In a locally compact space, any integrable function can be approximated by compactly supported
 continuous functions, version in terms of `∫⁻`. -/
-theorem Integrable.exists_hasCompactSupport_lintegral_sub_le [LocallyCompactSpace α] [μ.Regular]
+theorem Integrable.exists_hasCompactSupport_lintegral_sub_le
+    [WeaklyLocallyCompactSpace α] [μ.Regular]
     {f : α → E} (hf : Integrable f μ) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
     ∃ g : α → E,
       HasCompactSupport g ∧ (∫⁻ x, ‖f x - g x‖₊ ∂μ) ≤ ε ∧ Continuous g ∧ Integrable g μ := by
@@ -222,7 +224,8 @@ theorem Integrable.exists_hasCompactSupport_lintegral_sub_le [LocallyCompactSpac
 
 /-- In a locally compact space, any integrable function can be approximated by compactly supported
 continuous functions, version in terms of `∫`. -/
-theorem Integrable.exists_hasCompactSupport_integral_sub_le [LocallyCompactSpace α] [μ.Regular]
+theorem Integrable.exists_hasCompactSupport_integral_sub_le
+    [WeaklyLocallyCompactSpace α] [μ.Regular]
     {f : α → E} (hf : Integrable f μ) {ε : ℝ} (hε : 0 < ε) :
     ∃ g : α → E, HasCompactSupport g ∧ (∫ x, ‖f x - g x‖ ∂μ) ≤ ε ∧
       Continuous g ∧ Integrable g μ := by

Mathlib/MeasureTheory/Group/Measure.lean

@@ -606,7 +606,7 @@ on open sets has infinite mass. -/
 @[to_additive (attr := simp)
 "In a noncompact locally compact additive group, a left-invariant measure which is positive on open
 sets has infinite mass."]
-theorem measure_univ_of_isMulLeftInvariant [LocallyCompactSpace G] [NoncompactSpace G]
+theorem measure_univ_of_isMulLeftInvariant [WeaklyLocallyCompactSpace G] [NoncompactSpace G]
     (μ : Measure G) [IsOpenPosMeasure μ] [μ.IsMulLeftInvariant] : μ univ = ∞ := by
   /- Consider a closed compact set `K` with nonempty interior. For any compact set `L`, one may
     find `g = g (L)` such that `L` is disjoint from `g • K`. Iterating this, one finds
@@ -703,7 +703,7 @@ instance, to avoid an instance loop.
 
 See Note [lower instance priority]"]
 instance (priority := 100) isLocallyFiniteMeasure_of_isHaarMeasure {G : Type*} [Group G]
-    [MeasurableSpace G] [TopologicalSpace G] [LocallyCompactSpace G] (μ : Measure G)
+    [MeasurableSpace G] [TopologicalSpace G] [WeaklyLocallyCompactSpace G] (μ : Measure G)
     [IsHaarMeasure μ] : IsLocallyFiniteMeasure μ :=
   isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts
 #align measure_theory.measure.is_locally_finite_measure_of_is_haar_measure MeasureTheory.Measure.isLocallyFiniteMeasure_of_isHaarMeasure
@@ -805,7 +805,7 @@ group has no atoms.
 This applies in particular to show that an additive Haar measure on a nontrivial finite-dimensional
 real vector space has no atom."]
 instance (priority := 100) IsHaarMeasure.noAtoms [TopologicalGroup G] [BorelSpace G] [T1Space G]
-    [LocallyCompactSpace G] [(𝓝[≠] (1 : G)).NeBot] (μ : Measure G) [μ.IsHaarMeasure] :
+    [WeaklyLocallyCompactSpace G] [(𝓝[≠] (1 : G)).NeBot] (μ : Measure G) [μ.IsHaarMeasure] :
     NoAtoms μ := by
   cases eq_or_ne (μ 1) 0 with
   | inl h => constructor; simpa

Mathlib/MeasureTheory/Measure/Content.lean

@@ -305,7 +305,8 @@ theorem outerMeasure_preimage (f : G ≃ₜ G) (h : ∀ ⦃K : Compacts G⦄, μ
   convert μ.innerContent_comap f h ⟨s, hs⟩
 #align measure_theory.content.outer_measure_preimage MeasureTheory.Content.outerMeasure_preimage
 
-theorem outerMeasure_lt_top_of_isCompact [LocallyCompactSpace G] {K : Set G} (hK : IsCompact K) :
+theorem outerMeasure_lt_top_of_isCompact [WeaklyLocallyCompactSpace G]
+    {K : Set G} (hK : IsCompact K) :
     μ.outerMeasure K < ∞ := by
   rcases exists_compact_superset hK with ⟨F, h1F, h2F⟩
   calc
@@ -385,7 +386,7 @@ theorem measure_apply {s : Set G} (hs : MeasurableSet s) : μ.measure s = μ.out
 #align measure_theory.content.measure_apply MeasureTheory.Content.measure_apply
 
 /-- In a locally compact space, any measure constructed from a content is regular. -/
-instance regular [LocallyCompactSpace G] : μ.measure.Regular := by
+instance regular [WeaklyLocallyCompactSpace G] : μ.measure.Regular := by
   have : μ.measure.OuterRegular := by
     refine' ⟨fun A hA r (hr : _ < _) => _⟩
     rw [μ.measure_apply hA, outerMeasure_eq_iInf] at hr

Mathlib/MeasureTheory/Measure/MeasureSpace.lean

@@ -3804,7 +3804,7 @@ instance (priority := 100) sigmaFinite_of_locallyFinite [TopologicalSpace α]
 /-- A measure which is finite on compact sets in a locally compact space is locally finite.
 Not registered as an instance to avoid a loop with the other direction. -/
 theorem isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts [TopologicalSpace α]
-    [LocallyCompactSpace α] [IsFiniteMeasureOnCompacts μ] : IsLocallyFiniteMeasure μ :=
+    [WeaklyLocallyCompactSpace α] [IsFiniteMeasureOnCompacts μ] : IsLocallyFiniteMeasure μ :=
   ⟨fun x ↦
     let ⟨K, K_compact, K_mem⟩ := exists_compact_mem_nhds x
     ⟨K, K_mem, K_compact.measure_lt_top⟩⟩

Mathlib/Topology/Algebra/Group/Basic.lean

@@ -1668,14 +1668,13 @@ theorem compact_covered_by_mul_left_translates {K V : Set G} (hK : IsCompact K)
 #align compact_covered_by_mul_left_translates compact_covered_by_mul_left_translates
 #align compact_covered_by_add_left_translates compact_covered_by_add_left_translates
 
-/-- Every locally compact separable topological group is σ-compact.
+/-- Every weakly locally compact separable topological group is σ-compact.
   Note: this is not true if we drop the topological group hypothesis. -/
-@[to_additive SeparableLocallyCompactAddGroup.sigmaCompactSpace
-  "Every locally
-  compact separable topological group is σ-compact.
+@[to_additive SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace
+  "Every weakly locally compact separable topological additive group is σ-compact.
   Note: this is not true if we drop the topological group hypothesis."]
-instance (priority := 100) SeparableLocallyCompactGroup.sigmaCompactSpace [SeparableSpace G]
-    [LocallyCompactSpace G] : SigmaCompactSpace G := by
+instance (priority := 100) SeparableWeaklyLocallyCompactGroup.sigmaCompactSpace [SeparableSpace G]
+    [WeaklyLocallyCompactSpace G] : SigmaCompactSpace G := by
   obtain ⟨L, hLc, hL1⟩ := exists_compact_mem_nhds (1 : G)
   refine' ⟨⟨fun n => (fun x => x * denseSeq G n) ⁻¹' L, _, _⟩⟩
   · intro n
@@ -1686,8 +1685,8 @@ instance (priority := 100) SeparableLocallyCompactGroup.sigmaCompactSpace [Separ
       exact (denseRange_denseSeq G).inter_nhds_nonempty
           ((Homeomorph.mulLeft x).continuous.continuousAt <| hL1)
     exact ⟨n, hn⟩
-#align separable_locally_compact_group.sigma_compact_space SeparableLocallyCompactGroup.sigmaCompactSpace
-#align separable_locally_compact_add_group.sigma_compact_space SeparableLocallyCompactAddGroup.sigmaCompactSpace
+#align separable_locally_compact_group.sigma_compact_space SeparableWeaklyLocallyCompactGroup.sigmaCompactSpace
+#align separable_locally_compact_add_group.sigma_compact_space SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace
 
 /-- Given two compact sets in a noncompact topological group, there is a translate of the second
 one that is disjoint from the first one. -/
@@ -1744,7 +1743,7 @@ theorem local_isCompact_isClosed_nhds_of_group [LocallyCompactSpace G] {U : Set
 variable (G)
 
 @[to_additive]
-theorem exists_isCompact_isClosed_nhds_one [LocallyCompactSpace G] :
+theorem exists_isCompact_isClosed_nhds_one [WeaklyLocallyCompactSpace G] :
     ∃ K : Set G, IsCompact K ∧ IsClosed K ∧ K ∈ 𝓝 1 :=
   let ⟨_L, Lcomp, L1⟩ := exists_compact_mem_nhds (1 : G)
   let ⟨K, Kcl, Kcomp, _, K1⟩ := exists_isCompact_isClosed_subset_isCompact_nhds_one Lcomp L1

Mathlib/Topology/Algebra/Group/Compact.lean

@@ -30,25 +30,27 @@ section
 
 variable [TopologicalSpace G] [Group G] [TopologicalGroup G]
 
+/-- Every topological group in which there exists a compact set with nonempty interior
+is weakly locally compact. -/
+@[to_additive
+  "Every separated topological additive group
+  in which there exists a compact set with nonempty interior is weakly locally compact."]
+theorem TopologicalSpace.PositiveCompacts.weaklyLocallyCompactSpace_of_group
+    (K : PositiveCompacts G) : WeaklyLocallyCompactSpace G where
+  exists_compact_mem_nhds x := by
+    obtain ⟨y, hy⟩ := K.interior_nonempty
+    refine ⟨(x * y⁻¹) • (K : Set G), K.isCompact.smul _, ?_⟩
+    rw [mem_interior_iff_mem_nhds] at hy
+    simpa using smul_mem_nhds (x * y⁻¹) hy
+
 /-- Every separated topological group in which there exists a compact set with nonempty interior
 is locally compact. -/
 @[to_additive
-      "Every separated topological group in which there exists a compact set with nonempty
-      interior is locally compact."]
+  "Every separated topological additive group
+  in which there exists a compact set with nonempty interior is locally compact."]
 theorem TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_group [T2Space G]
-    (K : PositiveCompacts G) : LocallyCompactSpace G := by
-  refine' locally_compact_of_compact_nhds fun x => _
-  obtain ⟨y, hy⟩ := K.interior_nonempty
-  let F := Homeomorph.mulLeft (x * y⁻¹)
-  refine' ⟨F '' K, _, K.isCompact.image F.continuous⟩
-  suffices F.symm ⁻¹' K ∈ 𝓝 x by
-    convert this using 1
-    apply Equiv.image_eq_preimage
-  apply ContinuousAt.preimage_mem_nhds F.symm.continuous.continuousAt
-  have : F.symm x = y := by simp only [Homeomorph.mulLeft_symm, mul_inv_rev,
-      inv_inv, Homeomorph.coe_mulLeft, inv_mul_cancel_right]
-  rw [this]
-  exact mem_interior_iff_mem_nhds.1 hy
+    (K : PositiveCompacts G) : LocallyCompactSpace G :=
+  have := K.weaklyLocallyCompactSpace_of_group; inferInstance
 #align topological_space.positive_compacts.locally_compact_space_of_group TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_group
 #align topological_space.positive_compacts.locally_compact_space_of_add_group TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_addGroup
 
@@ -59,8 +61,7 @@ section Quotient
 variable [Group G] [TopologicalSpace G] [TopologicalGroup G] {Γ : Subgroup G}
 
 @[to_additive]
-instance QuotientGroup.continuousSMul [LocallyCompactSpace G] : ContinuousSMul G (G ⧸ Γ)
-    where
+instance QuotientGroup.continuousSMul [LocallyCompactSpace G] : ContinuousSMul G (G ⧸ Γ) where
   continuous_smul := by
     let F : G × G ⧸ Γ → G ⧸ Γ := fun p => p.1 • p.2
     change Continuous F

Mathlib/Topology/CompactOpen.lean

@@ -292,7 +292,7 @@ theorem tendsto_compactOpen_iff_forall {ι : Type*} {l : Filter ι} (F : ι →
 
 /-- A family `F` of functions in `C(α, β)` converges in the compact-open topology, if and only if
 it converges in the compact-open topology on each compact subset of `α`. -/
-theorem exists_tendsto_compactOpen_iff_forall [LocallyCompactSpace α] [T2Space β]
+theorem exists_tendsto_compactOpen_iff_forall [WeaklyLocallyCompactSpace α] [T2Space β]
     {ι : Type*} {l : Filter ι} [Filter.NeBot l] (F : ι → C(α, β)) :
     (∃ f, Filter.Tendsto F l (𝓝 f)) ↔
     ∀ (s : Set α) (hs : IsCompact s), ∃ f, Filter.Tendsto (fun i => (F i).restrict s) l (𝓝 f) := by

Mathlib/Topology/DiscreteSubset.lean

@@ -36,7 +36,7 @@ lemma tendsto_cofinite_cocompact_iff :
   refine' forall₂_congr (fun K _ ↦ _)
   simp only [mem_compl_iff, eventually_cofinite, not_not, preimage]
 
-lemma Continuous.discrete_of_tendsto_cofinite_cocompact [T1Space X] [LocallyCompactSpace Y]
+lemma Continuous.discrete_of_tendsto_cofinite_cocompact [T1Space X] [WeaklyLocallyCompactSpace Y]
     (hf' : Continuous f) (hf : Tendsto f cofinite (cocompact _)) :
     DiscreteTopology X := by
   refine' singletons_open_iff_discrete.mp (fun x ↦ _)
@@ -57,7 +57,7 @@ lemma IsClosed.tendsto_coe_cofinite_of_discreteTopology
     Tendsto ((↑) : s → X) cofinite (cocompact _) :=
   tendsto_cofinite_cocompact_of_discrete hs.closedEmbedding_subtype_val.tendsto_cocompact
 
-lemma IsClosed.tendsto_coe_cofinite_iff [T1Space X] [LocallyCompactSpace X]
+lemma IsClosed.tendsto_coe_cofinite_iff [T1Space X] [WeaklyLocallyCompactSpace X]
     {s : Set X} (hs : IsClosed s) :
     Tendsto ((↑) : s → X) cofinite (cocompact _) ↔ DiscreteTopology s :=
   ⟨continuous_subtype_val.discrete_of_tendsto_cofinite_cocompact,

Mathlib/Topology/MetricSpace/Baire.lean

@@ -48,8 +48,8 @@ class BaireSpace (α : Type*) [TopologicalSpace α] : Prop where
 
 /-- Baire theorems asserts that various topological spaces have the Baire property.
 Two versions of these theorems are given.
-The first states that complete pseudo_emetric spaces are Baire. -/
-instance (priority := 100) baire_category_theorem_emetric_complete [PseudoEMetricSpace α]
+The first states that complete `PseudoEMetricSpace`s are Baire. -/
+instance (priority := 100) BaireSpace.of_pseudoEMetricSpace_completeSpace [PseudoEMetricSpace α]
     [CompleteSpace α] : BaireSpace α := by
   refine' ⟨fun f ho hd => _⟩
   let B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
@@ -143,11 +143,11 @@ instance (priority := 100) baire_category_theorem_emetric_complete [PseudoEMetri
     exact this (yball (n + 1))
   show edist y x ≤ ε
   exact le_trans (yball 0) (min_le_left _ _)
-#align baire_category_theorem_emetric_complete baire_category_theorem_emetric_complete
+#align baire_category_theorem_emetric_complete BaireSpace.of_pseudoEMetricSpace_completeSpace
 
 /-- The second theorem states that locally compact spaces are Baire. -/
-instance (priority := 100) baire_category_theorem_locally_compact [TopologicalSpace α] [T2Space α]
-    [LocallyCompactSpace α] : BaireSpace α := by
+instance (priority := 100) BaireSpace.of_t2Space_locallyCompactSpace
+    [TopologicalSpace α] [T2Space α] [LocallyCompactSpace α] : BaireSpace α := by
   constructor
   intro f ho hd
   /- To prove that an intersection of open dense subsets is dense, prove that its intersection
@@ -182,7 +182,7 @@ instance (priority := 100) baire_category_theorem_locally_compact [TopologicalSp
       (fun n => (hK_decreasing n).trans (inter_subset_right _ _)) (fun n => (K n).nonempty)
       (K 0).isCompact fun n => (K n).isCompact.isClosed
   exact hK_nonempty.mono hK_subset
-#align baire_category_theorem_locally_compact baire_category_theorem_locally_compact
+#align baire_category_theorem_locally_compact BaireSpace.of_t2Space_locallyCompactSpace
 
 variable [TopologicalSpace α] [BaireSpace α]
 

Mathlib/Topology/Paracompact.lean

@@ -193,7 +193,7 @@ dealing with a covering of the whole space.
 
 In most cases (namely, if `B c r ∪ B c r'` is again a set of the form `B c r''`) it is possible
 to choose `α = X`. This fact is not yet formalized in `mathlib`. -/
-theorem refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set [LocallyCompactSpace X]
+theorem refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set [WeaklyLocallyCompactSpace X]
     [SigmaCompactSpace X] [T2Space X] {ι : X → Type u} {p : ∀ x, ι x → Prop} {B : ∀ x, ι x → Set X}
     {s : Set X} (hs : IsClosed s) (hB : ∀ x ∈ s, (𝓝 x).HasBasis (p x) (B x)) :
     ∃ (α : Type v) (c : α → X) (r : ∀ a, ι (c a)),
@@ -263,7 +263,7 @@ dealing with a covering of a closed set.
 
 In most cases (namely, if `B c r ∪ B c r'` is again a set of the form `B c r''`) it is possible
 to choose `α = X`. This fact is not yet formalized in `mathlib`. -/
-theorem refinement_of_locallyCompact_sigmaCompact_of_nhds_basis [LocallyCompactSpace X]
+theorem refinement_of_locallyCompact_sigmaCompact_of_nhds_basis [WeaklyLocallyCompactSpace X]
     [SigmaCompactSpace X] [T2Space X] {ι : X → Type u} {p : ∀ x, ι x → Prop} {B : ∀ x, ι x → Set X}
     (hB : ∀ x, (𝓝 x).HasBasis (p x) (B x)) :
     ∃ (α : Type v) (c : α → X) (r : ∀ a, ι (c a)),
@@ -276,7 +276,7 @@ theorem refinement_of_locallyCompact_sigmaCompact_of_nhds_basis [LocallyCompactS
 -- See note [lower instance priority]
 /-- A locally compact sigma compact Hausdorff space is paracompact. See also
 `refinement_of_locallyCompact_sigmaCompact_of_nhds_basis` for a more precise statement. -/
-instance (priority := 100) paracompact_of_locallyCompact_sigmaCompact [LocallyCompactSpace X]
+instance (priority := 100) paracompact_of_locallyCompact_sigmaCompact [WeaklyLocallyCompactSpace X]
     [SigmaCompactSpace X] [T2Space X] : ParacompactSpace X := by
   refine' ⟨fun α s ho hc ↦ _⟩
   choose i hi using iUnion_eq_univ_iff.1 hc

Mathlib/Topology/ProperMap.lean

@@ -246,7 +246,7 @@ theorem Continuous.isProperMap [CompactSpace X] [T2Space Y] (hf : Continuous f)
 
 /-- If `Y` is locally compact and Hausdorff, then proper maps `X → Y` are exactly continuous maps
 such that the preimage of any compact set is compact. -/
-theorem isProperMap_iff_isCompact_preimage [T2Space Y] [LocallyCompactSpace Y] :
+theorem isProperMap_iff_isCompact_preimage [T2Space Y] [WeaklyLocallyCompactSpace Y] :
     IsProperMap f ↔ Continuous f ∧ ∀ ⦃K⦄, IsCompact K → IsCompact (f ⁻¹' K) := by
   constructor <;> intro H
   -- The direct implication follows from the previous results
@@ -265,7 +265,7 @@ theorem isProperMap_iff_isCompact_preimage [T2Space Y] [LocallyCompactSpace Y] :
     exact ⟨x, hx⟩
 
 /-- Version of `isProperMap_iff_isCompact_preimage` in terms of `cocompact`. -/
-lemma isProperMap_iff_tendsto_cocompact [T2Space Y] [LocallyCompactSpace Y] :
+lemma isProperMap_iff_tendsto_cocompact [T2Space Y] [WeaklyLocallyCompactSpace Y] :
     IsProperMap f ↔ Continuous f ∧ Tendsto f (cocompact X) (cocompact Y) := by
   simp_rw [isProperMap_iff_isCompact_preimage, hasBasis_cocompact.tendsto_right_iff,
     ← mem_preimage, eventually_mem_set, preimage_compl]