OAI/NumberTheory/TwoPoint/Bounds/TraceCatalogMaps.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Injective encodings of the same trace catalog. Numerical-word estimates and column-wise forest estimates therefore have identical multiplicities.

  1. def OAI.TwoPointCorrelations.columnNatCode line 14
  2. lemma OAI.TwoPointCorrelations.columnNatCode_injective line 19
  3. def OAI.TwoPointCorrelations.columnStepCode line 29
  4. lemma OAI.TwoPointCorrelations.columnStepCode_word line 34
  5. lemma OAI.TwoPointCorrelations.columnStepCode_injective line 39
  6. lemma OAI.TwoPointCorrelations.largeUnlitCatalog_sum line 48
  7. lemma OAI.TwoPointCorrelations.trace_sum_image line 64