OAI/MeasureTheory/Falconer/Recursion/ProfileMergeStep.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The low-slope absorption step in the profile decomposition. The new interval has exactly the prescribed slope and retains the lower chord bound.

  1. theorem OAI.Falconer.exists_superlinear_merge_left line 12