OAI/Dynamics/StandardMap/Coding/TypicalDecodableCoupling.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HyperbolicCoding.MatrixCoupling.extendRows line 12
  2. lemma OAI.HyperbolicCoding.MatrixCoupling.sum_extendRows line 16
  3. lemma OAI.HyperbolicCoding.MatrixCoupling.extendRows_nonneg line 21
  4. lemma OAI.HyperbolicCoding.MatrixCoupling.extendRows_sum line 29
  5. lemma OAI.HyperbolicCoding.MatrixCoupling.sum_extendRows_mul line 35
  6. def OAI.HyperbolicCoding.MatrixCoupling.replaceSub line 44
  7. lemma OAI.HyperbolicCoding.MatrixCoupling.replaceSub_cost line 63
  8. lemma OAI.HyperbolicCoding.MatrixCoupling.replaceSub_bounded_cost line 71
  9. def OAI.HyperbolicCoding.MatrixCoupling.divide line 101
  10. lemma OAI.HyperbolicCoding.MatrixCoupling.divide_cost line 109
  11. theorem OAI.HyperbolicCoding.MatrixCoupling.decodable_coupling_total line 113
  12. theorem OAI.HyperbolicCoding.MatrixCoupling.decodable_subtransport line 143
  13. def OAI.HyperbolicCoding.MatrixCoupling.rectangle line 173
  14. lemma OAI.HyperbolicCoding.MatrixCoupling.rectangle_weight_le line 182
  15. lemma OAI.HyperbolicCoding.MatrixCoupling.sum_subtype_weight_le line 190
  16. lemma OAI.HyperbolicCoding.MatrixCoupling.rectangle_right_bound line 200
  17. lemma OAI.HyperbolicCoding.MatrixCoupling.rectangle_mass line 208
  18. lemma OAI.HyperbolicCoding.MatrixCoupling.rectangle_mass_ge line 214
  19. theorem OAI.HyperbolicCoding.MatrixCoupling.decodable_typical_coupling line 235
  20. def OAI.HyperbolicCoding.pushWeight line 287
  21. lemma OAI.HyperbolicCoding.pushWeight_sum line 290
  22. lemma OAI.HyperbolicCoding.pushWeight_nonneg line 297
  23. lemma OAI.HyperbolicCoding.pushWeight_add line 304
  24. lemma OAI.HyperbolicCoding.pushWeight_bound line 312
  25. theorem OAI.HyperbolicCoding.typical_pushforward line 326
  26. def OAI.HyperbolicCoding.MatrixCoupling.pushRight line 388
  27. lemma OAI.HyperbolicCoding.MatrixCoupling.pushRight_cost line 402
  28. lemma OAI.HyperbolicCoding.mass_mem_finset line 415
  29. lemma OAI.HyperbolicCoding.mass_codebook_lower line 426
  30. theorem OAI.HyperbolicCoding.MatrixCoupling.decodable_after_sanitizing line 447
  31. theorem OAI.HyperbolicCoding.MatrixCoupling.marked_word_decodable_coupling line 479