OAI/MeasureTheory/FalconerCompletion/Recursion/DescriptorValid.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Recursive policies and quantitative depth estimates.

  1. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.descriptorValid line 20
  2. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.endpointGood_at_cell line 24
  3. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.ae_occupied_anchor line 36
  4. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.uniform_original_fiber_test_bound line 54