English
Given the auxiliary bounds, a final inequality on the normalized difference is established for all i ≠ j.
Русский
С учётом вспомогательных ограничений выводится итоговое неравенство на нормированную разность для всех i ≠ j.
LaTeX
$$$$1 - δ ≤ \\|a.c i - (2/\\|a.c j\\|) a.c j\\|$$$$
Lean4
theorem exists_normalized {N : ℕ} {τ : ℝ} (a : SatelliteConfig E N τ) (lastc : a.c (last N) = 0)
(lastr : a.r (last N) = 1) (hτ : 1 ≤ τ) (δ : ℝ) (hδ1 : τ ≤ 1 + δ / 4) (hδ2 : δ ≤ 1) :
∃ c' : Fin N.succ → E, (∀ n, ‖c' n‖ ≤ 2) ∧ Pairwise fun i j => 1 - δ ≤ ‖c' i - c' j‖ :=
by
let c' : Fin N.succ → E := fun i => if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
have norm_c'_le : ∀ i, ‖c' i‖ ≤ 2 := by
intro i
simp only [c']
split_ifs with h; · exact h
by_cases hi : ‖a.c i‖ = 0 <;> simp [norm_smul, hi]
refine
⟨c', fun n => norm_c'_le n, fun i j inej => ?_⟩
-- up to exchanging `i` and `j`, one can assume `‖c i‖ ≤ ‖c j‖`.
wlog hij : ‖a.c i‖ ≤ ‖a.c j‖ generalizing i j
· rw [norm_sub_rev]; exact this j i inej.symm (le_of_not_ge hij)
rcases le_or_gt ‖a.c j‖ 2 with
(Hj | Hj)
-- case `‖c j‖ ≤ 2` (and therefore also `‖c i‖ ≤ 2`)
· simp_rw [c', Hj, hij.trans Hj, if_true]
exact exists_normalized_aux1 a lastr hτ δ hδ1 hδ2 i j inej
· have H'j : ‖a.c j‖ ≤ 2 ↔ False := by simpa only [not_le, iff_false] using Hj
rcases le_or_gt ‖a.c i‖ 2 with (Hi | Hi)
· -- case `‖c i‖ ≤ 2`
simp_rw [c', Hi, if_true, H'j, if_false]
exact exists_normalized_aux2 a lastc lastr hτ δ hδ1 hδ2 i j inej Hi Hj
· -- case `2 < ‖c i‖`
have H'i : ‖a.c i‖ ≤ 2 ↔ False := by simpa only [not_le, iff_false] using Hi
simp_rw [c', H'i, if_false, H'j, if_false]
exact exists_normalized_aux3 a lastc lastr hτ δ hδ1 i j inej Hi hij
