OAI/NumberTheory/TwoPoint/Halasz/HalaszNormalizedDoubleMoment.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Cancellation of the two complete-system degree costs against the coordinate volumes in the double moment.

  1. lemma OAI.TwoPointCorrelations.halasz_coordinate_degree line 12
  2. lemma OAI.TwoPointCorrelations.halasz_coordinate_total_degree line 23
  3. lemma OAI.TwoPointCorrelations.halasz_normalized_weight_nonneg line 28
  4. lemma OAI.TwoPointCorrelations.halasz_double_weight_nonneg line 33
  5. theorem OAI.TwoPointCorrelations.halasz_normalized_double_moment line 38