OAI/MeasureTheory/Falconer/Recursion/ProfileDecomposition.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Quantitative slope decomposition of the profile, with a uniform minimum interval length and explicit uncovered-length bound.

  1. theorem OAI.Falconer.equal_width_sum line 11
  2. theorem OAI.Falconer.quantitative_profile_slope_decomposition line 21