OAI/NumberTheory/TwoPoint/Walks/RankSliceCost.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The finite choice of perfect rows, lit designation and offending column is negligible compared with the rank saving.

  1. lemma OAI.TwoPointCorrelations.rank_slice_cost_bound line 12
  2. theorem OAI.TwoPointCorrelations.eventually_rank_slice_decay line 42