OAI/NumberTheory/TwoPoint/Halasz/HalaszPhaseTaylor.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Local phase expansion for the elementary near-twist sum comparison. The linear term cancels on intervals centered at an integer.

  1. lemma OAI.TwoPointCorrelations.halasz_log_one_add_small line 13

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

  2. lemma OAI.TwoPointCorrelations.halasz_phase_linear_error line 32

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPhaseTaylor.lean:32 (same declaration text).