OAI/GroupTheory/PolycyclicRecognition/Algebra/MassFractionBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.mass_fraction_left_le line 9
2. theorem OAI.PolycyclicRecognition.min_mass_mul_abs_fraction_sub_le line 31

   Source documentation

   Normalization of a partial mass costs at most its own change plus the change of the total mass, after multiplication by the smaller total.

   theorem min_mass_mul_abs_fraction_sub_le {A B u v : ℝ}
       (hA : 0 < A) (hB : 0 < B) (hu : 0 ≤ u) (huA : u ≤ A)
       (hv : 0 ≤ v) (hvB : v ≤ B) :
       min A B * |u / A - v / B| ≤ |u - v| + |A - B| := by
   …

3. theorem OAI.PolycyclicRecognition.min_mass_mul_min_fraction_le line 43

   Source documentation

   The smaller normalized partial mass, rescaled by the smaller total, never exceeds either original partial mass.

   theorem min_mass_mul_min_fraction_le {A B u v : ℝ}
       (hA : 0 < A) (hB : 0 < B) (hu : 0 ≤ u) (hv : 0 ≤ v) :
       min A B * min (u / A) (v / B) ≤ min u v := by
   …