OAI/MeasureTheory/Falconer/Recursion/PolicyRecursionBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A common budget for all actual policy recurrences

  1. def OAI.Falconer.PolicyPositiveBound line 14
  2. def OAI.Falconer.PolicyFarBound line 38
  3. def OAI.Falconer.PolicySuffixBound line 53
  4. structure OAI.Falconer.PolicyRecursionBounds line 64
  5. theorem OAI.Falconer.exists_policy_recursion_bounds line 71