OAI/NumberTheory/TwoPoint/Bounds/ShiftedPaddingBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The literal padding deletion bound when each product bin has its own averaging interval. The product-model cost is paid only once.

  1. theorem OAI.TwoPointCorrelations.BravermanDepth22Input.eventually_shifted_padding_deletion_uniform line 13
  2. theorem OAI.TwoPointCorrelations.BravermanDepth22Input.eventually_shifted_padding_deletion line 58