English
Given a, the distances and radii satisfy a lower bound: 1 − δ ≤ ∥a.c i − a.c j∥ after normalization and depending on base radius 1.
Русский
Даны радиусы и центры спутников; после нормировки существует нижняя граница расстояний между центрами спутников.
LaTeX
$$$$1 - δ ≤ \\|a.c i - a.c j\\|$$$$
Lean4
theorem exists_normalized_aux1 {N : ℕ} {τ : ℝ} (a : SatelliteConfig E N τ) (lastr : a.r (last N) = 1) (hτ : 1 ≤ τ)
(δ : ℝ) (hδ1 : τ ≤ 1 + δ / 4) (hδ2 : δ ≤ 1) (i j : Fin N.succ) (inej : i ≠ j) : 1 - δ ≤ ‖a.c i - 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 τpos : 0 < τ := _root_.zero_lt_one.trans_le hτ
have I : (1 - δ / 4) * τ ≤ 1 :=
calc
(1 - δ / 4) * τ ≤ (1 - δ / 4) * (1 + δ / 4) := by gcongr
_ = (1 : ℝ) - δ ^ 2 / 16 := by ring
_ ≤ 1 := by linarith only [sq_nonneg δ]
have J : 1 - δ ≤ 1 - δ / 4 := by linarith only [δnonneg]
have K : 1 - δ / 4 ≤ τ⁻¹ := by rw [inv_eq_one_div, le_div_iff₀ τpos]; exact I
suffices L : τ⁻¹ ≤ ‖a.c i - a.c j‖ by linarith only [J, K, L]
have hτ' : ∀ k, τ⁻¹ ≤ a.r k := by
intro k
rw [inv_eq_one_div, div_le_iff₀ τpos, ← lastr, mul_comm]
exact a.hlast' k hτ
rcases ah inej with (H | H)
· apply le_trans _ H.1
exact hτ' i
· rw [norm_sub_rev]
apply le_trans _ H.1
exact hτ' j
