OAI/MeasureTheory/FalconerCompletion/Recursion/CellPath.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

Recursive policies and quantitative depth estimates.

  1. abbrev OAI.GraphLiteralSupport.CurrentFalconer.TreeND.CellPath line 14
  2. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.dyadicPaths line 17
  3. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.mem_dyadicPaths line 22
  4. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.dyadicPaths_card_le line 31
  5. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.classLeaves line 43
  6. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.labeledChildren line 48
  7. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.extendLabel line 53
  8. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.upwardLabels line 57
  9. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.take_eq_of_take_eq line 62
  10. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.labeledChildren_eq line 67
  11. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.labeledChildren_nonempty line 73
  12. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.extendLabel_old line 79
  13. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.extendLabel_local line 83
  14. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.upwardLabels_old line 91
  15. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.upwardLabels_local line 98
  16. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.final_labeledChildren_eq line 108
  17. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.final_child_count_bin line 124
  18. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.final_child_count_bounds line 135
  19. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.labeledChildren_subset_extensions line 152
  20. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.labeledChildren_card_le line 167
  21. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.child_bin_le line 173
  22. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.extendLabel_card_le line 182
  23. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.upwardLabels_card_le line 198
  24. abbrev OAI.GraphLiteralSupport.CurrentFalconer.TreeND.blockDepth line 216
  25. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.blockLabel line 218
  26. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.blockDepth_antitone line 223
  27. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.blockDepth_gap line 227
  28. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.blockDepth_terminal line 232
  29. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.blockLabel_old line 239
  30. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.blockLabel_local line 253
  31. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.block_final_children line 271
  32. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.block_final_bin_eq line 288
  33. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.blockLabel_card_le line 298
  34. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.prefixFiber line 316
  35. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.prefixChildren line 320
  36. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.prefixFiber_zero line 323
  37. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.prefixFiber_leaf line 327
  38. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.prefixFiber_nonempty line 339
  39. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.prefixChildren_mem_image line 345
  40. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.prefixFiber_parent_filter line 351
  41. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.prefixFiber_card_sum line 364
  42. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.prefixFiber_count_bounds line 374
  43. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.prefixChildren_class_eq line 392
  44. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.blockBin line 402
  45. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.blockProduct line 406
  46. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.blockBin_pos line 409
  47. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.blockProduct_pos line 413
  48. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.blockBin_le line 417
  49. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.blockClass_child_bounds line 424
  50. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.blockClass_leaf_count line 448
  51. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.blockClass_root_count line 482