OAI/NumberTheory/Ostmann/Characters/TailCharacterBias.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Both character orders control the actual tail transform

  1. theorem OAI.Ostmann.translated_complexJacobi_mean line 12
  2. theorem OAI.Ostmann.translatedResidueCharacterMean_norm_le_higher line 24
  3. theorem OAI.Ostmann.translated_tail_character_mean_bound line 34
  4. theorem OAI.Ostmann.tailDensityMask_character_mean line 46
  5. theorem OAI.Ostmann.tailDensityMask_reverse_character_mean_bound line 60
  6. theorem OAI.Ostmann.tail_transform_mixed_bound line 77