OAI/Computability/PerfectCompleteness/Sampling/MetadataFreeLaw.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.MetadataFreeLaw.tape_weight_eq line 19
  2. theorem OAI.PerfectCompleteness.MetadataFreeLaw.tapeLaw_transport line 46
  3. abbrev OAI.PerfectCompleteness.MetadataFreeLaw.SignedOutcome line 59
  4. def OAI.PerfectCompleteness.MetadataFreeLaw.signedLaw line 64
  5. def OAI.PerfectCompleteness.MetadataFreeLaw.signedRationalLaw line 71
  6. theorem OAI.PerfectCompleteness.MetadataFreeLaw.signedLaw_positive line 80
  7. def OAI.PerfectCompleteness.MetadataFreeLaw.encodeOutcome line 86
  8. theorem OAI.PerfectCompleteness.MetadataFreeLaw.raw_weight_eq line 91
  9. theorem OAI.PerfectCompleteness.MetadataFreeLaw.raw_weight_rational line 113
  10. def OAI.PerfectCompleteness.MetadataFreeLaw.rawEquiv line 124
  11. theorem OAI.PerfectCompleteness.MetadataFreeLaw.rawLaw_transport line 144