OAI/NumberTheory/TwoPoint/Halasz/HalaszLogTaylor.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A uniform logarithmic Taylor remainder for the short multiplicative shifts in the double mean-value method.

  1. def OAI.TwoPointCorrelations.halaszLogTaylor line 13
  2. lemma OAI.TwoPointCorrelations.halasz_log_taylor_remainder line 16
  3. lemma OAI.TwoPointCorrelations.halasz_exp_phase_lipschitz line 45
  4. lemma OAI.TwoPointCorrelations.halasz_log_taylor_phase line 58