OAI/NumberTheory/TwoPointCorrelations/HalaszPretentiousCenter.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The minimizing twist and the elementary part of MRT Lemma A.4(ii). Two nearby candidates for the minimum force a lower bound by an explicit prime cosine sum. Analytic estimates for that prime sum are kept separate.

  1. lemma OAI.TwoPointCorrelations.halasz_distance_continuous line 16

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszPretentiousCenter.lean:16 (same declaration text).

  2. theorem OAI.TwoPointCorrelations.halasz_minimizing_twist line 21

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

  3. lemma OAI.TwoPointCorrelations.halasz_twist_sum_norm line 30

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszPretentiousCenter.lean:30 (same declaration text).

  4. theorem OAI.TwoPointCorrelations.halasz_two_twist_distance line 44

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszPretentiousCenter.lean:44 (same declaration text).

  5. lemma OAI.TwoPointCorrelations.halasz_distance_from_minimizer line 71

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszPretentiousCenter.lean:71 (same declaration text).

  6. lemma OAI.TwoPointCorrelations.halasz_prime_cosine_tail_lower line 81

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszPretentiousCenter.lean:81 (same declaration text).

  7. lemma OAI.TwoPointCorrelations.halasz_masked_cosine_tail_lower line 93

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszPretentiousCenter.lean:93 (same declaration text).