OAI/MeasureTheory/FalconerCompletion/Recursion/RecursiveProfileWithOverhead.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Recursive policies and quantitative depth estimates.

  1. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.uniform_recursive_profile_with_overhead line 26
  2. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.profileDimLoss line 167
  3. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.profileDimLoss_nonneg line 169
  4. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.uniform_actual_recursive_profile line 174
  5. def OAI.GraphLiteralSupport.CurrentFalconer.entryDepthND line 239
  6. lemma OAI.GraphLiteralSupport.CurrentFalconer.entryDepthND_spec line 243
  7. theorem OAI.GraphLiteralSupport.CurrentFalconer.entry_profile_boundsND line 263
  8. lemma OAI.GraphLiteralSupport.CurrentFalconer.entry_nonterminalND line 334
  9. theorem OAI.GraphLiteralSupport.CurrentFalconer.entry_potential_gainND line 347