OAI/NumberTheory/TwoPoint/Bounds/RecordedWitnessSegments.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Every actual main/witness family is represented in the finite segment catalog.

  1. def OAI.TwoPointCorrelations.recordedWitnessWord line 11
  2. theorem OAI.TwoPointCorrelations.recorded_witness_segments line 14