OAI/MeasureTheory/Falconer/Recursion/ProfileStepBudget.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

One explicit budget for the two branches of the endpoint scale product.

  1. def OAI.Falconer.profileStepBudget line 9
  2. theorem OAI.Falconer.profile_retention_cost_le line 11
  3. theorem OAI.Falconer.profile_step_budget_bounds line 21
  4. theorem OAI.Falconer.profile_label_cost_one_le line 75