OAI/NumberTheory/TwoPoint/Halasz/HalaszDistanceCutoff.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A fixed-power change of the prime cutoff changes the squared pretentious distance by an absolute constant.

  1. lemma OAI.TwoPointCorrelations.halasz_prime_cutoff_subset line 13

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszDistanceCutoff.lean:13 (same declaration text).

  2. theorem OAI.TwoPointCorrelations.halasz_distance_cutoff_loss line 18

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszDistanceCutoff.lean:18 (same declaration text).