OAI/NumberTheory/TwoPoint/Halasz/HalaszTorusWindow.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The product localization window and its exact volume on the finite coefficient torus.

  1. def OAI.TwoPointCorrelations.halaszTorusWindow line 13
  2. lemma OAI.TwoPointCorrelations.halasz_torus_window_measurable_set line 17
  3. lemma OAI.TwoPointCorrelations.halasz_torus_window_product line 21
  4. lemma OAI.TwoPointCorrelations.halasz_torus_window_memLp line 26
  5. lemma OAI.TwoPointCorrelations.halasz_torus_window_norm_square line 30
  6. lemma OAI.TwoPointCorrelations.halasz_torus_window_square_integral line 40
  7. lemma OAI.TwoPointCorrelations.halasz_torus_window_coefficient line 51