OAI/Analysis/FourierLLogL/Compress/Blocks.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Indexed blocks of letters

  1. abbrev OAI.FourierLLogL.Compress.Letters line 12
  2. abbrev OAI.FourierLLogL.Compress.WordSample line 13
  3. def OAI.FourierLLogL.Compress.offset line 17
  4. def OAI.FourierLLogL.Compress.readBlock line 19
  5. def OAI.FourierLLogL.Compress.prefixB line 21
  6. def OAI.FourierLLogL.Compress.readLetter line 22
  7. lemma OAI.FourierLLogL.Compress.offset_injective line 24
  8. lemma OAI.FourierLLogL.Compress.prefix_partition line 30
  9. lemma OAI.FourierLLogL.Compress.prefix_last_partition line 48
  10. lemma OAI.FourierLLogL.Compress.prefix_zero line 57
  11. lemma OAI.FourierLLogL.Compress.prefix_all line 60
  12. lemma OAI.FourierLLogL.Compress.block_cut line 64
  13. lemma OAI.FourierLLogL.Compress.block_in_prefix line 68
  14. def OAI.FourierLLogL.Compress.splitIx line 73
  15. lemma OAI.FourierLLogL.Compress.splitIx_left line 76
  16. lemma OAI.FourierLLogL.Compress.splitIx_right line 82
  17. lemma OAI.FourierLLogL.Compress.lift_perm line 94
  18. def OAI.FourierLLogL.Compress.subSample line 106
  19. lemma OAI.FourierLLogL.Compress.exch_subSample line 109
  20. lemma OAI.FourierLLogL.Compress.exch_subSample_cond line 118
  21. lemma OAI.FourierLLogL.Compress.prefix_bill line 141