OAI/MeasureTheory/FalconerCompletion/Recursion/RecursiveUnit.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Recursive policies and quantitative depth estimates.

  1. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.recursiveUnit line 26
  2. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.recursiveUnit_jets line 28
  3. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.RecursiveEnvironmentND.angularData line 35
  4. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.RecursiveEnvironmentND.energies line 39
  5. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.RecursiveEnvironmentND.energies_nonneg line 58
  6. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.unreachedDescriptorList_initial line 68
  7. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixAngularData line 75
  8. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixPhased_symbol line 78
  9. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixGraphChildMax_sameSymbol line 93
  10. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.RecursiveAngularND.reachedChildren_le line 117
  11. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.RecursiveAngularND.successor_energy_mem line 139
  12. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.uniform_recursive_high_closure line 153
  13. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.uniform_recursive_terminal line 213