OAI/NumberTheory/TwoPoint/Halasz/HalaszScaledFrequency.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The symmetric character pairing in the double mean-value argument.

  1. def OAI.TwoPointCorrelations.halaszScaledFrequency line 12
  2. lemma OAI.TwoPointCorrelations.halasz_scaled_character_symm line 16
  3. lemma OAI.TwoPointCorrelations.halasz_scaled_frequency_sub line 27
  4. lemma OAI.TwoPointCorrelations.halasz_scaled_norm_abs line 33
  5. lemma OAI.TwoPointCorrelations.halasz_scaled_near_abs line 39
  6. lemma OAI.TwoPointCorrelations.halasz_weighted_character_power line 46
  7. lemma OAI.TwoPointCorrelations.halasz_scaled_power line 60