OAI/MeasureTheory/FalconerCompletion/Recursion/DivisionBlocksControl.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Recursive policies and quantitative depth estimates.

  1. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.division_blocks_control line 17
  2. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.division_block_width line 26
  3. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.exists_regularization_block_control line 35
  4. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.blockDepth_brackets line 66
  5. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.profile_bracket_mass_bound line 80
  6. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.sourceProfile_short_increment line 102
  7. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.sourceClass_all_depth_comparison line 117