OAI/GroupTheory/PolycyclicRecognition/Algebra/NormalizePositiveMass.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Normalizing a positive partition mass bounded below by one

  1. theorem OAI.PolycyclicRecognition.norm_normalized_sub_le_two line 14

    Source documentation

    The cutoff partition has mass at least one. Normalizing such vectors costs at most a factor two in their normed distance.

    theorem norm_normalized_sub_le_two (x y : E) (hx : 1 ≤ ‖x‖) (hy : 1 ≤ ‖y‖) :
    ‖‖x‖⁻¹ • x - ‖y‖⁻¹ • y‖ ≤ 2 * ‖x - y‖ := by
…