Lean4
/-- The Gromov-Hausdorff space is second countable. -/
instance : SecondCountableTopology GHSpace :=
by
refine secondCountable_of_countable_discretization fun δ δpos => ?_
let ε := 2 / 5 * δ
have εpos : 0 < ε := mul_pos (by simp) δpos
have : ∀ p : GHSpace, ∃ s : Set p.Rep, s.Finite ∧ univ ⊆ ⋃ x ∈ s, ball x ε := fun p => by
simpa only [subset_univ, true_and] using finite_cover_balls_of_compact (X := p.Rep) isCompact_univ εpos
choose s hs using this
have : ∀ p : GHSpace, ∀ t : Set p.Rep, t.Finite → ∃ n : ℕ, ∃ _ : Equiv t (Fin n), True :=
by
intro p t ht
let _ : Fintype t := Finite.fintype ht
exact ⟨Fintype.card t, Fintype.equivFin t, trivial⟩
choose N e _ using this
let N := fun p : GHSpace =>
N p (s p)
(hs p).1
-- equiv from `s p`, a nice finite subset of `p.rep`, to `Fin (N p)`, called `E p`
let E := fun p : GHSpace =>
e p (s p)
(hs p).1
-- A function `F` associating to `p : GHSpace` the data of all distances between points
-- in the `ε`-dense set `s p`.
let F : GHSpace → Σ n : ℕ, Fin n → Fin n → ℤ := fun p => ⟨N p, fun a b => ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋⟩
refine
⟨Σ n, Fin n → Fin n → ℤ, by infer_instance, F, fun p q hpq => ?_⟩
/- As the target space of F is countable, it suffices to show that two points
`p` and `q` with `F p = F q` are at distance `≤ δ`.
For this, we construct a map `Φ` from `s p ⊆ p.rep` (representing `p`)
to `q.rep` (representing `q`) which is almost an isometry on `s p`, and
with image `s q`. For this, we compose the identification of `s p` with `Fin (N p)`
and the inverse of the identification of `s q` with `Fin (N q)`. Together with
the fact that `N p = N q`, this constructs `Ψ` between `s p` and `s q`, and then
composing with the canonical inclusion we get `Φ`. -/
have Npq : N p = N q := (Sigma.mk.inj_iff.1 hpq).1
let Ψ : s p → s q := fun x => (E q).symm (Fin.cast Npq ((E p) x))
let Φ : s p → q.Rep := fun x => Ψ x
have main : ghDist p.Rep q.Rep ≤ ε + ε / 2 + ε :=
by
refine ghDist_le_of_approx_subsets Φ ?_ ?_ ?_
· show ∀ x : p.Rep, ∃ y ∈ s p, dist x y ≤ ε
intro x
have : x ∈ ⋃ y ∈ s p, ball y ε := (hs p).2 (mem_univ _)
rcases mem_iUnion₂.1 this with ⟨y, ys, hy⟩
exact ⟨y, ys, le_of_lt hy⟩
· show ∀ x : q.Rep, ∃ z : s p, dist x (Φ z) ≤ ε
intro x
have : x ∈ ⋃ y ∈ s q, ball y ε := (hs q).2 (mem_univ _)
rcases mem_iUnion₂.1 this with ⟨y, ys, hy⟩
let i : ℕ := E q ⟨y, ys⟩
let hi := ((E q) ⟨y, ys⟩).is_lt
have ihi_eq : (⟨i, hi⟩ : Fin (N q)) = (E q) ⟨y, ys⟩ := by rw [Fin.ext_iff, Fin.val_mk]
have hiq : i < N q := hi
have hip : i < N p := by rwa [Npq.symm] at hiq
let z := (E p).symm ⟨i, hip⟩
use z
have C1 : (E p) z = ⟨i, hip⟩ := (E p).apply_symm_apply ⟨i, hip⟩
have C2 : Fin.cast Npq ⟨i, hip⟩ = ⟨i, hi⟩ := rfl
have C3 : (E q).symm ⟨i, hi⟩ = ⟨y, ys⟩ := by rw [ihi_eq]; exact (E q).symm_apply_apply ⟨y, ys⟩
have : Φ z = y := by simp only [Φ, Ψ]; rw [C1, C2, C3]
rw [this]
exact le_of_lt hy
· show ∀ x y : s p, |dist x y - dist (Φ x) (Φ y)| ≤ ε
intro x y
let i : ℕ := E p x
have hip : i < N p := ((E p) x).2
have hiq : i < N q := by rwa [Npq] at hip
have i' : i = (E q) (Ψ x) := by
simp only [i, Ψ, Equiv.apply_symm_apply, Fin.coe_cast]
-- introduce `j`, that codes both `y` and `Φ y` in `Fin (N p) = Fin (N q)`
let j : ℕ := E p y
have hjp : j < N p := ((E p) y).2
have hjq : j < N q := by rwa [Npq] at hjp
have j' : j = ((E q) (Ψ y)).1 := by
simp only [j, Ψ, Equiv.apply_symm_apply, Fin.coe_cast]
-- Express `dist x y` in terms of `F p`
have : (F p).2 ((E p) x) ((E p) y) = ⌊ε⁻¹ * dist x y⌋ := by simp only [F, (E p).symm_apply_apply]
have Ap : (F p).2 ⟨i, hip⟩ ⟨j, hjp⟩ = ⌊ε⁻¹ * dist x y⌋ := by
rw [← this]
-- Express `dist (Φ x) (Φ y)` in terms of `F q`
have : (F q).2 ((E q) (Ψ x)) ((E q) (Ψ y)) = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋ := by simp only [F, (E q).symm_apply_apply]
have Aq : (F q).2 ⟨i, hiq⟩ ⟨j, hjq⟩ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋ :=
by
rw [← this]
congr!
-- use the equality between `F p` and `F q` to deduce that the distances have equal
-- integer parts
have : (F p).2 ⟨i, hip⟩ ⟨j, hjp⟩ = (F q).2 ⟨i, hiq⟩ ⟨j, hjq⟩ :=
by
have hpq' : (F p).snd ≍ (F q).snd := (Sigma.mk.inj_iff.1 hpq).2
rw [Fin.heq_fun₂_iff Npq Npq] at hpq'
rw [← hpq']
rw [Ap, Aq] at this
have I :=
calc
|ε⁻¹| * |dist x y - dist (Ψ x) (Ψ y)| = |ε⁻¹ * (dist x y - dist (Ψ x) (Ψ y))| := (abs_mul _ _).symm
_ = |ε⁻¹ * dist x y - ε⁻¹ * dist (Ψ x) (Ψ y)| := by congr; ring
_ ≤ 1 := le_of_lt (abs_sub_lt_one_of_floor_eq_floor this)
calc
|dist x y - dist (Ψ x) (Ψ y)| = ε * ε⁻¹ * |dist x y - dist (Ψ x) (Ψ y)| := by
rw [mul_inv_cancel₀ (ne_of_gt εpos), one_mul]
_ = ε * (|ε⁻¹| * |dist x y - dist (Ψ x) (Ψ y)|) := by rw [abs_of_nonneg (le_of_lt (inv_pos.2 εpos)), mul_assoc]
_ ≤ ε * 1 := (mul_le_mul_of_nonneg_left I (le_of_lt εpos))
_ = ε := mul_one _
calc
dist p q = ghDist p.Rep q.Rep := dist_ghDist p q
_ ≤ ε + ε / 2 + ε := main
_ = δ := by ring
