OAI/NumberTheory/TwoPoint/Halasz/HalaszLargeDegrees.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The block of middle Taylor degrees supplying a quadratic total saving.

  1. def OAI.TwoPointCorrelations.halaszLargeDegreeMap line 12
  2. lemma OAI.TwoPointCorrelations.halasz_large_degree_map_injective line 15
  3. def OAI.TwoPointCorrelations.halaszLargeDegrees line 23
  4. lemma OAI.TwoPointCorrelations.halasz_large_degrees_card line 26
  5. lemma OAI.TwoPointCorrelations.halasz_large_degrees_range line 31
  6. theorem OAI.TwoPointCorrelations.halasz_large_degree_weight_product line 38