OAI/MathematicalPhysics/NavierStokes/BalancedTransport/PrefixCoding.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BalancedTransport.Recorder.Exec.single line 14
  2. theorem OAI.BalancedTransport.Recorder.Exec.trans line 18
  3. theorem OAI.BalancedTransport.Recorder.preparation line 32
  4. theorem OAI.BalancedTransport.Recorder.preparation_blank_tail line 56
  5. theorem OAI.BalancedTransport.Recorder.checkpoint_length line 71
  6. theorem OAI.BalancedTransport.Recorder.checkpoint_stay line 83
  7. theorem OAI.BalancedTransport.Recorder.checkpoint_left line 97
  8. theorem OAI.BalancedTransport.Recorder.checkpoint_right line 111
  9. theorem OAI.BalancedTransport.Recorder.checkpoint_extend line 125
  10. def OAI.BalancedTransport.Coding.word line 149
  11. def OAI.BalancedTransport.Coding.prefixPoint line 153
  12. def OAI.BalancedTransport.Coding.interval line 156
  13. theorem OAI.BalancedTransport.Coding.word_nil line 159
  14. theorem OAI.BalancedTransport.Coding.prefix_nil line 161
  15. theorem OAI.BalancedTransport.Coding.prefix_cons line 164
  16. theorem OAI.BalancedTransport.Coding.word_append line 170
  17. theorem OAI.BalancedTransport.Coding.prefix_append line 178
  18. theorem OAI.BalancedTransport.Coding.prefix_mem_interval line 183
  19. theorem OAI.BalancedTransport.Coding.interval_eq_image line 192
  20. def OAI.BalancedTransport.Coding.replacement line 209
  21. theorem OAI.BalancedTransport.Coding.replacement_prefix line 212
  22. theorem OAI.BalancedTransport.Coding.replacement_interval line 219
  23. def OAI.BalancedTransport.Coding.scales line 227
  24. theorem OAI.BalancedTransport.Coding.determinant_one line 230
  25. theorem OAI.BalancedTransport.Coding.scales_positive line 238
  26. def OAI.BalancedTransport.Coding.stream line 241
  27. theorem OAI.BalancedTransport.Coding.stream_mem_unit line 244
  28. theorem OAI.BalancedTransport.Coding.stream_cons line 256
  29. theorem OAI.BalancedTransport.Coding.stream_append line 261
  30. theorem OAI.BalancedTransport.Coding.stream_append_mem_interval line 269
  31. theorem OAI.BalancedTransport.Coding.replacement_stream line 275
  32. theorem OAI.BalancedTransport.Coding.stream_mem_interior line 282
  33. theorem OAI.BalancedTransport.Coding.prefix_mem_unit line 297
  34. theorem OAI.BalancedTransport.Coding.interval_subset_unit line 309
  35. theorem OAI.BalancedTransport.Coding.prefix_gap line 316