OAI/MeasureTheory/Falconer/Estimates/ScalarErrorBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Absorbing the scalar shell's fixed cost and squared remainder

The shell width costs at most one power of R. Selecting the stationary accuracy before scale therefore absorbs the square and the fixed constants.

  1. theorem OAI.Falconer.eventual_scalar_shell_error_budget line 13
  2. theorem OAI.Falconer.eventual_scalar_shell_absorption line 43