OAI/NumberTheory/TwoPoint/Bounds/PrimeBlockDimension.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual tuple copies and the length-exp(103L) block fit the exp(106L) starting-vertex allowance in the matrix trace.

  1. lemma OAI.TwoPointCorrelations.primeTuple_card_le line 13
  2. theorem OAI.TwoPointCorrelations.actual_prime_block_dimension line 33