OAI/Dynamics/StandardMap/Coupling/CoarseConditionalBudget.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.HyperbolicCoding.coarse_conditional_budget line 16
  2. theorem OAI.HyperbolicCoding.finite_local_entropy_bridge line 46
  3. def OAI.HyperbolicCoding.MatrixCoupling.piCoupling line 90
  4. lemma OAI.HyperbolicCoding.MatrixCoupling.piCoupling_cost line 101
  5. theorem OAI.HyperbolicCoding.nonstationary_conditional_transport line 136
  6. def OAI.HyperbolicCoding.selectGaps line 196
  7. lemma OAI.HyperbolicCoding.retained_and_gaps_injective line 199
  8. lemma OAI.HyperbolicCoding.entropy_retained_chunks line 216
  9. theorem OAI.HyperbolicCoding.nonstationary_chunk_transport line 248
  10. def OAI.HyperbolicCoding.extractedChunk line 293
  11. lemma OAI.HyperbolicCoding.extractedChunk_measurable line 297
  12. lemma OAI.HyperbolicCoding.extractedChunk_name line 311
  13. theorem OAI.HyperbolicCoding.nonstationary_word_transport line 319
  14. lemma OAI.HyperbolicCoding.extractedChunk_entropy_defect line 356
  15. def OAI.HyperbolicCoding.fullBlock line 381
  16. lemma OAI.HyperbolicCoding.fullBlock_measurable line 385
  17. lemma OAI.HyperbolicCoding.fullBlock_name line 398
  18. lemma OAI.HyperbolicCoding.fullBlock_prefix_name line 406
  19. theorem OAI.HyperbolicCoding.nonstationary_conditional_word_transport line 422