Lean4
/-- If `δ` is small enough, a `(1-δ)`-separated set in the ball of radius `2` also has cardinality
at most `multiplicity E`. -/
theorem exists_goodδ :
∃ δ : ℝ,
0 < δ ∧
δ < 1 ∧
∀ s : Finset E, (∀ c ∈ s, ‖c‖ ≤ 2) → (∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 - δ ≤ ‖c - d‖) → s.card ≤ multiplicity E :=
by
classical
/- This follows from a compactness argument: otherwise, one could extract a converging
subsequence, to obtain a `1`-separated set in the ball of radius `2` with cardinality
`N = multiplicity E + 1`. To formalize this, we work with functions `Fin N → E`.
-/
by_contra! h
set N := multiplicity E + 1 with hN
have : ∀ δ : ℝ, 0 < δ → ∃ f : Fin N → E, (∀ i : Fin N, ‖f i‖ ≤ 2) ∧ Pairwise fun i j => 1 - δ ≤ ‖f i - f j‖ :=
by
intro δ hδ
rcases lt_or_ge δ 1 with (hδ' | hδ')
· rcases h δ hδ hδ' with ⟨s, hs, h's, s_card⟩
obtain ⟨f, f_inj, hfs⟩ : ∃ f : Fin N → E, Function.Injective f ∧ range f ⊆ ↑s :=
by
have : Fintype.card (Fin N) ≤ s.card := by simp only [Fintype.card_fin]; exact s_card
rcases Function.Embedding.exists_of_card_le_finset this with ⟨f, hf⟩
exact ⟨f, f.injective, hf⟩
simp only [range_subset_iff, Finset.mem_coe] at hfs
exact ⟨f, fun i => hs _ (hfs i), fun i j hij => h's _ (hfs i) _ (hfs j) (f_inj.ne hij)⟩
·
exact
⟨fun _ => 0, by simp, fun i j _ => by simpa only [norm_zero, sub_nonpos, sub_self]⟩
-- For `δ > 0`, `F δ` is a function from `Fin N` to the ball of radius `2` for which two points
-- in the image are separated by `1 - δ`.
choose! F hF using this
have : ∃ f : Fin N → E, (∀ i : Fin N, ‖f i‖ ≤ 2) ∧ Pairwise fun i j => 1 ≤ ‖f i - f j‖ :=
by
obtain ⟨u, _, zero_lt_u, hu⟩ :
∃ u : ℕ → ℝ, (∀ m n : ℕ, m < n → u n < u m) ∧ (∀ n : ℕ, 0 < u n) ∧ Filter.Tendsto u Filter.atTop (𝓝 0) :=
exists_seq_strictAnti_tendsto (0 : ℝ)
have A : ∀ n, F (u n) ∈ closedBall (0 : Fin N → E) 2 :=
by
intro n
simp only [pi_norm_le_iff_of_nonneg zero_le_two, mem_closedBall, dist_zero_right, (hF (u n) (zero_lt_u n)).left,
forall_const]
obtain ⟨f, fmem, φ, φ_mono, hf⟩ :
∃ f ∈ closedBall (0 : Fin N → E) 2, ∃ φ : ℕ → ℕ, StrictMono φ ∧ Tendsto ((F ∘ u) ∘ φ) atTop (𝓝 f) :=
IsCompact.tendsto_subseq (isCompact_closedBall _ _) A
refine ⟨f, fun i => ?_, fun i j hij => ?_⟩
· simp only [pi_norm_le_iff_of_nonneg zero_le_two, mem_closedBall, dist_zero_right] at fmem
exact fmem i
· have A : Tendsto (fun n => ‖F (u (φ n)) i - F (u (φ n)) j‖) atTop (𝓝 ‖f i - f j‖) :=
((hf.apply_nhds i).sub (hf.apply_nhds j)).norm
have B : Tendsto (fun n => 1 - u (φ n)) atTop (𝓝 (1 - 0)) := tendsto_const_nhds.sub (hu.comp φ_mono.tendsto_atTop)
rw [sub_zero] at B
exact le_of_tendsto_of_tendsto' B A fun n => (hF (u (φ n)) (zero_lt_u _)).2 hij
rcases this with
⟨f, hf, h'f⟩
-- the range of `f` contradicts the definition of `multiplicity E`.
have finj : Function.Injective f := by
intro i j hij
by_contra h
have : 1 ≤ ‖f i - f j‖ := h'f h
simp only [hij, norm_zero, sub_self] at this
exact lt_irrefl _ (this.trans_lt zero_lt_one)
let s := Finset.image f Finset.univ
have s_card : s.card = N := by rw [Finset.card_image_of_injective _ finj]; exact Finset.card_fin N
have hs : ∀ c ∈ s, ‖c‖ ≤ 2 := by
simp only [s, hf, forall_apply_eq_imp_iff, forall_const, forall_exists_index, Finset.mem_univ, Finset.mem_image,
true_and]
have h's : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖ :=
by
simp only [s, forall_apply_eq_imp_iff, forall_exists_index, Finset.mem_univ, Finset.mem_image, Ne,
forall_apply_eq_imp_iff, true_and]
intro i j hij
have : i ≠ j := fun h => by rw [h] at hij; exact hij rfl
exact h'f this
have : s.card ≤ multiplicity E := card_le_multiplicity hs h's
rw [s_card, hN] at this
exact lt_irrefl _ ((Nat.lt_succ_self (multiplicity E)).trans_le this)
