OAI/Computability/PerfectCompleteness/Decoding/RightDecoderLemmas.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.RightDecoder.F2 line 15
  2. def OAI.PerfectCompleteness.RightDecoder.law line 39
  3. theorem OAI.PerfectCompleteness.RightDecoder.probability_law line 44
  4. theorem OAI.PerfectCompleteness.RightDecoder.success_lower line 53
  5. theorem OAI.PerfectCompleteness.RightDecoder.coset_lower line 66
  6. theorem OAI.PerfectCompleteness.RightDecoder.coset_lower_of_balanced line 84
  7. abbrev OAI.PerfectCompleteness.RightDecoderDescendant.F2 line 128
  8. def OAI.PerfectCompleteness.RightDecoderDescendant.leafEquiv line 136
  9. def OAI.PerfectCompleteness.RightDecoderDescendant.restriction line 142
  10. theorem OAI.PerfectCompleteness.RightDecoderDescendant.restriction_restrictNode line 146
  11. def OAI.PerfectCompleteness.RightDecoderDescendant.squareEmbedding line 162
  12. theorem OAI.PerfectCompleteness.RightDecoderDescendant.squareEmbedding_apply line 169
  13. theorem OAI.PerfectCompleteness.RightDecoderDescendant.squareEmbedding_restrictNode line 174
  14. theorem OAI.PerfectCompleteness.RightDecoderDescendant.squareEmbedding_injective line 180
  15. def OAI.PerfectCompleteness.RightDecoderDescendant.functional line 188
  16. abbrev OAI.PerfectCompleteness.RightDecoderDescendant.Form line 192
  17. def OAI.PerfectCompleteness.RightDecoderDescendant.form line 194
  18. theorem OAI.PerfectCompleteness.RightDecoderDescendant.form_apply line 198
  19. theorem OAI.PerfectCompleteness.RightDecoderDescendant.form_evaluation line 204
  20. theorem OAI.PerfectCompleteness.RightDecoderDescendant.form_evaluation_restrictNode line 211
  21. theorem OAI.PerfectCompleteness.RightDecoderDescendant.functional_eq_of_sub_mem line 218
  22. theorem OAI.PerfectCompleteness.RightDecoderDescendant.form_eq_of_sub_mem line 232
  23. def OAI.PerfectCompleteness.RightDecoderDescendant.formLaw line 264
  24. theorem OAI.PerfectCompleteness.RightDecoderDescendant.probability_formLaw line 268
  25. theorem OAI.PerfectCompleteness.RightDecoderDescendant.coset_probability_le_form_probability line 275
  26. theorem OAI.PerfectCompleteness.RightDecoderDescendant.form_contract_eq line 290
  27. theorem OAI.PerfectCompleteness.RightDecoderDescendant.form_success_lower_of_balanced line 303