OAI/NumberTheory/TwoPoint/Halasz/HalaszShortScale.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Integer short-variable lengths for the logarithmic bilinear argument.

  1. def OAI.TwoPointCorrelations.halaszShortScale line 8
  2. lemma OAI.TwoPointCorrelations.halasz_short_scale_bounds line 10
  3. lemma OAI.TwoPointCorrelations.halasz_short_scale_square line 21
  4. lemma OAI.TwoPointCorrelations.halasz_short_scale_le_base line 30