OAI/NumberTheory/TwoPoint/Halasz/HalaszPhaseSum.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A uniform power-sum estimate, using centered cells past the frequency.

  1. lemma OAI.TwoPointCorrelations.halasz_phase_cells_telescope line 11

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPhaseSum.lean:11 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.halasz_phase_cell_sum_error line 27

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPhaseSum.lean:27 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.halasz_power_phase_prefix_norm line 57

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPhaseSum.lean:57 (same declaration text).

  4. theorem OAI.TwoPointCorrelations.halasz_power_phase_sum_integral line 63

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPhaseSum.lean:63 (same declaration text).

  5. theorem OAI.TwoPointCorrelations.halasz_power_phase_sum line 128

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPhaseSum.lean:128 (same declaration text).

  6. theorem OAI.TwoPointCorrelations.halasz_power_phase_sum_real line 137

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPhaseSum.lean:137 (same declaration text).