OAI/MeasureTheory/FalconerCompletion/Recursion/SourceSymbol.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Recursive policies and quantitative depth estimates.

  1. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualSourceSymbol line 23
  2. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualSourceSymbol_measurable line 32
  3. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualSourceSymbol_support line 43
  4. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualPolicyAmbientGood line 53
  5. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualPolicyAmbientGood_even line 59
  6. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualPolicyAmbientGood_measurable line 71
  7. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.uniform_actualSourceSymbol_support line 83
  8. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.uniform_actualSourceSymbol_derivatives line 108
  9. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualEndpointSmooth_reached line 161
  10. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualEndpointAngular_reached line 171
  11. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualAngularProduct_reached line 180
  12. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.reachedDescriptorList line 194
  13. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.unreachedDescriptorList line 197
  14. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualPolicyAngular_reached_factorization line 200
  15. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.reachedSymbol_constant_on_cell line 217
  16. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.uniform_reachedSymbol_bound line 227