centerAndRescale — Mathlib

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

Похожие утверждения