OAI/MeasureTheory/Falconer/Estimates/ScalarScaleAlignment.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Align any fine dyadic resolution with a fixed block width. The difference is at most one block and all covering losses stay fixed.

  1. theorem OAI.Falconer.scalar_block_ceiling_bounds line 9
  2. theorem OAI.Falconer.scalar_block_scale_comparison line 16
  3. theorem OAI.Falconer.scalar_fixed_losses line 30