OAI/NumberTheory/TwoPoint/Walks/WitnessRecordBudget.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

One explicit polynomial budget covers all concatenated witness lengths and prime slots.

  1. def OAI.TwoPointCorrelations.witnessRecordBudget line 12

    Source documentation

    The bound includes the main length and number of witnesses as well as all prime slots.

    def witnessRecordBudget (D J M n : ℕ) : ℕ := D * (J + M) + D + n
  2. lemma OAI.TwoPointCorrelations.witnessRecordBudget_length line 14
  3. lemma OAI.TwoPointCorrelations.witnessRecordBudget_witnesses line 18
  4. lemma OAI.TwoPointCorrelations.witnessRecordBudget_slots line 22
  5. lemma OAI.TwoPointCorrelations.eventually_witnessRecordBudget line 26