OAI/MeasureTheory/Falconer/Recursion/ProfileNormalBudget.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A polynomial depth loss suffices for a normal interval once its point and pencil constants fit the common weak budget.

  1. theorem OAI.Falconer.planarCriticalConstant_le_depth line 10
  2. theorem OAI.Falconer.planar_normal_cost_bound line 19
  3. theorem OAI.Falconer.profileEndpointBound_normal_budget line 40