OAI/MeasureTheory/Falconer/Recursion/ProfileInterpolation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Profiles with the correct all-dimensional slope

The logarithmic child counts are linearly interpolated. Their exact slope bound is d/N; after rescaling the depth interval to [0,1] it is d.

  1. def OAI.Falconer.Regularization.intervalRamp line 16
  2. theorem OAI.Falconer.Regularization.intervalRamp_increment line 18
  3. def OAI.Falconer.Regularization.finiteRampProfile line 25
  4. theorem OAI.Falconer.Regularization.finiteRampProfile_continuous line 28
  5. theorem OAI.Falconer.Regularization.intervalRamp_sum line 35
  6. theorem OAI.Falconer.Regularization.finiteRampProfile_zero line 41
  7. theorem OAI.Falconer.Regularization.finiteRampProfile_increment line 45
  8. def OAI.Falconer.Regularization.blockSlope line 69
  9. def OAI.Falconer.Regularization.regularizedProfile line 74
  10. theorem OAI.Falconer.Regularization.blockSlope_bounds line 78
  11. theorem OAI.Falconer.Regularization.regularizedProfile_continuous line 105
  12. theorem OAI.Falconer.Regularization.regularizedProfile_zero line 109
  13. theorem OAI.Falconer.Regularization.regularizedProfile_increment line 113
  14. theorem OAI.Falconer.Regularization.regularizedProfile_adjusted_increment line 125