OAI/MeasureTheory/FalconerCompletion/Recursion/DescriptorSmooth.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Recursive policies and quantitative depth estimates.

  1. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualDescriptorSmooth line 21
  2. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualEndpointSmooth_of_mem line 27
  3. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualEndpointSmooth_of_absent line 36
  4. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualEndpointAngular_partition line 47
  5. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualEndpointAngular_measurable line 74
  6. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualEndpointSmooth_even line 98
  7. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualEndpointAngular_even line 112