OAI/NumberTheory/TwoPoint/Bounds/DilatedWindows.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact short-window reindexing for a sequence supported on multiples of a fixed integer. Only one endpoint term is lost to a fixed window length.

  1. def OAI.TwoPointCorrelations.dilationSequence line 14
  2. lemma OAI.TwoPointCorrelations.additiveCharacter_nat_mul line 17
  3. lemma OAI.TwoPointCorrelations.shortExponentialSum_dilation line 24
  4. lemma OAI.TwoPointCorrelations.quotient_window_length line 67
  5. lemma OAI.TwoPointCorrelations.norm_shortWindowSum_le_succ line 76
  6. lemma OAI.TwoPointCorrelations.norm_shortExponentialSum_dilation_le line 93
  7. lemma OAI.TwoPointCorrelations.quotient_sample_sum_le line 105