Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
chore(MetricSpace/PseudoMetric): split out proper spaces (#9812)
And move one lemma to a better place. Shaves off another 130 lines from a 2200 line file; #9815 continues with a more far-reaching split. Co-authored-by: grunweg <grunweg@posteo.de>
- Loading branch information
Showing
4 changed files
with
161 additions
and
136 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,153 @@ | ||
| /- | ||
| Copyright (c) 2018 Sébastien Gouëzel. All rights reserved. | ||
| Released under Apache 2.0 license as described in the file LICENSE. | ||
| Authors: Sébastien Gouëzel | ||
| -/ | ||
| import Mathlib.Topology.MetricSpace.PseudoMetric | ||
|
|
||
| /-! ## Proper spaces | ||
| ## Main definitions and results | ||
| * `ProperSpace α`: a `PseudoMetricSpace` where all closed balls are compact | ||
| * `isCompact_sphere`: any sphere in a proper space is compact. | ||
| * `proper_of_compact`: compact spaces are proper. | ||
| * `secondCountable_of_proper`: proper spaces are sigma-compact, hence second countable. | ||
| * `locally_compact_of_proper`: proper spaces are locally compact. | ||
| * `pi_properSpace`: finite products of proper spaces are proper. | ||
| -/ | ||
|
|
||
| open Set Filter | ||
|
|
||
| universe u v w | ||
|
|
||
| variable {α : Type u} {β : Type v} {X ι : Type*} | ||
|
|
||
| section ProperSpace | ||
|
|
||
| open Metric | ||
|
|
||
| /-- A pseudometric space is proper if all closed balls are compact. -/ | ||
| class ProperSpace (α : Type u) [PseudoMetricSpace α] : Prop where | ||
| isCompact_closedBall : ∀ x : α, ∀ r, IsCompact (closedBall x r) | ||
| #align proper_space ProperSpace | ||
|
|
||
| export ProperSpace (isCompact_closedBall) | ||
|
|
||
| /-- In a proper pseudometric space, all spheres are compact. -/ | ||
| theorem isCompact_sphere {α : Type*} [PseudoMetricSpace α] [ProperSpace α] (x : α) (r : ℝ) : | ||
| IsCompact (sphere x r) := | ||
| (isCompact_closedBall x r).of_isClosed_subset isClosed_sphere sphere_subset_closedBall | ||
| #align is_compact_sphere isCompact_sphere | ||
|
|
||
| /-- In a proper pseudometric space, any sphere is a `CompactSpace` when considered as a subtype. -/ | ||
| instance Metric.sphere.compactSpace {α : Type*} [PseudoMetricSpace α] [ProperSpace α] | ||
| (x : α) (r : ℝ) : CompactSpace (sphere x r) := | ||
| isCompact_iff_compactSpace.mp (isCompact_sphere _ _) | ||
|
|
||
| variable [PseudoMetricSpace α] | ||
|
|
||
| -- see Note [lower instance priority] | ||
| /-- A proper pseudo metric space is sigma compact, and therefore second countable. -/ | ||
| instance (priority := 100) secondCountable_of_proper [ProperSpace α] : | ||
| SecondCountableTopology α := by | ||
| -- We already have `sigmaCompactSpace_of_locallyCompact_secondCountable`, so we don't | ||
| -- add an instance for `SigmaCompactSpace`. | ||
| suffices SigmaCompactSpace α from EMetric.secondCountable_of_sigmaCompact α | ||
| rcases em (Nonempty α) with (⟨⟨x⟩⟩ | hn) | ||
| · exact ⟨⟨fun n => closedBall x n, fun n => isCompact_closedBall _ _, iUnion_closedBall_nat _⟩⟩ | ||
| · exact ⟨⟨fun _ => ∅, fun _ => isCompact_empty, iUnion_eq_univ_iff.2 fun x => (hn ⟨x⟩).elim⟩⟩ | ||
| #align second_countable_of_proper secondCountable_of_proper | ||
|
|
||
| /-- 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 : ℝ) | ||
| (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 | ||
|
|
||
| -- A compact pseudometric space is proper | ||
| -- see Note [lower instance priority] | ||
| instance (priority := 100) proper_of_compact [CompactSpace α] : ProperSpace α := | ||
| ⟨fun _ _ => isClosed_ball.isCompact⟩ | ||
| #align proper_of_compact proper_of_compact | ||
|
|
||
| -- see Note [lower instance priority] | ||
| /-- A proper space is locally compact -/ | ||
| instance (priority := 100) locally_compact_of_proper [ProperSpace α] : LocallyCompactSpace α := | ||
| .of_hasBasis (fun _ => nhds_basis_closedBall) fun _ _ _ => | ||
| isCompact_closedBall _ _ | ||
| #align locally_compact_of_proper locally_compact_of_proper | ||
|
|
||
| -- see Note [lower instance priority] | ||
| /-- A proper space is complete -/ | ||
| instance (priority := 100) complete_of_proper [ProperSpace α] : CompleteSpace α := | ||
| ⟨fun {f} hf => by | ||
| /- We want to show that the Cauchy filter `f` is converging. It suffices to find a closed | ||
| ball (therefore compact by properness) where it is nontrivial. -/ | ||
| obtain ⟨t, t_fset, ht⟩ : ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, dist x y < 1 := | ||
| (Metric.cauchy_iff.1 hf).2 1 zero_lt_one | ||
| rcases hf.1.nonempty_of_mem t_fset with ⟨x, xt⟩ | ||
| have : closedBall x 1 ∈ f := mem_of_superset t_fset fun y yt => (ht y yt x xt).le | ||
| rcases (isCompact_iff_totallyBounded_isComplete.1 (isCompact_closedBall x 1)).2 f hf | ||
| (le_principal_iff.2 this) with | ||
| ⟨y, -, hy⟩ | ||
| exact ⟨y, hy⟩⟩ | ||
| #align complete_of_proper complete_of_proper | ||
|
|
||
| /-- A binary product of proper spaces is proper. -/ | ||
| instance prod_properSpace {α : Type*} {β : Type*} [PseudoMetricSpace α] [PseudoMetricSpace β] | ||
| [ProperSpace α] [ProperSpace β] : ProperSpace (α × β) where | ||
| isCompact_closedBall := by | ||
| rintro ⟨x, y⟩ r | ||
| rw [← closedBall_prod_same x y] | ||
| exact (isCompact_closedBall x r).prod (isCompact_closedBall y r) | ||
| #align prod_proper_space prod_properSpace | ||
|
|
||
| /-- 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 => _ | ||
| rw [closedBall_pi _ hr] | ||
| exact isCompact_univ_pi fun _ => isCompact_closedBall _ _ | ||
| #align pi_proper_space pi_properSpace | ||
|
|
||
| variable [ProperSpace α] {x : α} {r : ℝ} {s : Set α} | ||
|
|
||
| /-- If a nonempty ball in a proper space includes a closed set `s`, then there exists a nonempty | ||
| ball with the same center and a strictly smaller radius that includes `s`. -/ | ||
| theorem exists_pos_lt_subset_ball (hr : 0 < r) (hs : IsClosed s) (h : s ⊆ ball x r) : | ||
| ∃ r' ∈ Ioo 0 r, s ⊆ ball x r' := by | ||
| rcases eq_empty_or_nonempty s with (rfl | hne) | ||
| · exact ⟨r / 2, ⟨half_pos hr, half_lt_self hr⟩, empty_subset _⟩ | ||
| have : IsCompact s := | ||
| (isCompact_closedBall x r).of_isClosed_subset hs (h.trans ball_subset_closedBall) | ||
| obtain ⟨y, hys, hy⟩ : ∃ y ∈ s, s ⊆ closedBall x (dist y x) := | ||
| this.exists_forall_ge hne (continuous_id.dist continuous_const).continuousOn | ||
| have hyr : dist y x < r := h hys | ||
| rcases exists_between hyr with ⟨r', hyr', hrr'⟩ | ||
| exact ⟨r', ⟨dist_nonneg.trans_lt hyr', hrr'⟩, hy.trans <| closedBall_subset_ball hyr'⟩ | ||
| #align exists_pos_lt_subset_ball exists_pos_lt_subset_ball | ||
|
|
||
| /-- If a ball in a proper space includes a closed set `s`, then there exists a ball with the same | ||
| center and a strictly smaller radius that includes `s`. -/ | ||
| theorem exists_lt_subset_ball (hs : IsClosed s) (h : s ⊆ ball x r) : ∃ r' < r, s ⊆ ball x r' := by | ||
| rcases le_or_lt r 0 with hr | hr | ||
| · rw [ball_eq_empty.2 hr, subset_empty_iff] at h | ||
| subst s | ||
| exact (exists_lt r).imp fun r' hr' => ⟨hr', empty_subset _⟩ | ||
| · exact (exists_pos_lt_subset_ball hr hs h).imp fun r' hr' => ⟨hr'.1.2, hr'.2⟩ | ||
| #align exists_lt_subset_ball exists_lt_subset_ball | ||
|
|
||
| end ProperSpace | ||
|
|
||
| theorem Metric.exists_isLocalMin_mem_ball [PseudoMetricSpace α] [ProperSpace α] [TopologicalSpace β] | ||
| [ConditionallyCompleteLinearOrder β] [OrderTopology β] {f : α → β} {a z : α} {r : ℝ} | ||
| (hf : ContinuousOn f (closedBall a r)) (hz : z ∈ closedBall a r) | ||
| (hf1 : ∀ z' ∈ sphere a r, f z < f z') : ∃ z ∈ ball a r, IsLocalMin f z := by | ||
| simp_rw [← closedBall_diff_ball] at hf1 | ||
| exact (isCompact_closedBall a r).exists_isLocalMin_mem_open ball_subset_closedBall hf hz hf1 | ||
| isOpen_ball | ||
| #align metric.exists_local_min_mem_ball Metric.exists_isLocalMin_mem_ball |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters