OAI/MeasureTheory/Falconer/Recursion/ProfileGainParameters.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Quantitative choices for the final profile application. These scalar bounds keep the gain, rounding error and recursive losses independent.

  1. theorem OAI.Falconer.exists_profile_gain_accuracy line 9
  2. theorem OAI.Falconer.exists_profile_gain_budget line 20
  3. theorem OAI.Falconer.profile_gain_parameters_close line 44
  4. theorem OAI.Falconer.exists_incidence_profile_grid_threshold line 71