OAI/Computability/PerfectCompleteness/Construction/OriginalChildScalarAssemblyLemmas.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.OriginalChildScalarAssembly.stepSquareMap_self line 22
  2. theorem OAI.PerfectCompleteness.OriginalChildScalarAssembly.stepSquareMap_other line 32
  3. theorem OAI.PerfectCompleteness.OriginalChildScalarAssembly.recursiveSum_eq_sum line 42
  4. theorem OAI.PerfectCompleteness.OriginalChildScalarAssembly.childSquareLift_squareSum line 54
  5. theorem OAI.PerfectCompleteness.OriginalChildScalarAssembly.recursiveSum_stepSquareMap line 63
  6. theorem OAI.PerfectCompleteness.OriginalChildScalarAssembly.recursiveSum_callContributions line 111
  7. theorem OAI.PerfectCompleteness.OriginalChildScalarAssembly.recursiveSum_callContributions_tuple line 120
  8. def OAI.PerfectCompleteness.TreeShapeBounds.leafCount line 140
  9. def OAI.PerfectCompleteness.TreeShapeBounds.domainCountBound line 144
  10. def OAI.PerfectCompleteness.TreeShapeBounds.functionCountBound line 147
  11. def OAI.PerfectCompleteness.TreeShapeBounds.arrayCountBound line 150
  12. theorem OAI.PerfectCompleteness.TreeShapeBounds.slots_card_eq_leafCount line 156
  13. theorem OAI.PerfectCompleteness.TreeShapeBounds.domainBound_eq line 167
  14. theorem OAI.PerfectCompleteness.TreeShapeBounds.functionBound_eq line 171
  15. theorem OAI.PerfectCompleteness.TreeShapeBounds.domainBound_zero line 175
  16. theorem OAI.PerfectCompleteness.TreeShapeBounds.domainBound_succ line 180
  17. theorem OAI.PerfectCompleteness.TreeShapeBounds.functionBound_zero line 187
  18. theorem OAI.PerfectCompleteness.TreeShapeBounds.functionBound_succ line 191
  19. theorem OAI.PerfectCompleteness.TreeShapeBounds.arraysBound_zero line 195
  20. theorem OAI.PerfectCompleteness.TreeShapeBounds.arraysBound_succ line 199
  21. theorem OAI.PerfectCompleteness.TreeShapeBounds.arraysBound_eq line 214
  22. theorem OAI.PerfectCompleteness.TreeShapeBounds.leafCount_congr line 222
  23. theorem OAI.PerfectCompleteness.TreeShapeBounds.domainCountBound_congr line 234
  24. theorem OAI.PerfectCompleteness.TreeShapeBounds.functionCountBound_congr line 239
  25. theorem OAI.PerfectCompleteness.TreeShapeBounds.arrayCountBound_congr line 244
  26. theorem OAI.PerfectCompleteness.TreeShapeBounds.domainBound_congr line 260
  27. theorem OAI.PerfectCompleteness.TreeShapeBounds.functionBound_congr line 266
  28. theorem OAI.PerfectCompleteness.TreeShapeBounds.arraysBound_congr line 272
  29. theorem OAI.PerfectCompleteness.TreeShapeBounds.update_agrees_below line 279
  30. theorem OAI.PerfectCompleteness.TreeShapeBounds.domainBound_update line 284
  31. theorem OAI.PerfectCompleteness.TreeShapeBounds.functionBound_update line 288
  32. theorem OAI.PerfectCompleteness.TreeShapeBounds.arraysBound_update line 292
  33. theorem OAI.PerfectCompleteness.ChildBlockCardinality.shape_bound_pos line 302
  34. theorem OAI.PerfectCompleteness.ChildBlockCardinality.bound_congr line 306
  35. theorem OAI.PerfectCompleteness.ChildBlockCardinality.bound_update line 314
  36. def OAI.PerfectCompleteness.ChildBlockCardinality.zeroRaw line 331
  37. def OAI.PerfectCompleteness.ChildBlockCardinality.allZero line 335
  38. theorem OAI.PerfectCompleteness.ChildBlockCardinality.allZero_iff line 339
  39. theorem OAI.PerfectCompleteness.ChildBlockCardinality.probability_allZero line 354
  40. def OAI.PerfectCompleteness.ChildBlockCardinality.cleanLowerBound line 372
  41. theorem OAI.PerfectCompleteness.ChildBlockCardinality.cleanLowerBound_pos line 375
  42. theorem OAI.PerfectCompleteness.ChildBlockCardinality.cleanLowerBound_le_one line 379
  43. theorem OAI.PerfectCompleteness.ChildBlockCardinality.cleanLowerBound_le_probability line 386
  44. theorem OAI.PerfectCompleteness.ChildBlockCardinality.cleanLowerBound_update line 393
  45. def OAI.PerfectCompleteness.FixedBranching.extend line 410
  46. def OAI.PerfectCompleteness.FixedBranching.cleanRate line 413
  47. theorem OAI.PerfectCompleteness.FixedBranching.cleanRate_pos line 415
  48. theorem OAI.PerfectCompleteness.FixedBranching.cleanRate_le_one line 421
  49. theorem OAI.PerfectCompleteness.FixedBranching.exists_branching line 429
  50. theorem OAI.PerfectCompleteness.FixedBranching.rational_probability line 458
  51. theorem OAI.PerfectCompleteness.FixedSourceBranching.source_rate line 479
  52. theorem OAI.PerfectCompleteness.FixedSourceBranching.exists_source_branching line 491