OAI/NumberTheory/TwoPoint/Bounds/SourceDeletionTerms.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The three source deletions at the actual, possibly bin-dependent, integer sampling sites. Extra pair eligibility is retained in the rare term and may be discarded in the two nonnegative numerical terms.

  1. lemma OAI.TwoPointCorrelations.uniformAverage_finset_sum line 16
  2. lemma OAI.TwoPointCorrelations.uniformAverage_prohibitedPositiveRow line 22
  3. def OAI.TwoPointCorrelations.positiveDeletionAtom line 32
  4. lemma OAI.TwoPointCorrelations.positiveDeletionAtom_le line 44
  5. lemma OAI.TwoPointCorrelations.variable_source_deletion_split line 65
  6. lemma OAI.TwoPointCorrelations.shifted_source_deletion_split line 103