OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/OneBounded.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OrdinaryCorrelations.OneBounded line 15

    Also declared: ComparatorChallenges/OrdinaryElliott.lean:11 (same declaration text).

  2. def OAI.OrdinaryCorrelations.Multiplicative line 17

    Also declared: ComparatorChallenges/OrdinaryElliott.lean:13 (same declaration text).

  3. def OAI.OrdinaryCorrelations.distanceSq line 20

    Also declared: ComparatorChallenges/OrdinaryElliott.lean:16 (same declaration text).

  4. def OAI.OrdinaryCorrelations.distance line 26

    Also declared: ComparatorChallenges/OrdinaryElliott.lean:22 (same declaration text).

  5. def OAI.OrdinaryCorrelations.UniformlyNonpretentious line 29

    Also declared: ComparatorChallenges/OrdinaryElliott.lean:25 (same declaration text).

  6. def OAI.OrdinaryCorrelations.shiftAverage line 34

    Also declared: ComparatorChallenges/OrdinaryElliott.lean:30 (same declaration text).

  7. def OAI.OrdinaryCorrelations.affineAverage line 37
  8. def OAI.OrdinaryCorrelations.progressionAverage line 40
  9. def OAI.OrdinaryCorrelations.liouville line 45
  10. def OAI.OrdinaryCorrelations.affineLiouvilleSum line 47
  11. def OAI.OrdinaryCorrelations.progressionLiouvilleSum line 50
  12. def OAI.OrdinaryCorrelations.BinaryCorrectedElliott line 54
  13. def OAI.OrdinaryCorrelations.AffineElliott line 61
  14. def OAI.OrdinaryCorrelations.ProgressionElliott line 68
  15. def OAI.OrdinaryCorrelations.AffineLiouvilleLogSaving line 75
  16. def OAI.OrdinaryCorrelations.ProgressionLiouvilleLogSaving line 80