OAI/NumberTheory/TwoPoint/Bounds/NonrawRoughData.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The rough coefficient families obtained by selecting at least one constant term in the center-band expansion. Their support and unit bound are derived from the actual finite prime products.

  1. def OAI.TwoPointCorrelations.nonrawRoughSupport line 16
  2. def OAI.TwoPointCorrelations.nonrawRoughData line 20
  3. def OAI.TwoPointCorrelations.activeNonrawDivisors line 25
  4. lemma OAI.TwoPointCorrelations.nonraw_support_primeFactors line 28
  5. lemma OAI.TwoPointCorrelations.nonraw_support_rough line 33
  6. lemma OAI.TwoPointCorrelations.nonraw_support_bin line 42
  7. lemma OAI.TwoPointCorrelations.nonrawRoughData_inBin line 55
  8. lemma OAI.TwoPointCorrelations.activeNonrawDivisor_pos line 71
  9. lemma OAI.TwoPointCorrelations.activeNonrawDivisor_lower line 75
  10. lemma OAI.TwoPointCorrelations.nonraw_support_same_core line 93
  11. lemma OAI.TwoPointCorrelations.nonraw_cutoff_dilation line 106