OAI/NumberTheory/TwoPoint/Bounds/QuantitativeDivisorBins.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Quantitative finite extraction at Y=floor(X/u), with the exact reciprocal mass of u and the absolute exponent 1000 retained.

  1. lemma OAI.TwoPointCorrelations.finite_rescaled_prefix_bound_at line 14
  2. theorem OAI.TwoPointCorrelations.quantitative_residue_bin_family line 38