OAI/NumberTheory/TwoPoint/Halasz/HalaszWindowOverlap.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Translated product windows only interact at nearby centers.

  1. def OAI.TwoPointCorrelations.HalaszWindowNear line 12
  2. lemma OAI.TwoPointCorrelations.halasz_window_common_near line 15
  3. lemma OAI.TwoPointCorrelations.halasz_window_product_bound line 30
  4. lemma OAI.TwoPointCorrelations.halasz_window_translate_memLp line 43
  5. lemma OAI.TwoPointCorrelations.halasz_window_overlap_integral line 52
  6. def OAI.TwoPointCorrelations.halaszWindowL2 line 80
  7. lemma OAI.TwoPointCorrelations.halasz_window_l2_coe line 84
  8. lemma OAI.TwoPointCorrelations.halasz_window_l2_overlap line 90