OAI/Computability/PerfectCompleteness/Machines/OwnInputReferenceLemmas.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.OwnInputReference.F2 line 16
  2. abbrev OAI.PerfectCompleteness.OwnInputReference.UpperSpace line 24
  3. abbrev OAI.PerfectCompleteness.OwnInputReference.UpperVector line 25
  4. abbrev OAI.PerfectCompleteness.OwnInputReference.LowerVector line 26
  5. abbrev OAI.PerfectCompleteness.OwnInputReference.OtherNodes line 27
  6. structure OAI.PerfectCompleteness.OwnInputReference.Cut line 29
  7. theorem OAI.PerfectCompleteness.OwnInputReference.Cut.upper_ne_lower line 36
  8. theorem OAI.PerfectCompleteness.OwnInputReference.Cut.family_eq line 42
  9. abbrev OAI.PerfectCompleteness.OwnInputReference.OtherArrays line 50
  10. structure OAI.PerfectCompleteness.OwnInputReference.Exterior line 54
  11. instance OAI.PerfectCompleteness.OwnInputReference.exteriorFinite line 58
  12. instance OAI.PerfectCompleteness.OwnInputReference.exteriorFintype line 65
  13. structure OAI.PerfectCompleteness.OwnInputReference.Input line 69
  14. def OAI.PerfectCompleteness.OwnInputReference.readInput line 74
  15. abbrev OAI.PerfectCompleteness.OwnInputReference.SideOutput line 82
  16. def OAI.PerfectCompleteness.OwnInputReference.sideFunction line 85
  17. def OAI.PerfectCompleteness.OwnInputReference.knownOutput line 91
  18. def OAI.PerfectCompleteness.OwnInputReference.query line 96
  19. def OAI.PerfectCompleteness.OwnInputReference.sampledQuery line 105
  20. theorem OAI.PerfectCompleteness.OwnInputReference.query_readInput_hidden line 116
  21. def OAI.PerfectCompleteness.OwnInputReference.response line 130
  22. theorem OAI.PerfectCompleteness.OwnInputReference.response_readInput_hidden line 136
  23. def OAI.PerfectCompleteness.OwnInputReference.referenceLaw line 151
  24. abbrev OAI.PerfectCompleteness.OwnInputReference.ScalarSample line 155
  25. instance OAI.PerfectCompleteness.OwnInputReference.scalarSampleFintype line 158
  26. abbrev OAI.PerfectCompleteness.OwnInputReference.RawSample line 164
  27. instance OAI.PerfectCompleteness.OwnInputReference.rawSampleFintype line 169
  28. def OAI.PerfectCompleteness.OwnInputReference.rawLaw line 177
  29. def OAI.PerfectCompleteness.OwnInputReference.inputEvent line 183
  30. theorem OAI.PerfectCompleteness.OwnInputReference.conditional_referenceLaw line 190
  31. instance OAI.PerfectCompleteness.OwnInputReference.frequencyFintype line 208
  32. def OAI.PerfectCompleteness.OwnInputReference.heavyList line 213
  33. theorem OAI.PerfectCompleteness.OwnInputReference.mem_heavyList line 223
  34. abbrev OAI.PerfectCompleteness.OwnInputCanonicalQuery.F2 line 244
  35. abbrev OAI.PerfectCompleteness.OwnInputCanonicalQuery.CanonicalOutput line 252
  36. def OAI.PerfectCompleteness.OwnInputCanonicalQuery.reorder line 256
  37. theorem OAI.PerfectCompleteness.OwnInputCanonicalQuery.reorder_injective line 262
  38. def OAI.PerfectCompleteness.OwnInputCanonicalQuery.unreorder line 276
  39. theorem OAI.PerfectCompleteness.OwnInputCanonicalQuery.reorder_unreorder line 283
  40. def OAI.PerfectCompleteness.OwnInputCanonicalQuery.outputEquiv line 294
  41. def OAI.PerfectCompleteness.OwnInputCanonicalQuery.exteriorOf line 302
  42. def OAI.PerfectCompleteness.OwnInputCanonicalQuery.assemble line 306
  43. theorem OAI.PerfectCompleteness.OwnInputCanonicalQuery.assemble_upper line 312
  44. theorem OAI.PerfectCompleteness.OwnInputCanonicalQuery.assemble_lower line 318
  45. theorem OAI.PerfectCompleteness.OwnInputCanonicalQuery.assemble_other line 324
  46. theorem OAI.PerfectCompleteness.OwnInputCanonicalQuery.assemble_original line 331
  47. def OAI.PerfectCompleteness.OwnInputCanonicalQuery.canonicalQuery line 342
  48. theorem OAI.PerfectCompleteness.OwnInputCanonicalQuery.sampledQuery_eq_reorder line 345
  49. theorem OAI.PerfectCompleteness.OwnInputCanonicalQuery.numbered_sampledQuery_eq line 376
  50. theorem OAI.PerfectCompleteness.OwnInputCanonicalQuery.sampled_key_eq line 388
  51. theorem OAI.PerfectCompleteness.OwnInputCanonicalQuery.sampled_response_eq line 402
  52. theorem OAI.PerfectCompleteness.OwnInputCanonicalQuery.response_readInput_hidden_eq line 419
  53. theorem OAI.PerfectCompleteness.OwnInputCanonicalQuery.response_readInput_hidden_arrays line 436