OAI/NumberTheory/TwoPoint/Bounds/ShiftedRareComparison.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Rare-site row comparison with a distinct additive shift at every numerical pair, in particular the opposite endpoint of that edge.

  1. def OAI.TwoPointCorrelations.shiftedProhibitedRow line 15
  2. theorem OAI.TwoPointCorrelations.BravermanDepth22Input.eventually_shifted_prohibited_row_comparison line 22