OAI/NumberTheory/Ostmann/Construction/WordTransferTemplate.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

The concrete transfer system of word products and reconstructed pivots

  1. structure OAI.Ostmann.WordTransferNode line 14
  2. inductive OAI.Ostmann.WordTransferTemplate line 21
  3. abbrev OAI.Ostmann.WordTransferState line 26
  4. def OAI.Ostmann.WordTransferTemplate.state line 28
  5. def OAI.Ostmann.wordTransferLeft line 31
  6. def OAI.Ostmann.wordTransferRight line 35
  7. def OAI.Ostmann.wordTransferChildBound line 39
  8. def OAI.Ostmann.wordTransferPivotBound line 43
  9. def OAI.Ostmann.wordTransferLeftState line 47
  10. def OAI.Ostmann.wordTransferRightState line 51
  11. def OAI.Ostmann.wordTransferSystem line 55
  12. def OAI.Ostmann.NonzeroInternalFrequencies line 63
  13. theorem OAI.Ostmann.ValidTransferHistory.nonzero_internal line 67
  14. def OAI.Ostmann.wordTransferStep line 76
  15. def OAI.Ostmann.WordTransferTemplate.branching line 86
  16. theorem OAI.Ostmann.wordTransferStep_numerator line 94
  17. theorem OAI.Ostmann.wordTransferStep_valid line 104
  18. theorem OAI.Ostmann.wordTransferStep_apply line 113