OAI/MeasureTheory/FalconerCompletion/Recursion/AssemblyDescriptorList.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Recursive policies and quantitative depth estimates.

  1. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assemblyDescriptorList line 25
  2. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assemblySymbol line 28
  3. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assemblyRootEnergy line 37
  4. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assemblyDescriptorList_valid line 61
  5. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assemblyDescriptorList_length line 67
  6. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assemblySymbol_measurable line 78
  7. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assemblySymbol_smooth line 86
  8. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assemblySymbol_eq line 94
  9. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.uniform_assemblySymbol_jets line 105
  10. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.uniform_assemblySymbol_imposes line 131