OAI/MeasureTheory/Falconer/Recursion/BranchErrorBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PlanarFalconer.DiscreteProfileLipschitz.increment_le_one line 8
  2. theorem OAI.PlanarFalconer.DiscreteProfileLipschitz.abs_le_one line 18
  3. theorem OAI.PlanarFalconer.DiscreteProfileLipschitz.minimum_cost_le_one line 23
  4. theorem OAI.PlanarFalconer.BranchStep.cost_le_one line 31
  5. theorem OAI.PlanarFalconer.BranchStep.exponent_le_four line 46
  6. theorem OAI.PlanarFalconer.PolicyBranch.ancestor_exponent_bound line 59
  7. theorem OAI.PlanarFalconer.source_error_exponent line 73
  8. theorem OAI.PlanarFalconer.uniform_source_error_branch line 84
  9. theorem OAI.PlanarFalconer.source_profile_exponent_lower line 105
  10. theorem OAI.PlanarFalconer.uniform_recursion_count_subpower line 114