OAI/Computability/PerfectCompleteness/Foundations/HierarchicalAdviceExperimentLemmas.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PerfectCompleteness.HierarchicalAdviceExperiment.Experiment line 24
  2. abbrev OAI.PerfectCompleteness.HierarchicalAdviceExperiment.Background line 38
  3. abbrev OAI.PerfectCompleteness.HierarchicalAdviceExperiment.Input line 42
  4. abbrev OAI.PerfectCompleteness.HierarchicalAdviceExperiment.Value line 53
  5. abbrev OAI.PerfectCompleteness.HierarchicalAdviceExperiment.Advice line 57
  6. abbrev OAI.PerfectCompleteness.HierarchicalAdviceExperiment.Coarse line 58
  7. abbrev OAI.PerfectCompleteness.HierarchicalAdviceExperiment.ReferenceSample line 59
  8. def OAI.PerfectCompleteness.HierarchicalAdviceExperiment.background line 62
  9. def OAI.PerfectCompleteness.HierarchicalAdviceExperiment.matrix line 65
  10. def OAI.PerfectCompleteness.HierarchicalAdviceExperiment.coarse line 68
  11. def OAI.PerfectCompleteness.HierarchicalAdviceExperiment.lowerEvent line 71
  12. def OAI.PerfectCompleteness.HierarchicalAdviceExperiment.table line 75
  13. def OAI.PerfectCompleteness.HierarchicalAdviceExperiment.J line 80
  14. def OAI.PerfectCompleteness.HierarchicalAdviceExperiment.I line 83
  15. def OAI.PerfectCompleteness.HierarchicalAdviceExperiment.adviceLaw line 86
  16. def OAI.PerfectCompleteness.HierarchicalAdviceExperiment.originalLaw line 89
  17. def OAI.PerfectCompleteness.HierarchicalAdviceExperiment.observe line 92
  18. def OAI.PerfectCompleteness.HierarchicalAdviceExperiment.referenceLaw line 95
  19. def OAI.PerfectCompleteness.HierarchicalAdviceExperiment.referenceObserve line 99
  20. def OAI.PerfectCompleteness.HierarchicalAdviceExperiment.prediction line 102
  21. theorem OAI.PerfectCompleteness.HierarchicalAdviceExperiment.I_implies_mark line 107
  22. theorem OAI.PerfectCompleteness.HierarchicalAdviceExperiment.lower_I_implies_prediction line 118
  23. theorem OAI.PerfectCompleteness.HierarchicalAdviceExperiment.prediction_implies_J line 129
  24. theorem OAI.PerfectCompleteness.HierarchicalAdviceExperiment.reference_J_mass_ge line 135
  25. theorem OAI.PerfectCompleteness.HierarchicalAdviceExperiment.prediction_difference line 155
  26. theorem OAI.PerfectCompleteness.HierarchicalAdviceExperiment.prediction_difference_le_good_mass line 182
  27. abbrev OAI.PerfectCompleteness.HierarchicalAdviceFamily.Background line 225
  28. abbrev OAI.PerfectCompleteness.HierarchicalAdviceFamily.Input line 231
  29. abbrev OAI.PerfectCompleteness.HierarchicalAdviceFamily.Row line 232
  30. abbrev OAI.PerfectCompleteness.HierarchicalAdviceFamily.Value line 233
  31. def OAI.PerfectCompleteness.HierarchicalAdviceFamily.table line 244
  32. abbrev OAI.PerfectCompleteness.HierarchicalAdviceFamily.OriginalSample line 248
  33. abbrev OAI.PerfectCompleteness.HierarchicalAdviceFamily.Observation line 251
  34. abbrev OAI.PerfectCompleteness.HierarchicalAdviceFamily.ReferenceSample line 258
  35. def OAI.PerfectCompleteness.HierarchicalAdviceFamily.originalLaw line 261
  36. def OAI.PerfectCompleteness.HierarchicalAdviceFamily.observe line 265
  37. def OAI.PerfectCompleteness.HierarchicalAdviceFamily.backgroundLaw line 268
  38. def OAI.PerfectCompleteness.HierarchicalAdviceFamily.referenceLaw line 273
  39. def OAI.PerfectCompleteness.HierarchicalAdviceFamily.referenceObserve line 278
  40. def OAI.PerfectCompleteness.HierarchicalAdviceFamily.J line 281
  41. def OAI.PerfectCompleteness.HierarchicalAdviceFamily.I line 284
  42. def OAI.PerfectCompleteness.HierarchicalAdviceFamily.prediction line 287
  43. theorem OAI.PerfectCompleteness.HierarchicalAdviceFamily.reference_J line 291
  44. theorem OAI.PerfectCompleteness.HierarchicalAdviceFamily.reference_I line 296
  45. theorem OAI.PerfectCompleteness.HierarchicalAdviceFamily.reference_J_mass_ge line 300
  46. theorem OAI.PerfectCompleteness.HierarchicalAdviceFamily.reference_I_mass_ge line 324
  47. theorem OAI.PerfectCompleteness.HierarchicalAdviceFamily.lower_I_implies_prediction line 344
  48. theorem OAI.PerfectCompleteness.HierarchicalAdviceFamily.prediction_difference line 351
  49. def OAI.PerfectCompleteness.HierarchicalOwnPrediction.input line 402
  50. abbrev OAI.PerfectCompleteness.HierarchicalOwnPrediction.hidden line 407
  51. theorem OAI.PerfectCompleteness.HierarchicalOwnPrediction.response_eq_rightUpper line 409
  52. def OAI.PerfectCompleteness.HierarchicalOwnPrediction.correction line 420
  53. theorem OAI.PerfectCompleteness.HierarchicalOwnPrediction.correction_eq_of_background_eq line 433
  54. def OAI.PerfectCompleteness.HierarchicalOwnPrediction.nativeCorrection line 446
  55. def OAI.PerfectCompleteness.HierarchicalOwnPrediction.visibleOffset line 451
  56. theorem OAI.PerfectCompleteness.HierarchicalOwnPrediction.affinePrediction_eq_tensor line 458
  57. theorem OAI.PerfectCompleteness.HierarchicalOwnPrediction.prediction_iff_own_tensor line 471
  58. abbrev OAI.PerfectCompleteness.HierarchicalUsefulFamily.Sample line 505
  59. def OAI.PerfectCompleteness.HierarchicalUsefulFamily.originalLaw line 507
  60. def OAI.PerfectCompleteness.HierarchicalUsefulFamily.jointEvent line 510
  61. def OAI.PerfectCompleteness.HierarchicalUsefulFamily.usefulEvent line 513
  62. theorem OAI.PerfectCompleteness.HierarchicalUsefulFamily.usefulEvent_eq_table_defined line 520
  63. theorem OAI.PerfectCompleteness.HierarchicalUsefulFamily.joint_probability_eq_mean line 529
  64. theorem OAI.PerfectCompleteness.HierarchicalUsefulFamily.useful_probability_eq_mean line 537
  65. theorem OAI.PerfectCompleteness.HierarchicalUsefulFamily.mean_useful_probability_ge_sub line 545
  66. theorem OAI.PerfectCompleteness.HierarchicalUsefulFamily.useful_probability_ge_sub line 572
  67. theorem OAI.PerfectCompleteness.HierarchicalUsefulFamily.mean_useful_probability_ge_half line 580
  68. theorem OAI.PerfectCompleteness.HierarchicalUsefulFamily.useful_probability_ge_half line 590