OAI/MeasureTheory/FalconerCompletion/Recursion/RecursiveEnvironment.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Recursive policies and quantitative depth estimates.

  1. structure OAI.GraphLiteralSupport.CurrentFalconer.TreeND.RecursiveEnvironmentND line 28
  2. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.RecursiveEnvironmentND.profile line 38
  3. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.RecursiveEnvironmentND.distanceData line 41
  4. structure OAI.GraphLiteralSupport.CurrentFalconer.TreeND.RecursiveAngularND line 46
  5. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.RecursiveAngularND.profile line 56
  6. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.RecursiveAngularND.fullList line 57
  7. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.RecursiveAngularND.retainedList line 59
  8. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.RecursiveAngularND.symbol line 61
  9. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.RecursiveAngularND.energy line 69
  10. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.RecursiveAngularND.sameSymbolChildren line 80
  11. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.RecursiveAngularND.graphFactor line 88
  12. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.RecursiveAngularND.symbol_measurable line 92
  13. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.RecursiveAngularND.symbol_smooth line 99
  14. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.uniform_recursive_symbol_jets line 108
  15. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.uniform_recursive_symbol_imposes line 132
  16. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.uniform_recursive_direct_graph line 158
  17. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.RecursiveAngularND.reachedChildren line 249
  18. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.RecursiveAngularND.successor line 257
  19. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.uniform_recursive_reached_removal line 261