OAI/Computability/PerfectCompleteness/Decoding/DecoderContraction.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.DecoderContraction.F2 line 16
  2. def OAI.PerfectCompleteness.DecoderContraction.chosenRow line 21
  3. theorem OAI.PerfectCompleteness.DecoderContraction.chosenRow_value_one line 25
  4. def OAI.PerfectCompleteness.DecoderContraction.contract line 29
  5. theorem OAI.PerfectCompleteness.DecoderContraction.contract_eq line 33
  6. theorem OAI.PerfectCompleteness.DecoderContraction.contract_eq_zero line 38
  7. def OAI.PerfectCompleteness.DecoderContraction.baseFrequency line 43
  8. theorem OAI.PerfectCompleteness.DecoderContraction.baseFrequency_tmul line 47
  9. theorem OAI.PerfectCompleteness.DecoderContraction.contract_baseFrequency line 52
  10. def OAI.PerfectCompleteness.DecoderContraction.errorSpace line 61
  11. theorem OAI.PerfectCompleteness.DecoderContraction.mem_errorSpace line 77
  12. theorem OAI.PerfectCompleteness.DecoderContraction.equationSpace_le_errorSpace line 81
  13. theorem OAI.PerfectCompleteness.DecoderContraction.contract_sub_mem line 86
  14. theorem OAI.PerfectCompleteness.DecoderContraction.contract_sub_mem_of_equationSpace line 99
  15. theorem OAI.PerfectCompleteness.DecoderContraction.factored_mem_errorSpace line 107
  16. def OAI.PerfectCompleteness.DecoderContraction.descendantSquareEmbedding line 118
  17. theorem OAI.PerfectCompleteness.DecoderContraction.descendantSquareEmbedding_apply line 127
  18. theorem OAI.PerfectCompleteness.DecoderContraction.descendantSquareEmbedding_injective line 132
  19. def OAI.PerfectCompleteness.DecoderContraction.descendantFunctional line 140
  20. def OAI.PerfectCompleteness.DecoderContraction.descendantForm line 146
  21. theorem OAI.PerfectCompleteness.DecoderContraction.descendantFunctional_contract_eq line 152