OAI/MeasureTheory/Falconer/Estimates/ScalarTreeUniformization.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Scalar dyadic block regularization for the multiscale sum-product argument. Exact prefix classes preserve local child counts; the loss per block is only its width plus one.

  1. theorem OAI.Falconer.Regularization.scalar_blockLabel_card_le line 12
  2. theorem OAI.Falconer.Regularization.exists_large_scalar_block_class line 28
  3. theorem OAI.Falconer.Regularization.scalar_block_uniformization line 51