OAI/MeasureTheory/Falconer/Recursion/DimensionalBranchBounds.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Branch weights for the ambient-dimensional profile

The excess profile is d-Lipschitz. These estimates retain that factor in both the terminal potential payment and the accumulated error exponent.

  1. def OAI.Falconer.DimensionalProfileLipschitz line 15
  2. theorem OAI.Falconer.profileExcess_dimensional_lipschitz line 18
  3. theorem OAI.Falconer.dimensional_potential_le_final_start line 25
  4. theorem OAI.Falconer._root_.OAI.PlanarFalconer.PolicyBranch.dimensional_costs_le_final_start line 42
  5. theorem OAI.Falconer.DimensionalProfileLipschitz.increment_le line 71
  6. theorem OAI.Falconer.DimensionalProfileLipschitz.abs_le line 82
  7. theorem OAI.Falconer.DimensionalProfileLipschitz.minimum_cost_le line 87
  8. theorem OAI.Falconer._root_.OAI.PlanarFalconer.BranchStep.dimensional_cost_le line 94
  9. theorem OAI.Falconer._root_.OAI.PlanarFalconer.BranchStep.dimensional_exponent_le line 109
  10. theorem OAI.Falconer._root_.OAI.PlanarFalconer.PolicyBranch.dimensional_ancestor_exponent_bound line 122
  11. theorem OAI.Falconer.dimensional_source_branch_exponent line 136
  12. theorem OAI.Falconer.uniform_dimensional_source_branch_exponent line 176
  13. theorem OAI.Falconer.dimensional_source_error_exponent line 204
  14. theorem OAI.Falconer.dimensional_uniform_source_error_branch line 214
  15. theorem OAI.Falconer.dimensional_source_profile_exponent_lower line 235
  16. theorem OAI.Falconer.dimensional_uniform_source_weighted_terminal line 244
  17. theorem OAI.Falconer.dimensional_uniform_source_weighted_error line 261