OAI/NumberTheory/TwoPoint/Walks/TuplePaddingDeletion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Sum the padding-cut estimate over all tuple divisors. The center of the logarithmic bins may depend on the tuple, as required for the actual product d*q bins.

  1. theorem OAI.TwoPointCorrelations.BravermanDepth22Input.eventually_integer_tuple_padding_deletion line 15