OAI/NumberTheory/TwoPoint/Halasz/HalaszPowerTranslation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Translation of the complete system on a finite set of coordinates. The natural-number version uses an integer translation for the reverse implication, so no truncated subtraction is hidden in the statement.

  1. lemma OAI.TwoPointCorrelations.halasz_finite_power_translate line 12
  2. lemma OAI.TwoPointCorrelations.halasz_nat_power_translate_iff line 34
  3. lemma OAI.TwoPointCorrelations.halasz_power_vector_eq_iff line 49
  4. lemma OAI.TwoPointCorrelations.halasz_power_vector_translate_iff line 61