OAI/NumberTheory/TwoPoint/Halasz/HalaszRepeatedCoordinates.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A repeated coordinate in any two prescribed positions is counted by the same doubled-variable system.

  1. lemma OAI.TwoPointCorrelations.halasz_equiv_two_points line 12
  2. lemma OAI.TwoPointCorrelations.halasz_frequency_permute line 28
  3. def OAI.TwoPointCorrelations.halaszRepeatTuple line 34
  4. lemma OAI.TwoPointCorrelations.halasz_repeat_tuple_frequency line 37
  5. def OAI.TwoPointCorrelations.halaszPairCollision line 45
  6. lemma OAI.TwoPointCorrelations.halasz_repeat_recover line 50
  7. lemma OAI.TwoPointCorrelations.halasz_canonical_collision_bound line 59
  8. theorem OAI.TwoPointCorrelations.halasz_pair_collision_bound line 90