OAI/Dynamics/StandardMap/Coupling/FiniteConditionalLawTests.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HyperbolicCoding.conditional_entropy_law_test line 15
  2. lemma OAI.HyperbolicCoding.conditional_entropy_law_test_uniform line 39
  3. lemma OAI.HyperbolicCoding.marginal_joint_test line 66
  4. lemma OAI.HyperbolicCoding.independence_joint_test line 77
  5. lemma OAI.HyperbolicCoding.wordPack_apply_coord line 102
  6. lemma OAI.HyperbolicCoding.wordPack_symm_coord line 105
  7. lemma OAI.HyperbolicCoding.fullBlock_packed line 110
  8. def OAI.HyperbolicCoding.suffixPrefix line 117
  9. def OAI.HyperbolicCoding.vectorFuture line 120
  10. lemma OAI.HyperbolicCoding.fullBlock_local_future line 123
  11. lemma OAI.HyperbolicCoding.block_inner_future_lt line 134
  12. lemma OAI.HyperbolicCoding.vectorFuture_inside_block line 140
  13. lemma OAI.HyperbolicCoding.word_vectorFuture line 154
  14. lemma OAI.HyperbolicCoding.nameCost_wordPack line 163
  15. lemma OAI.HyperbolicCoding.fullBlock_nested_head line 168
  16. lemma OAI.HyperbolicCoding.fullBlock_nested_future line 178
  17. lemma OAI.HyperbolicCoding.map_word_coordinate line 200
  18. lemma OAI.HyperbolicCoding.map_word_head_future line 207
  19. lemma OAI.HyperbolicCoding.block_law_head_test line 226
  20. lemma OAI.HyperbolicCoding.block_law_local_test line 239
  21. lemma OAI.HyperbolicCoding.eventually_conditional_single_test line 255
  22. lemma OAI.HyperbolicCoding.remote_law_as_blocks line 265
  23. lemma OAI.HyperbolicCoding.lawClose_one line 289
  24. def OAI.HyperbolicCoding.insideCoarse line 296
  25. def OAI.HyperbolicCoding.extendedCoarse line 305
  26. lemma OAI.HyperbolicCoding.extendedCoarse_at line 309
  27. lemma OAI.HyperbolicCoding.insideCoarse_good line 314
  28. lemma OAI.HyperbolicCoding.insideCoarse_bad line 320
  29. def OAI.HyperbolicCoding.boundaryLoss line 325
  30. lemma OAI.HyperbolicCoding.boundaryLoss_nonneg line 328
  31. lemma OAI.HyperbolicCoding.boundary_count_le line 332
  32. lemma OAI.HyperbolicCoding.boundaryLoss_sum_le line 360
  33. def OAI.HyperbolicCoding.nestedOutput line 378
  34. lemma OAI.HyperbolicCoding.nestedOutput_measurable line 382
  35. lemma OAI.HyperbolicCoding.nestedOutput_head line 387
  36. lemma OAI.HyperbolicCoding.nestedOutput_future line 393
  37. theorem OAI.HyperbolicCoding.block_recoding_word_transport line 403