OAI/Analysis/FreeWords/HaarTwistMoments.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KKFreeWords.letterBlock line 86
  2. def OAI.KKFreeWords.powerBlock line 89
  3. theorem OAI.KKFreeWords.letterBlock_value line 96
  4. theorem OAI.KKFreeWords.powerBlock_value line 101
  5. theorem OAI.KKFreeWords.letterBlock_mem line 119
  6. theorem OAI.KKFreeWords.powerBlock_mem line 131
  7. theorem OAI.KKFreeWords.powerBlock_ne_nil line 141
  8. theorem OAI.KKFreeWords.letterBlock_chain line 150
  9. theorem OAI.KKFreeWords.letterBlock_chain_append line 160
  10. theorem OAI.KKFreeWords.powerBlock_chain line 177
  11. theorem OAI.KKFreeWords.powerBlock_chain_append line 187
  12. def OAI.KKFreeWords.powerBlocks line 197
  13. theorem OAI.KKFreeWords.powerBlocks_value line 201
  14. theorem OAI.KKFreeWords.powerBlocks_mem line 215
  15. theorem OAI.KKFreeWords.powerBlocks_chain line 222
  16. theorem OAI.KKFreeWords.powerBlocks_ne_nil line 231
  17. theorem OAI.KKFreeWords.haar_twist_moments line 241