OAI/NumberTheory/TwoPoint/QuantitativeAffineTransfer.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Quantitative passage from all progression classes to the main affine Liouville statement. The logarithmic exponent is preserved.

  1. lemma OAI.TwoPointCorrelations.progressionSum_eq_residuePrefix line 15
  2. lemma OAI.TwoPointCorrelations.liouville_affine_norm_le line 24
  3. lemma OAI.TwoPointCorrelations.eventually_log_power_le_self line 41
  4. lemma OAI.TwoPointCorrelations.affine_cutoff_log_bound line 50
  5. lemma OAI.TwoPointCorrelations.real_log_saving_extend line 95
  6. theorem OAI.TwoPointCorrelations.liouvilleLogSaving_of_progression line 130