OAI/Computability/PerfectCompleteness/Decoding/LowerProjectedOriginalSuccessLemmas.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.LowerProjectedOriginalSuccess.kernelSuccess line 46
  2. def OAI.PerfectCompleteness.LowerProjectedOriginalSuccess.rawSuccess line 67
  3. theorem OAI.PerfectCompleteness.LowerProjectedOriginalSuccess.fiberSuccess_eq line 75
  4. theorem OAI.PerfectCompleteness.LowerProjectedOriginalSuccess.rawSuccess_eq_meanSuccess line 96
  5. theorem OAI.PerfectCompleteness.LowerProjectedOriginalSuccess.rawSuccess_square_le line 120
  6. abbrev OAI.PerfectCompleteness.LowerPhysicalFiberSuccess.path line 157
  7. abbrev OAI.PerfectCompleteness.LowerPhysicalFiberSuccess.Raw line 172
  8. def OAI.PerfectCompleteness.LowerPhysicalFiberSuccess.tape line 175
  9. def OAI.PerfectCompleteness.LowerPhysicalFiberSuccess.knownRaw line 181
  10. def OAI.PerfectCompleteness.LowerPhysicalFiberSuccess.knownBackground line 187
  11. theorem OAI.PerfectCompleteness.LowerPhysicalFiberSuccess.knownRaw_eq line 194
  12. def OAI.PerfectCompleteness.LowerPhysicalFiberSuccess.physicalSuccess line 212
  13. theorem OAI.PerfectCompleteness.LowerPhysicalFiberSuccess.physicalSuccess_eq_rawSuccess line 221
  14. theorem OAI.PerfectCompleteness.LowerPhysicalFiberSuccess.physicalSuccess_square_le line 236