OAI/NumberTheory/TwoPoint/Halasz/HalaszResidueQuotient.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Quotient coordinates in one positive residue class. Representatives p*u-a, with 0<=a<p, avoid a boundary point at u=0.

  1. def OAI.TwoPointCorrelations.halaszResidueQuotient line 13
  2. def OAI.TwoPointCorrelations.halaszResidueIndex line 16
  3. lemma OAI.TwoPointCorrelations.halasz_residue_quotient_recover line 19
  4. lemma OAI.TwoPointCorrelations.halasz_residue_quotient_injOn line 28
  5. def OAI.TwoPointCorrelations.halaszResidueTupleQuotient line 42
  6. lemma OAI.TwoPointCorrelations.halasz_residue_tuple_quotient_injOn line 47
  7. lemma OAI.TwoPointCorrelations.halasz_residue_tuple_trace line 63