Lean4
/-- Compactness criterion: a closed set of compact metric spaces is compact if the spaces have
a uniformly bounded diameter, and for all `ε` the number of balls of radius `ε` required
to cover the spaces is uniformly bounded. This is an equivalence, but we only prove the
interesting direction that these conditions imply compactness. -/
theorem totallyBounded {t : Set GHSpace} {C : ℝ} {u : ℕ → ℝ} {K : ℕ → ℕ} (ulim : Tendsto u atTop (𝓝 0))
(hdiam : ∀ p ∈ t, diam (univ : Set (GHSpace.Rep p)) ≤ C)
(hcov : ∀ p ∈ t, ∀ n : ℕ, ∃ s : Set (GHSpace.Rep p), (#s) ≤ K n ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)) :
TotallyBounded t := by
/- Let `δ>0`, and `ε = δ/5`. For each `p`, we construct a finite subset `s p` of `p`, which
is `ε`-dense and has cardinality at most `K n`. Encoding the mutual distances of points
in `s p`, up to `ε`, we will get a map `F` associating to `p` finitely many data, and making
it possible to reconstruct `p` up to `ε`. This is enough to prove total boundedness. -/
refine Metric.totallyBounded_of_finite_discretization fun δ δpos => ?_
let ε := 1 / 5 * δ
have εpos : 0 < ε := mul_pos (by simp) δpos
rcases Metric.tendsto_atTop.1 ulim ε εpos with ⟨n, hn⟩
have u_le_ε : u n ≤ ε := by
have := hn n le_rfl
simp only [Real.dist_eq, add_zero, sub_eq_add_neg, neg_zero] at this
exact
le_of_lt
(lt_of_le_of_lt (le_abs_self _) this)
-- construct a finite subset `s p` of `p` which is `ε`-dense and has cardinal `≤ K n`
have : ∀ p : GHSpace, ∃ s : Set p.Rep, ∃ N ≤ K n, ∃ _ : Equiv s (Fin N), p ∈ t → univ ⊆ ⋃ x ∈ s, ball x (u n) :=
by
intro p
by_cases hp : p ∉ t
· have : Nonempty (Equiv (∅ : Set p.Rep) (Fin 0)) := by rw [← Fintype.card_eq, card_empty, Fintype.card_fin]
use ∅, 0, bot_le, this.some
exact fun hp' => (hp hp').elim
· rcases hcov _ (Set.not_notMem.1 hp) n with ⟨s, ⟨scard, scover⟩⟩
rcases Cardinal.lt_aleph0.1 (lt_of_le_of_lt scard (Cardinal.nat_lt_aleph0 _)) with ⟨N, hN⟩
rw [hN, Nat.cast_le] at scard
have : #s = #(Fin N) := by rw [hN, Cardinal.mk_fin]
obtain ⟨E⟩ := Quotient.exact this
use s, N, scard, E
simp only [scover, imp_true_iff]
choose s N hN E hs using this
let M := ⌊ε⁻¹ * max C 0⌋₊
let F : GHSpace → Σ k : Fin (K n).succ, Fin k → Fin k → Fin M.succ := fun p =>
⟨⟨N p, lt_of_le_of_lt (hN p) (Nat.lt_succ_self _)⟩, fun a b =>
⟨min M ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋₊, (min_le_left _ _).trans_lt (Nat.lt_succ_self _)⟩⟩
refine ⟨_, ?_, fun p => F p, ?_⟩
·
infer_instance
-- It remains to show that if `F p = F q`, then `p` and `q` are `ε`-close
rintro ⟨p, pt⟩ ⟨q, qt⟩ hpq
have Npq : N p = N q := Fin.ext_iff.1 (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
-- to prove the main inequality, argue that `s p` is `ε`-dense in `p`, and `s q` is `ε`-dense
-- in `q`, and `s p` and `s q` are almost isometric. Then closeness follows
-- from `ghDist_le_of_approx_subsets`
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 (u n) := (hs p pt) (mem_univ _)
rcases mem_iUnion₂.1 this with ⟨y, ys, hy⟩
exact ⟨y, ys, le_trans (le_of_lt hy) u_le_ε⟩
· show ∀ x : q.Rep, ∃ z : s p, dist x (Φ z) ≤ ε
intro x
have : x ∈ ⋃ y ∈ s q, ball y (u n) := (hs q qt) (mem_univ _)
rcases mem_iUnion₂.1 this with ⟨y, ys, hy⟩
let i : ℕ := E q ⟨y, ys⟩
let hi := ((E q) ⟨y, ys⟩).2
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_trans (le_of_lt hy) u_le_ε
· show ∀ x y : s p, |dist x y - dist (Φ x) (Φ y)| ≤ ε
intro x y
have : dist (Φ x) (Φ y) = dist (Ψ x) (Ψ y) := rfl
rw [this]
-- introduce `i`, that codes both `x` and `Φ x` in `Fin (N p) = Fin (N q)`
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) := by
simp only [j, Ψ, Equiv.apply_symm_apply, Fin.coe_cast]
-- Express `dist x y` in terms of `F p`
have Ap : ((F p).2 ⟨i, hip⟩ ⟨j, hjp⟩).1 = ⌊ε⁻¹ * dist x y⌋₊ :=
calc
((F p).2 ⟨i, hip⟩ ⟨j, hjp⟩).1 = ((F p).2 ((E p) x) ((E p) y)).1 := by congr
_ = min M ⌊ε⁻¹ * dist x y⌋₊ := by simp only [F, (E p).symm_apply_apply]
_ = ⌊ε⁻¹ * dist x y⌋₊ := by
refine min_eq_right (Nat.floor_mono ?_)
refine mul_le_mul_of_nonneg_left (le_trans ?_ (le_max_left _ _)) (inv_pos.2 εpos).le
change dist (x : p.Rep) y ≤ C
refine (dist_le_diam_of_mem isCompact_univ.isBounded (mem_univ _) (mem_univ _)).trans ?_
exact hdiam p pt
have Aq : ((F q).2 ⟨i, hiq⟩ ⟨j, hjq⟩).1 = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋₊ :=
calc
((F q).2 ⟨i, hiq⟩ ⟨j, hjq⟩).1 = ((F q).2 ((E q) (Ψ x)) ((E q) (Ψ y))).1 := by congr!
_ = min M ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋₊ := by simp only [F, (E q).symm_apply_apply]
_ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋₊ := by
refine min_eq_right (Nat.floor_mono ?_)
refine mul_le_mul_of_nonneg_left (le_trans ?_ (le_max_left _ _)) (inv_pos.2 εpos).le
change dist (Ψ x : q.Rep) (Ψ y) ≤ C
refine (dist_le_diam_of_mem isCompact_univ.isBounded (mem_univ _) (mem_univ _)).trans ?_
exact hdiam q qt
have : ((F p).2 ⟨i, hip⟩ ⟨j, hjp⟩).1 = ((F q).2 ⟨i, hiq⟩ ⟨j, hjq⟩).1 :=
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']
have : ⌊ε⁻¹ * dist x y⌋ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋ :=
by
rw [Ap, Aq] at this
have D : 0 ≤ ⌊ε⁻¹ * dist x y⌋ := floor_nonneg.2 (mul_nonneg (le_of_lt (inv_pos.2 εpos)) dist_nonneg)
have D' : 0 ≤ ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋ := floor_nonneg.2 (mul_nonneg (le_of_lt (inv_pos.2 εpos)) dist_nonneg)
rw [← Int.toNat_of_nonneg D, ← Int.toNat_of_nonneg D', Int.floor_toNat, Int.floor_toNat, this]
-- deduce that the distances coincide up to `ε`, by a straightforward computation
-- that should be automated
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
_ = δ / 2 := by simp only [ε, one_div]; ring
_ < δ := half_lt_self δpos
