OAI/NumberTheory/TwoPointCorrelations/HalaszBandSummation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Summing the minimum of the trivial band estimate and the distance estimate. This is the step that keeps the factor (M+1) exp(-M).

  1. lemma OAI.TwoPointCorrelations.halasz_band_scale_sum line 12

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszBandSummation.lean:12 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.halasz_band_scale_sum_le line 21

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszBandSummation.lean:21 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.halasz_band_inverse_sum line 28

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszBandSummation.lean:28 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.halasz_band_inverse_sum_le line 38

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszBandSummation.lean:38 (same declaration text).

  5. lemma OAI.TwoPointCorrelations.halasz_band_min_split line 45

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszBandSummation.lean:45 (same declaration text).

  6. theorem OAI.TwoPointCorrelations.halasz_band_saving_sum line 56

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszBandSummation.lean:56 (same declaration text).