OAI/Computability/PerfectCompleteness/Foundations/TupleIndexEmitterLemmas.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.PerfectCompleteness.TupleIndexEmitter.Tape line 18
  2. inductive OAI.PerfectCompleteness.TupleIndexEmitter.Label line 25
  3. def OAI.PerfectCompleteness.TupleIndexEmitter.labelAt line 33
  4. def OAI.PerfectCompleteness.TupleIndexEmitter.program line 37
  5. def OAI.PerfectCompleteness.TupleIndexEmitter.prefixWords line 45
  6. theorem OAI.PerfectCompleteness.TupleIndexEmitter.prefixWords_zero line 48
  7. theorem OAI.PerfectCompleteness.TupleIndexEmitter.prefixWords_succ line 51
  8. theorem OAI.PerfectCompleteness.TupleIndexEmitter.prefixWords_all line 57
  9. def OAI.PerfectCompleteness.TupleIndexEmitter.prefixBudget line 61
  10. theorem OAI.PerfectCompleteness.TupleIndexEmitter.prefixBudget_zero line 64
  11. theorem OAI.PerfectCompleteness.TupleIndexEmitter.prefixBudget_succ line 67
  12. theorem OAI.PerfectCompleteness.TupleIndexEmitter.prefixBudget_all line 73
  13. def OAI.PerfectCompleteness.TupleIndexEmitter.outputTapes line 80
  14. theorem OAI.PerfectCompleteness.TupleIndexEmitter.outputTapes_output line 84
  15. theorem OAI.PerfectCompleteness.TupleIndexEmitter.outputTapes_current line 88
  16. theorem OAI.PerfectCompleteness.TupleIndexEmitter.outputTapes_scratch line 93
  17. theorem OAI.PerfectCompleteness.TupleIndexEmitter.outputTapes_extra line 97
  18. theorem OAI.PerfectCompleteness.TupleIndexEmitter.outputTapes_nil line 102
  19. theorem OAI.PerfectCompleteness.TupleIndexEmitter.outputTapes_outputTapes line 106
  20. def OAI.PerfectCompleteness.TupleIndexEmitter.prefixInTimeFor line 111
  21. def OAI.PerfectCompleteness.TupleIndexEmitter.prefixInTime line 162
  22. def OAI.PerfectCompleteness.TupleIndexEmitter.emitInTimeFor line 174
  23. def OAI.PerfectCompleteness.TupleIndexEmitter.emitInTime line 195
  24. theorem OAI.PerfectCompleteness.TupleIndexEmitter.budget_eq line 207
  25. def OAI.PerfectCompleteness.TupleIndexEmitter.placedEmitInTime line 220
  26. def OAI.PerfectCompleteness.TupleIndexEmitter.haltInTime line 235
  27. def OAI.PerfectCompleteness.TupleIndexEmitter.machine line 252
  28. def OAI.PerfectCompleteness.UsefulMark.marginalMass line 276
  29. def OAI.PerfectCompleteness.UsefulMark.lowerFiberMass line 279
  30. def OAI.PerfectCompleteness.UsefulMark.conditionalLower line 283
  31. def OAI.PerfectCompleteness.UsefulMark.useful line 287
  32. theorem OAI.PerfectCompleteness.UsefulMark.useful_iff line 292
  33. theorem OAI.PerfectCompleteness.UsefulMark.marginalMass_nonneg line 299
  34. theorem OAI.PerfectCompleteness.UsefulMark.lowerFiberMass_nonneg line 303
  35. theorem OAI.PerfectCompleteness.UsefulMark.lowerFiberMass_le_marginalMass line 308
  36. theorem OAI.PerfectCompleteness.UsefulMark.lowerFiberMass_eq_zero line 313
  37. theorem OAI.PerfectCompleteness.UsefulMark.conditionalLower_eq_zero line 320
  38. theorem OAI.PerfectCompleteness.UsefulMark.marginalMass_eq_pushforward_weight line 325
  39. theorem OAI.PerfectCompleteness.UsefulMark.sum_marginalMass line 329
  40. theorem OAI.PerfectCompleteness.UsefulMark.probability_eq_sum_fibers line 334
  41. theorem OAI.PerfectCompleteness.UsefulMark.probability_mark_eq_sum line 342
  42. theorem OAI.PerfectCompleteness.UsefulMark.lowerFiberMass_le_of_not_useful line 361
  43. theorem OAI.PerfectCompleteness.UsefulMark.discarded_lower_le line 375
  44. theorem OAI.PerfectCompleteness.UsefulMark.joint_le_discarded_add_marked line 390
  45. theorem OAI.PerfectCompleteness.UsefulMark.useful_upper_ge_sub line 402
  46. theorem OAI.PerfectCompleteness.UsefulMark.useful_upper_ge_half line 410
  47. def OAI.PerfectCompleteness.PositiveFiberMass.jMass line 432
  48. def OAI.PerfectCompleteness.PositiveFiberMass.matchMass line 435
  49. def OAI.PerfectCompleteness.PositiveFiberMass.conditionalMatch line 439
  50. def OAI.PerfectCompleteness.PositiveFiberMass.goodRecord line 443
  51. theorem OAI.PerfectCompleteness.PositiveFiberMass.goodRecord_iff line 448
  52. theorem OAI.PerfectCompleteness.PositiveFiberMass.jMass_nonneg line 455
  53. theorem OAI.PerfectCompleteness.PositiveFiberMass.matchMass_nonneg line 460
  54. theorem OAI.PerfectCompleteness.PositiveFiberMass.matchMass_le_jMass line 465
  55. theorem OAI.PerfectCompleteness.PositiveFiberMass.matchMass_eq_zero line 474
  56. theorem OAI.PerfectCompleteness.PositiveFiberMass.matchMass_le_of_not_goodRecord line 481
  57. theorem OAI.PerfectCompleteness.PositiveFiberMass.fiber_difference_le_good_mass line 497
  58. theorem OAI.PerfectCompleteness.PositiveFiberMass.sum_jMass line 509
  59. theorem OAI.PerfectCompleteness.PositiveFiberMass.sum_matchMass line 513
  60. theorem OAI.PerfectCompleteness.PositiveFiberMass.difference_eq_sum line 519
  61. theorem OAI.PerfectCompleteness.PositiveFiberMass.difference_le_good_mass line 525
  62. theorem OAI.PerfectCompleteness.PositiveFiberMass.good_mass_ge_difference_lower_bound line 535
  63. theorem OAI.PerfectCompleteness.PositiveFiberMass.conditional_probability_ge_of_goodRecord line 543
  64. theorem OAI.PerfectCompleteness.UsefulAdvice.marked_probability_eq_sum line 574
  65. theorem OAI.PerfectCompleteness.UsefulAdvice.useful_fiber_lower line 582
  66. theorem OAI.PerfectCompleteness.UsefulAdvice.marked_lower_bound line 588
  67. theorem OAI.PerfectCompleteness.UsefulAdvice.product_probability_advice_first line 603
  68. theorem OAI.PerfectCompleteness.UsefulAdvice.independent_advice_lower_bound line 622
  69. theorem OAI.PerfectCompleteness.UsefulAdvice.independent_advice_predicts line 634
  70. theorem OAI.PerfectCompleteness.PredictionDifference.scalar_bound line 660
  71. theorem OAI.PerfectCompleteness.PredictionDifference.of_observed_variation line 682
  72. theorem OAI.PerfectCompleteness.PredictionDifference.of_original_usefulness line 714