OAI/Computability/PerfectCompleteness/Repetition/CutChildCleanLawLemmas.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.CutChildCleanLaw.Raw line 26
  2. instance OAI.PerfectCompleteness.CutChildCleanLaw.rawFintype line 29
  3. def OAI.PerfectCompleteness.CutChildCleanLaw.zeroRaw line 31
  4. instance OAI.PerfectCompleteness.CutChildCleanLaw.rawNonempty line 33
  5. def OAI.PerfectCompleteness.CutChildCleanLaw.rawEquiv line 35
  6. def OAI.PerfectCompleteness.CutChildCleanLaw.allZero line 49
  7. theorem OAI.PerfectCompleteness.CutChildCleanLaw.allZero_rawEquiv line 52
  8. def OAI.PerfectCompleteness.CutChildCleanLaw.rawLaw line 67
  9. theorem OAI.PerfectCompleteness.CutChildCleanLaw.rawLaw_reindex line 70
  10. def OAI.PerfectCompleteness.CutChildCleanLaw.shapeProbability line 80
  11. theorem OAI.PerfectCompleteness.CutChildCleanLaw.probability_allZero_eq_cleanTree line 85
  12. theorem OAI.PerfectCompleteness.CutChildCleanLaw.probability_allZero line 96
  13. theorem OAI.PerfectCompleteness.CutChildCleanLaw.probability_allZero_pos line 102
  14. theorem OAI.PerfectCompleteness.CutChildCleanLaw.probability_allZero_eq_of_card_eq line 107
  15. theorem OAI.PerfectCompleteness.CutChildCleanLaw.probability_wholeCalls line 117
  16. theorem OAI.PerfectCompleteness.CutChildCleanLaw.probability_wholeCalls_eq line 124
  17. abbrev OAI.PerfectCompleteness.UniformCleanSources.ChildRaw line 158
  18. def OAI.PerfectCompleteness.UniformCleanSources.childKernel line 160
  19. def OAI.PerfectCompleteness.UniformCleanSources.childClean line 165
  20. def OAI.PerfectCompleteness.UniformCleanSources.childrenLaw line 169
  21. abbrev OAI.PerfectCompleteness.UniformCleanSources.Record line 177
  22. def OAI.PerfectCompleteness.UniformCleanSources.cleanRecord line 179
  23. abbrev OAI.PerfectCompleteness.UniformCleanSources.CleanIndices line 183
  24. def OAI.PerfectCompleteness.UniformCleanSources.rowEvent line 186
  25. def OAI.PerfectCompleteness.UniformCleanSources.recordEvent line 193
  26. theorem OAI.PerfectCompleteness.UniformCleanSources.clean_source_law line 200
  27. abbrev OAI.PerfectCompleteness.CleanSourceRecord.Rest line 266
  28. def OAI.PerfectCompleteness.CleanSourceRecord.assemble line 268
  29. theorem OAI.PerfectCompleteness.CleanSourceRecord.assemble_designated line 273
  30. theorem OAI.PerfectCompleteness.CleanSourceRecord.assemble_other line 279
  31. abbrev OAI.PerfectCompleteness.CleanSourceRecord.Sample line 291
  32. abbrev OAI.PerfectCompleteness.CleanSourceRecord.Record line 294
  33. def OAI.PerfectCompleteness.CleanSourceRecord.clean line 296
  34. def OAI.PerfectCompleteness.CleanSourceRecord.sourceTree line 299
  35. theorem OAI.PerfectCompleteness.CleanSourceRecord.sourceTree_designated line 308
  36. def OAI.PerfectCompleteness.CleanSourceRecord.visible line 312
  37. def OAI.PerfectCompleteness.CleanSourceRecord.rawProjected line 322
  38. def OAI.PerfectCompleteness.CleanSourceRecord.projected line 326
  39. theorem OAI.PerfectCompleteness.CleanSourceRecord.clean_projected line 338
  40. theorem OAI.PerfectCompleteness.CleanSourceRecord.observation_eq line 351
  41. theorem OAI.PerfectCompleteness.CleanSourceRecord.visible_eq_reveal line 363
  42. theorem OAI.PerfectCompleteness.CleanSourceRecord.projected_eq_raw line 402
  43. theorem OAI.PerfectCompleteness.CleanSourceRecord.clean_projected_raw line 426
  44. theorem OAI.PerfectCompleteness.CleanSourceRecord.reconstructLeft_eq line 440
  45. theorem OAI.PerfectCompleteness.CleanSourceRecord.reconstructRight_eq line 455
  46. theorem OAI.PerfectCompleteness.CleanSourceRecord.reconstructRight_slots line 472
  47. abbrev OAI.PerfectCompleteness.ProjectedCleanLaw.treeFactors line 507
  48. def OAI.PerfectCompleteness.ProjectedCleanLaw.treeZeros line 510
  49. theorem OAI.PerfectCompleteness.ProjectedCleanLaw.designated_source_law line 518
  50. abbrev OAI.PerfectCompleteness.UniformCleanSoundness.Sample line 561
  51. abbrev OAI.PerfectCompleteness.UniformCleanSoundness.FullRecord line 562
  52. def OAI.PerfectCompleteness.UniformCleanSoundness.observations line 564
  53. theorem OAI.PerfectCompleteness.UniformCleanSoundness.recordEvent_eq line 573
  54. theorem OAI.PerfectCompleteness.UniformCleanSoundness.observed_clean_count line 589
  55. theorem OAI.PerfectCompleteness.UniformCleanSoundness.conditional_source_bound line 610
  56. theorem OAI.PerfectCompleteness.UniformCleanSoundness.source_soundness line 638
  57. def OAI.PerfectCompleteness.ProjectedCleanRate.zeroProbability line 702
  58. theorem OAI.PerfectCompleteness.ProjectedCleanRate.zeroProbability_positive line 707
  59. theorem OAI.PerfectCompleteness.ProjectedCleanRate.zeroProbability_le_one line 712
  60. theorem OAI.PerfectCompleteness.ProjectedCleanRate.raw_zero_probability line 721
  61. def OAI.PerfectCompleteness.ProjectedCleanRate.coefficient line 728
  62. theorem OAI.PerfectCompleteness.ProjectedCleanRate.coefficient_eq line 732
  63. theorem OAI.PerfectCompleteness.ProjectedCleanRate.coefficient_bounds line 740
  64. def OAI.PerfectCompleteness.ProjectedCleanRate.projectionDensity line 753
  65. theorem OAI.PerfectCompleteness.ProjectedCleanRate.projectionDensity_bounds line 755
  66. def OAI.PerfectCompleteness.ProjectedCleanRate.projectionFlag line 763
  67. theorem OAI.PerfectCompleteness.ProjectedCleanRate.projectionFlag_true line 767
  68. theorem OAI.PerfectCompleteness.ProjectedCleanRate.cube_product line 771
  69. abbrev OAI.PerfectCompleteness.ProjectedCleanRate.Factors line 794
  70. def OAI.PerfectCompleteness.ProjectedCleanRate.zeros line 798
  71. theorem OAI.PerfectCompleteness.ProjectedCleanRate.bound_from_repetition line 812
  72. theorem OAI.PerfectCompleteness.ProjectedCleanRate.exists_cube_errors_lt line 844