OAI/NumberTheory/TwoPoint/Bounds/PaddingCutCost.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The two padding deletions with the positive tuple weight retained. The literal rejection function depends only on Q residues.

  1. def OAI.TwoPointCorrelations.paddingRejectedMass line 14
  2. lemma OAI.TwoPointCorrelations.paddingRejectedMass_nonneg line 22
  3. lemma OAI.TwoPointCorrelations.paddingRejectedMass_residue_congr line 30
  4. lemma OAI.TwoPointCorrelations.ProhibitedPrimeFamily.positive_prime_padding_factor line 47
  5. theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_positive_padding_cut_cost line 59
  6. theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_tuple_padding_cut_cost line 90