OAI/MeasureTheory/FalconerCompletion/Recursion/TreeCellMembershipConstantOnFinerGrid.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Recursive policies and quantitative depth estimates.

  1. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.treeCell_membership_constant_on_finer_grid line 22
  2. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualEndpointSmooth_grid_reached line 39
  3. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualAngularProduct_grid_reached line 58
  4. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.newlyReachedDescriptorList line 75
  5. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualResidualAngular_step_factorization line 78
  6. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualResidualSourceSymbol_grid_factorization line 103
  7. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualResidualTransform_grid_factorization line 126
  8. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.uniform_newlyReachedSymbol_bound line 151
  9. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualResidual_graph_reached_removalND line 178