OAI/Computability/PerfectCompleteness/Decoding/SourceQuestionCollisionTransportLemmas.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.SourceQuestionCollisionTransport.firstAnswer line 33
  2. def OAI.PerfectCompleteness.SourceQuestionCollisionTransport.secondAnswer line 46
  3. def OAI.PerfectCompleteness.SourceQuestionCollisionTransport.projection line 68
  4. def OAI.PerfectCompleteness.SourceQuestionCollisionTransport.globalRestricted line 79
  5. theorem OAI.PerfectCompleteness.SourceQuestionCollisionTransport.globalRestricted_imp_native line 94
  6. abbrev OAI.PerfectCompleteness.FixedSourceGlobalCollision.Questions line 201
  7. abbrev OAI.PerfectCompleteness.FixedSourceGlobalCollision.Table line 204
  8. abbrev OAI.PerfectCompleteness.FixedSourceGlobalCollision.TableFamily line 225
  9. def OAI.PerfectCompleteness.FixedSourceGlobalCollision.flag line 233
  10. abbrev OAI.PerfectCompleteness.FixedSourceGlobalCollision.Choice line 238
  11. def OAI.PerfectCompleteness.FixedSourceGlobalCollision.nativeProbability line 241
  12. theorem OAI.PerfectCompleteness.FixedSourceGlobalCollision.nativeProbability_eq_marked line 260
  13. def OAI.PerfectCompleteness.FixedSourceGlobalCollision.globalProbability line 304
  14. theorem OAI.PerfectCompleteness.FixedSourceGlobalCollision.globalProbability_le_marked line 318
  15. def OAI.PerfectCompleteness.FixedSourceGlobalCollision.localTables line 336
  16. def OAI.PerfectCompleteness.FixedSourceGlobalCollision.localProbability line 341
  17. theorem OAI.PerfectCompleteness.FixedSourceGlobalCollision.globalProbability_eq_local line 354
  18. theorem OAI.PerfectCompleteness.FixedSourceGlobalCollision.mean_global_le line 378
  19. theorem OAI.PerfectCompleteness.FixedSourceGlobalCollision.mean_local_le line 397