English
For last center and radius, appropriate bounds hold: 1−δ ≤ ∥a.c i∥ for various i, with last fixed at 0 and r at last equal to 1.
Русский
Для последнего центра и радиуса выполняются необходимые неравенства; последний центр равен 0, радиус равен 1.
LaTeX
$$$$1 - δ ≤ ∥a.c i∥$$$$
Lean4
theorem exists_normalized_aux2 {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) (i j : Fin N.succ)
(inej : i ≠ j) (hi : ‖a.c i‖ ≤ 2) (hj : 2 < ‖a.c j‖) : 1 - δ ≤ ‖a.c i - (2 / ‖a.c j‖) • a.c j‖ :=
by
have ah :
Pairwise fun i j => a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j := by
simpa only [dist_eq_norm] using a.h
have δnonneg : 0 ≤ δ := by linarith only [hτ, hδ1]
have D : 0 ≤ 1 - δ / 4 := by linarith only [hδ2]
have hcrj : ‖a.c j‖ ≤ a.r j + 1 := by simpa only [lastc, lastr, dist_zero_right] using a.inter' j
have I : a.r i ≤ 2 := by
rcases lt_or_ge i (last N) with (H | H)
· apply (a.hlast i H).1.trans
simpa only [dist_eq_norm, lastc, sub_zero] using hi
· have : i = last N := top_le_iff.1 H
rw [this, lastr]
exact one_le_two
have J : (1 - δ / 4) * τ ≤ 1 :=
calc
(1 - δ / 4) * τ ≤ (1 - δ / 4) * (1 + δ / 4) := by gcongr
_ = (1 : ℝ) - δ ^ 2 / 16 := by ring
_ ≤ 1 := by linarith only [sq_nonneg δ]
have A : a.r j - δ ≤ ‖a.c i - a.c j‖ := by
rcases ah inej.symm with (H | H); · rw [norm_sub_rev]; linarith [H.1]
have C : a.r j ≤ 4 :=
calc
a.r j ≤ τ * a.r i := H.2
_ ≤ τ * 2 := by gcongr
_ ≤ 5 / 4 * 2 := by gcongr; linarith only [hδ1, hδ2]
_ ≤ 4 := by norm_num
calc
a.r j - δ ≤ a.r j - a.r j / 4 * δ := by
gcongr _ - ?_
exact mul_le_of_le_one_left δnonneg (by linarith only [C])
_ = (1 - δ / 4) * a.r j := by ring
_ ≤ (1 - δ / 4) * (τ * a.r i) := (mul_le_mul_of_nonneg_left H.2 D)
_ ≤ 1 * a.r i := by rw [← mul_assoc]; gcongr
_ ≤ ‖a.c i - a.c j‖ := by rw [one_mul]; exact H.1
set d := (2 / ‖a.c j‖) • a.c j with hd
have : a.r j - δ ≤ ‖a.c i - d‖ + (a.r j - 1) :=
calc
a.r j - δ ≤ ‖a.c i - a.c j‖ := A
_ ≤ ‖a.c i - d‖ + ‖d - a.c j‖ := by simp only [← dist_eq_norm, dist_triangle]
_ ≤ ‖a.c i - d‖ + (a.r j - 1) := by
apply add_le_add_left
have A : 0 ≤ 1 - 2 / ‖a.c j‖ := by simpa [div_le_iff₀ (zero_le_two.trans_lt hj)] using hj.le
rw [← one_smul ℝ (a.c j), hd, ← sub_smul, norm_smul, norm_sub_rev, Real.norm_eq_abs, abs_of_nonneg A, sub_mul]
field_simp
linarith only [hcrj]
linarith only [this]
