OAI/NumberTheory/TwoPoint/Halasz/HalaszRootScale.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A natural modulus scale just above the k-th root, with the exact division endpoint controlled for the classical recurrence.

  1. def OAI.TwoPointCorrelations.halaszRootScale line 9
  2. lemma OAI.TwoPointCorrelations.halasz_root_scale_pos line 11
  3. lemma OAI.TwoPointCorrelations.halasz_root_scale_lt line 15
  4. lemma OAI.TwoPointCorrelations.halasz_root_scale_upper line 26
  5. lemma OAI.TwoPointCorrelations.halasz_root_scale_large line 34
  6. lemma OAI.TwoPointCorrelations.halasz_root_scale_le_endpoint line 41
  7. lemma OAI.TwoPointCorrelations.halasz_division_endpoint line 63