OAI/NumberTheory/Ostmann/Quadratic/QuadraticScaleContinuity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Scale continuity on a common finite quadratic cutoff

  1. theorem OAI.Ostmann.inv_sub_abs_le_of_one_le line 12
  2. theorem OAI.Ostmann.sqrt_sub_abs_le_of_one_le line 20
  3. theorem OAI.Ostmann.inv_sqrt_sub_abs_le_of_one_le line 35
  4. theorem OAI.Ostmann.quadratic_normalizer_factor line 41
  5. theorem OAI.Ostmann.quadraticDensityTerm_scale_sub_bound line 48