OAI/NumberTheory/TwoPoint/Halasz/HalaszDoubleWindow.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The coefficient window used in the double mean-value specialization.

  1. def OAI.TwoPointCorrelations.halaszDoubleWindow line 11
  2. lemma OAI.TwoPointCorrelations.halasz_double_window_pos line 14
  3. lemma OAI.TwoPointCorrelations.halasz_double_window_small line 21
  4. lemma OAI.TwoPointCorrelations.halasz_double_window_phase line 31
  5. lemma OAI.TwoPointCorrelations.halasz_double_window_product line 43