OAI/MeasureTheory/FalconerCompletion/Recursion/ProfileLipschitz.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Recursive policies and quantitative depth estimates.

  1. def OAI.GraphLiteralSupport.CurrentFalconer.DimensionalPolicy.ProfileLipschitzND line 33
  2. lemma OAI.GraphLiteralSupport.CurrentFalconer.DimensionalPolicy.adjusted_profile_lipschitzND line 36
  3. lemma OAI.GraphLiteralSupport.CurrentFalconer.DimensionalPolicy.potential_le_final_startND line 59
  4. theorem OAI.GraphLiteralSupport.CurrentFalconer.DimensionalPolicy.policy_costs_le_final_startND line 76
  5. def OAI.GraphLiteralSupport.CurrentFalconer.DimensionalPolicy.branchExponentND line 107
  6. lemma OAI.GraphLiteralSupport.CurrentFalconer.DimensionalPolicy.branch_exponent_sumND line 112
  7. theorem OAI.GraphLiteralSupport.CurrentFalconer.DimensionalPolicy.source_branch_exponentND line 123
  8. theorem OAI.GraphLiteralSupport.CurrentFalconer.DimensionalPolicy.uniform_source_branch_exponentND line 167
  9. theorem OAI.GraphLiteralSupport.CurrentFalconer.DimensionalPolicy.BranchStep.strict_progress line 208
  10. theorem OAI.GraphLiteralSupport.CurrentFalconer.DimensionalPolicy.BranchStep.width_decreases line 237
  11. theorem OAI.GraphLiteralSupport.CurrentFalconer.DimensionalPolicy.valid_step_wellFounded line 248
  12. theorem OAI.GraphLiteralSupport.CurrentFalconer.DimensionalPolicy.nonterminal_has_step line 258
  13. def OAI.GraphLiteralSupport.CurrentFalconer.DimensionalPolicy.PolicyBranch.prepend line 285
  14. theorem OAI.GraphLiteralSupport.CurrentFalconer.DimensionalPolicy.exists_terminal_branch line 304
  15. theorem OAI.GraphLiteralSupport.CurrentFalconer.DimensionalPolicy.uniform_terminal_branch line 330