OAI/MeasureTheory/FalconerCompletion/Recursion/OccupiedDescendantPath.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Recursive policies and quantitative depth estimates.

  1. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.occupiedDescendant_path line 27
  2. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.RegularizedProfileData.occupiedDescendant_lower line 41
  3. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.recursive_near_max_le line 53
  4. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.recursive_far_max_le line 87
  5. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.uniform_recursive_near_far line 125
  6. theorem OAI.GraphLiteralSupport.CurrentFalconer.DimensionalPolicy.weighted_branch_energy_induction line 245