OAI/NumberTheory/TwoPoint/Bounds/PrimeRowSecondMoment.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Finite second moments for the positive row majorant used to delete rare sites. Independence is used only under the auxiliary product law.

  1. lemma OAI.TwoPointCorrelations.FiniteLaw.average_add line 15
  2. lemma OAI.TwoPointCorrelations.FiniteLaw.independent_average_coordinate_mul line 19
  3. lemma OAI.TwoPointCorrelations.booleanLaw_indicator_average line 45
  4. lemma OAI.TwoPointCorrelations.independent_boolean_count_average line 49
  5. lemma OAI.TwoPointCorrelations.independent_boolean_count_square line 61
  6. lemma OAI.TwoPointCorrelations.independent_boolean_shifted_count_square line 97
  7. lemma OAI.TwoPointCorrelations.padding_weight_square_average line 118