English
Rescaling a satellite configuration in a vector space to place the basepoint at 0 and the base radius at 1.
Русский
Пере масштабирование и перенастройка спутниковой конфигурации в векторном пространстве так, чтобы база находилась в нуле, а базовый радиус стал равным 1.
LaTeX
$$$$\\text{centerAndRescale : SatelliteConfig E N \\u03c4}$$$$
Lean4
/-- Rescaling a satellite configuration in a vector space, to put the basepoint at `0` and the base
radius at `1`. -/
def centerAndRescale : SatelliteConfig E N τ
where
c i := (a.r (last N))⁻¹ • (a.c i - a.c (last N))
r i := (a.r (last N))⁻¹ * a.r i
rpos i := by positivity
h i j
hij := by
simp (disch := positivity) only [dist_smul₀, dist_sub_right, mul_left_comm τ, Real.norm_of_nonneg]
rcases a.h hij with (⟨H₁, H₂⟩ | ⟨H₁, H₂⟩) <;> [left; right] <;> constructor <;> gcongr
hlast i
hi := by
simp (disch := positivity) only [dist_smul₀, dist_sub_right, mul_left_comm τ, Real.norm_of_nonneg]
have ⟨H₁, H₂⟩ := a.hlast i hi
constructor <;> gcongr
inter i
hi := by
simp (disch := positivity) only [dist_smul₀, ← mul_add, dist_sub_right, Real.norm_of_nonneg]
gcongr
exact a.inter i hi