OAI/MeasureTheory/Falconer/Estimates/ScalarCompressedBunching.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Realizing a bunching ledger after grouping the original regularized dyadic levels. The final gap is stated in the original geometric scale.

  1. theorem OAI.Falconer.Regularization.ScalarPathLevel.mono_gap line 9
  2. theorem OAI.Falconer.Regularization.scalar_compressed_bunch_pruning_of_leaves line 13
  3. theorem OAI.Falconer.Regularization.scalar_compressed_bunch_pruning line 60