OAI/MeasureTheory/Falconer/Estimates/ScalarCompressedLevels.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Consecutive original blocks collapse to a separated level. Its gap is controlled by the final original block, so prescribed porous endpoints supply the separation needed after bunching.

  1. theorem OAI.Falconer.Regularization.scalar_branch_scale_mono line 10
  2. theorem OAI.Falconer.Regularization.scalar_grouped_path_level line 20
  3. def OAI.Falconer.Regularization.scalarCompressedBranch line 38
  4. theorem OAI.Falconer.Regularization.scalar_compressed_path_level line 41
  5. theorem OAI.Falconer.Regularization.scalar_compressed_group_separated line 51