OAI/NumberTheory/TwoPoint/Bounds/ActualPaddingMarginal.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual padding estimates under the full tuple-and-padding residue law. All dependence on the tuple coordinates is removed by the proved product-law restriction identity.

  1. lemma OAI.TwoPointCorrelations.ProhibitedPrimeFamily.residue_average_padding_squares line 19
  2. lemma OAI.TwoPointCorrelations.ProhibitedPrimeFamily.residue_average_padding_degree_tail line 42
  3. theorem OAI.TwoPointCorrelations.ModFiveThetaInput.actual_family_padding_bin_square line 59
  4. theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_actual_family_padding_degree_tail line 94