OAI/Dynamics/StandardMap/Coding/EntropyRateCodebook.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.HyperbolicCoding.entropy_rate_codebook line 16
  2. def OAI.HyperbolicCoding.Marker.HeadMarker line 64
  3. def OAI.HyperbolicCoding.Marker.MarkedBlock line 67
  4. def OAI.HyperbolicCoding.Marker.centeredWindow line 71
  5. def OAI.HyperbolicCoding.Marker.column line 74
  6. lemma OAI.HyperbolicCoding.Marker.column_centeredWindow line 77
  7. lemma OAI.HyperbolicCoding.Marker.self_column_centeredWindow line 84
  8. def OAI.HyperbolicCoding.Marker.candidates line 89
  9. lemma OAI.HyperbolicCoding.Marker.mem_candidates line 93
  10. def OAI.HyperbolicCoding.Marker.phase line 98
  11. lemma OAI.HyperbolicCoding.Marker.phase_eq_of_no_earlier line 102
  12. theorem OAI.HyperbolicCoding.Marker.phase_centeredWindow line 115
  13. def OAI.HyperbolicCoding.Marker.decodeWindow line 134
  14. theorem OAI.HyperbolicCoding.Marker.decode_centeredWindow line 138
  15. def OAI.HyperbolicCoding.Marker.markWord line 147
  16. lemma OAI.HyperbolicCoding.Marker.exists_multiple_window line 150
  17. lemma OAI.HyperbolicCoding.Marker.exists_guard line 162
  18. theorem OAI.HyperbolicCoding.Marker.markWord_isMarked line 172
  19. def OAI.HyperbolicCoding.Marker.reserved line 195
  20. lemma OAI.HyperbolicCoding.Marker.markWord_eq_outside line 199
  21. lemma OAI.HyperbolicCoding.Marker.reserved_card line 204
  22. lemma OAI.HyperbolicCoding.Marker.markWord_cost line 242
  23. lemma OAI.HyperbolicCoding.Marker.markWord_cost_le line 257
  24. lemma OAI.HyperbolicCoding.Marker.overwrite_fiber_card line 261
  25. lemma OAI.HyperbolicCoding.Marker.markWord_fiber_card line 278
  26. lemma OAI.HyperbolicCoding.marked_entropy_exponent_bound line 292
  27. theorem OAI.HyperbolicCoding.exists_entropy_slack_parameters line 330