OAI/Computability/PerfectCompleteness/Construction/SourceChildKernelLemmas.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.SourceChildKernel.Block line 21
  2. instance OAI.PerfectCompleteness.SourceChildKernel.blockFintype line 25
  3. def OAI.PerfectCompleteness.SourceChildKernel.zeroBlock line 29
  4. instance OAI.PerfectCompleteness.SourceChildKernel.blockNonempty line 33
  5. abbrev OAI.PerfectCompleteness.SourceChildKernel.Rest line 40
  6. abbrev OAI.PerfectCompleteness.SourceChildKernel.Source line 43
  7. def OAI.PerfectCompleteness.SourceChildKernel.tree line 45
  8. def OAI.PerfectCompleteness.SourceChildKernel.nativeSlots line 49
  9. def OAI.PerfectCompleteness.SourceChildKernel.ids line 53
  10. def OAI.PerfectCompleteness.SourceChildKernel.mixedSlots line 57
  11. theorem OAI.PerfectCompleteness.SourceChildKernel.mixedSlots_eq_rightTuple line 62
  12. abbrev OAI.PerfectCompleteness.SourceChildKernel.Native line 68
  13. abbrev OAI.PerfectCompleteness.SourceChildKernel.Projected line 71
  14. abbrev OAI.PerfectCompleteness.SourceChildKernel.Factors line 74
  15. abbrev OAI.PerfectCompleteness.SourceChildKernel.D line 77
  16. abbrev OAI.PerfectCompleteness.SourceChildKernel.Raw line 80
  17. instance OAI.PerfectCompleteness.SourceChildKernel.rawFintype line 84
  18. def OAI.PerfectCompleteness.SourceChildKernel.nonprojected line 89
  19. def OAI.PerfectCompleteness.SourceChildKernel.kernel line 93
  20. def OAI.PerfectCompleteness.SourceChildKernel.projectedEquiv line 99
  21. def OAI.PerfectCompleteness.SourceChildKernel.zero line 106
  22. theorem OAI.PerfectCompleteness.SourceChildKernel.projectedEquiv_zero line 112
  23. theorem OAI.PerfectCompleteness.SourceChildKernel.projectedEquiv_law line 116
  24. def OAI.PerfectCompleteness.SourceChildKernel.rawProjected line 129
  25. def OAI.PerfectCompleteness.SourceChildKernel.rawTag line 133
  26. theorem OAI.PerfectCompleteness.SourceChildKernel.kernel_tag line 138
  27. def OAI.PerfectCompleteness.SourceChildKernel.decodeNative line 147
  28. def OAI.PerfectCompleteness.SourceChildKernel.decodeProjected line 153
  29. theorem OAI.PerfectCompleteness.SourceChildKernel.decodeNative_tagged line 162
  30. theorem OAI.PerfectCompleteness.SourceChildKernel.decodeProjected_tagged line 167
  31. def OAI.PerfectCompleteness.SourceChildKernel.decodeRight line 174
  32. theorem OAI.PerfectCompleteness.SourceChildKernel.decodeNative_law line 180
  33. theorem OAI.PerfectCompleteness.SourceChildKernel.decodeProjected_law line 192
  34. theorem OAI.PerfectCompleteness.SourceChildKernel.decodeRight_clean line 200
  35. def OAI.PerfectCompleteness.SourceChildKernel.projection line 222
  36. abbrev OAI.PerfectCompleteness.SourceChildKernel.Sources line 231
  37. def OAI.PerfectCompleteness.SourceChildKernel.parentLeftSlots line 233
  38. def OAI.PerfectCompleteness.SourceChildKernel.parentRightSlots line 237
  39. def OAI.PerfectCompleteness.SourceChildKernel.parentProjection line 243
  40. def OAI.PerfectCompleteness.SourceChildKernel.rightChildren line 250
  41. def OAI.PerfectCompleteness.SourceChildKernel.leftChildren line 255
  42. theorem OAI.PerfectCompleteness.SourceChildKernel.leftChildren_apply line 262
  43. theorem OAI.PerfectCompleteness.SourceChildKernel.assemble_leftChildren line 270
  44. abbrev OAI.PerfectCompleteness.SourceChildKernel.Sample line 282
  45. instance OAI.PerfectCompleteness.SourceChildKernel.sampleFintype line 285
  46. def OAI.PerfectCompleteness.SourceChildKernel.childrenLaw line 289
  47. theorem OAI.PerfectCompleteness.SourceChildKernel.childrenLaw_tag line 296
  48. theorem OAI.PerfectCompleteness.SourceChildKernel.childrenLaw_clean_zero line 306
  49. def OAI.PerfectCompleteness.SourceChildKernel.originalLaw line 321
  50. abbrev OAI.PerfectCompleteness.SourceChildKernelJoint.RawTuple line 346
  51. def OAI.PerfectCompleteness.SourceChildKernelJoint.groupEquiv line 349
  52. theorem OAI.PerfectCompleteness.SourceChildKernelJoint.groupEquiv_sources line 358
  53. theorem OAI.PerfectCompleteness.SourceChildKernelJoint.groupEquiv_raw line 363
  54. theorem OAI.PerfectCompleteness.SourceChildKernelJoint.childrenLaw_group line 368
  55. theorem OAI.PerfectCompleteness.SourceChildKernelJoint.originalLaw_group line 395
  56. abbrev OAI.PerfectCompleteness.SourceChildKernelRate.Factors line 428
  57. abbrev OAI.PerfectCompleteness.SourceChildKernelRate.Record line 429
  58. abbrev OAI.PerfectCompleteness.SourceChildKernelRate.Sample line 432
  59. abbrev OAI.PerfectCompleteness.SourceChildKernelRate.CleanChildren line 433
  60. theorem OAI.PerfectCompleteness.SourceChildKernelRate.bound_from_repetition line 436
  61. theorem OAI.PerfectCompleteness.SourceChildKernelRate.amplified_bound line 495