English
There is a lower bound for ∥(2/∥a.c i∥) a.c i − (2/∥a.c j∥) a.c j∥ in terms of δ and τ, for i ≠ j.
Русский
Для i ≠ j существует нижняя граница на разность норм двух нормированных спутников, выраженная через δ и τ.
LaTeX
$$$$1 - δ ≤ \\left\\| \\left(\\frac{2}{\\|a.c i\\|}\\right)a.c i - \\left(\\frac{2}{\\|a.c j\\|}\\right)a.c j\\right\\| $$$$
Lean4
theorem exists_normalized_aux3 {N : ℕ} {τ : ℝ} (a : SatelliteConfig E N τ) (lastc : a.c (last N) = 0)
(lastr : a.r (last N) = 1) (hτ : 1 ≤ τ) (δ : ℝ) (hδ1 : τ ≤ 1 + δ / 4) (i j : Fin N.succ) (inej : i ≠ j)
(hi : 2 < ‖a.c i‖) (hij : ‖a.c i‖ ≤ ‖a.c j‖) : 1 - δ ≤ ‖(2 / ‖a.c i‖) • 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 hcrj : ‖a.c j‖ ≤ a.r j + 1 := by simpa only [lastc, lastr, dist_zero_right] using a.inter' j
have A : a.r i ≤ ‖a.c i‖ :=
by
have : i < last N := by
apply lt_top_iff_ne_top.2
intro iN
change i = last N at iN
rw [iN, lastc, norm_zero] at hi
exact lt_irrefl _ (zero_le_two.trans_lt hi)
convert (a.hlast i this).1 using 1
rw [dist_eq_norm, lastc, sub_zero]
have hj : 2 < ‖a.c j‖ := hi.trans_le hij
set s := ‖a.c i‖
have spos : 0 < s := zero_lt_two.trans hi
set d := (s / ‖a.c j‖) • a.c j with hd
have I : ‖a.c j - a.c i‖ ≤ ‖a.c j‖ - s + ‖d - a.c i‖ :=
calc
‖a.c j - a.c i‖ ≤ ‖a.c j - d‖ + ‖d - a.c i‖ := by simp [← dist_eq_norm, dist_triangle]
_ = ‖a.c j‖ - ‖a.c i‖ + ‖d - a.c i‖ := by
nth_rw 1 [← one_smul ℝ (a.c j)]
rw [add_left_inj, hd, ← sub_smul, norm_smul, Real.norm_eq_abs, abs_of_nonneg, sub_mul, one_mul,
div_mul_cancel₀ _ (zero_le_two.trans_lt hj).ne']
rwa [sub_nonneg, div_le_iff₀ (zero_lt_two.trans hj), one_mul]
have J : a.r j - ‖a.c j - a.c i‖ ≤ s / 2 * δ :=
calc
a.r j - ‖a.c j - a.c i‖ ≤ s * (τ - 1) :=
by
rcases ah inej.symm with (H | H)
·
calc
a.r j - ‖a.c j - a.c i‖ ≤ 0 := sub_nonpos.2 H.1
_ ≤ s * (τ - 1) := mul_nonneg spos.le (sub_nonneg.2 hτ)
· rw [norm_sub_rev] at H
calc
a.r j - ‖a.c j - a.c i‖ ≤ τ * a.r i - a.r i := sub_le_sub H.2 H.1
_ = a.r i * (τ - 1) := by ring
_ ≤ s * (τ - 1) := mul_le_mul_of_nonneg_right A (sub_nonneg.2 hτ)
_ ≤ s * (δ / 2) := (mul_le_mul_of_nonneg_left (by linarith only [δnonneg, hδ1]) spos.le)
_ = s / 2 * δ := by ring
have invs_nonneg : 0 ≤ 2 / s := div_nonneg zero_le_two (zero_le_two.trans hi.le)
calc
1 - δ = 2 / s * (s / 2 - s / 2 * δ) := by field_simp
_ ≤ 2 / s * ‖d - a.c i‖ := (mul_le_mul_of_nonneg_left (by linarith only [hcrj, I, J, hi]) invs_nonneg)
_ = ‖(2 / s) • a.c i - (2 / ‖a.c j‖) • a.c j‖ :=
by
conv_lhs => rw [norm_sub_rev, ← abs_of_nonneg invs_nonneg]
rw [← Real.norm_eq_abs, ← norm_smul, smul_sub, hd, smul_smul]
congr 3
field_simp
