OAI/NumberTheory/TwoPoint/Halasz/HalaszBandWeights.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

On one logarithmic band the two prime mean-square masses cancel: the adaptive denominator contributes v⁻² and the two prime masses O(v²).

  1. lemma OAI.TwoPointCorrelations.halasz_prime_set_mass_le line 14

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszBandWeights.lean:14 (same declaration text).

  2. theorem OAI.TwoPointCorrelations.halasz_band_mean_square_weights line 26

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszBandWeights.lean:26 (same declaration text).