OAI/NumberTheory/TwoPoint/Bounds/PaddedListCode.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Fixed-length code slots for finite lists with a bounded length.

  1. def OAI.TwoPointCorrelations.paddedListCode line 12
  2. theorem OAI.TwoPointCorrelations.paddedListCode_ofFn line 17