OAI/Dynamics/StandardMap/Coding/FixedWindowCost.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HyperbolicCoding.blockWindow line 12
  2. def OAI.HyperbolicCoding.blockCenter line 14
  3. def OAI.HyperbolicCoding.decoderNameCost line 17
  4. def OAI.HyperbolicCoding.fixedWindowCost line 21
  5. lemma OAI.HyperbolicCoding.decoderNameCost_nonneg line 25
  6. lemma OAI.HyperbolicCoding.decoderNameCost_le_length line 28
  7. lemma OAI.HyperbolicCoding.fixedWindowCost_nonneg line 33
  8. lemma OAI.HyperbolicCoding.fixedWindowCost_le_one line 36
  9. lemma OAI.HyperbolicCoding.symbolCost_factor_le line 46
  10. lemma OAI.HyperbolicCoding.symbolCost_function_le_sum line 52
  11. lemma OAI.HyperbolicCoding.sum_blockWindow_cost_le line 61
  12. lemma OAI.HyperbolicCoding.decoderNameCost_modify line 78
  13. lemma OAI.HyperbolicCoding.fixedWindowCost_markWord line 88
  14. lemma OAI.HyperbolicCoding.finite_sum_injective_le line 111
  15. lemma OAI.HyperbolicCoding.fixedWindowCost_factor_triangle line 119
  16. lemma OAI.HyperbolicCoding.graph_window_word line 165
  17. lemma OAI.HyperbolicCoding.graph_fixedWindowCost_zero line 177
  18. theorem OAI.HyperbolicCoding.lift_joint_graph_transport line 194
  19. theorem OAI.HyperbolicCoding.fixed_window_fd_graph line 236
  20. theorem OAI.HyperbolicCoding.synchronized_cost_producer line 271
  21. lemma OAI.HyperbolicCoding.tower_error_integral line 343
  22. lemma OAI.HyperbolicCoding.boundedCost_left_triangle line 389
  23. theorem OAI.HyperbolicCoding.lift_cost_transport line 398