OAI/MeasureTheory/Falconer/Recursion/RoundedProfileError.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Preserve the analytic bounds when the chosen profile intervals are rounded inward to the finite scale grid.

  1. theorem OAI.Falconer.rounded_error_change line 10
  2. theorem OAI.Falconer.rounded_interval_subset line 24
  3. theorem OAI.Falconer.rounded_profile_linear_error line 32
  4. theorem OAI.Falconer.rounded_profile_superlinear_error line 48
  5. theorem OAI.Falconer.rounded_profile_slope_error line 59