OAI/MeasureTheory/FalconerCompletion/Recursion/Extend.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Recursive policies and quantitative depth estimates.

  1. def OAI.GraphLiteralSupport.CurrentFalconer.DimensionalPolicy.PolicyBranch.extend line 30
  2. theorem OAI.GraphLiteralSupport.CurrentFalconer.DimensionalPolicy.PolicyBranch.extend_state_le line 47
  3. theorem OAI.GraphLiteralSupport.CurrentFalconer.DimensionalPolicy.PolicyBranch.extend_label_lt line 52
  4. theorem OAI.GraphLiteralSupport.CurrentFalconer.DimensionalPolicy.PolicyBranch.extend_last_state line 57
  5. theorem OAI.GraphLiteralSupport.CurrentFalconer.DimensionalPolicy.PolicyBranch.extend_last_label line 62
  6. def OAI.GraphLiteralSupport.CurrentFalconer.DimensionalPolicy.PolicyBranch.exponentSum line 72
  7. def OAI.GraphLiteralSupport.CurrentFalconer.DimensionalPolicy.PolicyBranch.weight line 75
  8. theorem OAI.GraphLiteralSupport.CurrentFalconer.DimensionalPolicy.PolicyBranch.weight_pos line 78
  9. theorem OAI.GraphLiteralSupport.CurrentFalconer.DimensionalPolicy.PolicyBranch.exponentSum_extend line 82
  10. theorem OAI.GraphLiteralSupport.CurrentFalconer.DimensionalPolicy.PolicyBranch.weight_extend line 97
  11. theorem OAI.GraphLiteralSupport.CurrentFalconer.DimensionalPolicy.PolicyBranch.weight_eq_product line 105
  12. theorem OAI.GraphLiteralSupport.CurrentFalconer.DimensionalPolicy.PolicyBranch.weight_zero line 110
  13. theorem OAI.GraphLiteralSupport.CurrentFalconer.DimensionalPolicy.ProfileLipschitzND.increment_le line 115
  14. theorem OAI.GraphLiteralSupport.CurrentFalconer.DimensionalPolicy.ProfileLipschitzND.minimum_cost_le line 126
  15. theorem OAI.GraphLiteralSupport.CurrentFalconer.DimensionalPolicy.BranchStep.cost_le line 133
  16. theorem OAI.GraphLiteralSupport.CurrentFalconer.DimensionalPolicy.BranchStep.exponent_leND line 148
  17. theorem OAI.GraphLiteralSupport.CurrentFalconer.DimensionalPolicy.PolicyBranch.ancestor_exponent_boundND line 161
  18. theorem OAI.GraphLiteralSupport.CurrentFalconer.DimensionalPolicy.uniform_source_weighted_terminalND line 172
  19. theorem OAI.GraphLiteralSupport.CurrentFalconer.DimensionalPolicy.uniform_source_weighted_errorND line 189