OAI/NumberTheory/TwoPoint/Halasz/HalaszIntegerKernel.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual finite weighted integer kernel used by sparse cofactor energy.

  1. def OAI.TwoPointCorrelations.halaszTriangleSupport line 12
  2. lemma OAI.TwoPointCorrelations.halasz_triangle_nat_zero line 15
  3. lemma OAI.TwoPointCorrelations.halasz_triangle_neg_zero line 23
  4. lemma OAI.TwoPointCorrelations.halasz_triangle_finite_sum line 30
  5. lemma OAI.TwoPointCorrelations.halasz_triangle_polynomial line 50
  6. theorem OAI.TwoPointCorrelations.halasz_integer_kernel line 63