OAI/Dynamics/StandardMap/Coding/DecodedTowerCopy.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HyperbolicCoding.prefixNameCost line 15
  2. lemma OAI.HyperbolicCoding.nameCost_le_prefixNameCost line 21
  3. theorem OAI.HyperbolicCoding.realize_prefix_tower_coupling line 32
  4. lemma OAI.HyperbolicCoding.prefix_tower_decoder_error line 80
  5. lemma OAI.HyperbolicCoding.ae_observation_of_zero_bad_mass line 105
  6. theorem OAI.HyperbolicCoding.decoded_prefix_tower_copy line 123
  7. lemma OAI.HyperbolicCoding.prefixNameCost_nonneg line 157
  8. lemma OAI.HyperbolicCoding.prefixNameCost_le_length line 161
  9. lemma OAI.HyperbolicCoding.prefixNameCost_modify line 167
  10. def OAI.HyperbolicCoding.normalizedPrefixCost line 179
  11. lemma OAI.HyperbolicCoding.normalizedPrefixCost_nonneg line 182
  12. lemma OAI.HyperbolicCoding.normalizedPrefixCost_le_one line 185
  13. lemma OAI.HyperbolicCoding.normalizedPrefixCost_markWord line 190
  14. theorem OAI.HyperbolicCoding.synchronized_codebook_producer line 211
  15. theorem OAI.HyperbolicCoding.unsanitize_tower line 282
  16. theorem OAI.HyperbolicCoding.unsanitize_marked_tower line 311
  17. lemma OAI.HyperbolicCoding.word_disagreement_le line 327
  18. lemma OAI.HyperbolicCoding.word_lawClose_of_repaint line 352
  19. lemma OAI.HyperbolicCoding.normalizedPrefixCost_left_triangle line 374
  20. lemma OAI.HyperbolicCoding.tower_real_mass_le_one line 387
  21. lemma OAI.HyperbolicCoding.tower_suffix_mass_le line 398
  22. theorem OAI.HyperbolicCoding.lift_decoded_prefix_transport line 408