OAI/NumberTheory/TwoPoint/Bounds/ShiftedPaddingComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Each numerical pair can be sampled at its own additive shift. The common model is recovered by exact residue translation.

  1. theorem OAI.TwoPointCorrelations.BravermanDepth22Input.eventually_shifted_padding_comparison line 14