OAI/MeasureTheory/Falconer/Recursion/ProfileUniformIterationBudget.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Choose the block width after fixing the maximal number of intervals. All recursive losses then fit a prescribed weak exponent uniformly in depth.

  1. theorem OAI.Falconer.exists_uniform_profile_iteration_budget line 10