OAI/MeasureTheory/Falconer/Incidence/BlockGrid.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact identification of the normalized integer grid with block depths. This lets the rounded analytic intervals select genuine scales of the tree.

  1. theorem OAI.Falconer.Regularization.blockDepth_multiple line 10
  2. theorem OAI.Falconer.Regularization.normalized_blockDepth line 16
  3. theorem OAI.Falconer.Regularization.innerProfileCell_natural_endpoints line 24
  4. theorem OAI.Falconer.Regularization.innerProfileCell_block_endpoints line 41