OAI/NumberTheory/TwoPoint/Bounds/TruncatedDilation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A fixed dilation is approximated by finitely many smooth-divisor components. The discarded values lie in a literal smooth-divisor tail.

  1. def OAI.TwoPointCorrelations.smoothDilationTerm line 14
  2. lemma OAI.TwoPointCorrelations.smoothDilationTerm_eq_zero line 18
  3. lemma OAI.TwoPointCorrelations.smoothDilationTerm_at_part line 27
  4. def OAI.TwoPointCorrelations.truncatedDilation line 46
  5. lemma OAI.TwoPointCorrelations.truncatedDilation_eq_sum line 49
  6. lemma OAI.TwoPointCorrelations.norm_truncatedDilation_error line 74
  7. lemma OAI.TwoPointCorrelations.smoothPart_tail_indicator line 84