OAI/MeasureTheory/Falconer/Estimates/ScalarPathLevel.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Separated levels retain only the information used by the projection argument. They allow bunching without requiring a new closest-pair witness.

  1. structure OAI.Falconer.Regularization.ScalarPathLevel line 10
  2. theorem OAI.Falconer.Regularization.ScalarPathLevel.prune_lower line 16
  3. theorem OAI.Falconer.Regularization.ScalarPathLevel.prune_upper line 31
  4. theorem OAI.Falconer.Regularization.ScalarPathLevel.of_branching line 45
  5. theorem OAI.Falconer.Regularization.ScalarPathLevel.trim line 50
  6. def OAI.Falconer.Regularization.scalarSeparatedPathTreeOfLeafFibers line 65
  7. def OAI.Falconer.Regularization.scalarSeparatedPathTreeOfLevels line 125