OAI/MeasureTheory/Falconer/Estimates/ScalarNonporousEntropy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Logarithmic form of the fixed-fold sumset bound, and the resulting quantitative supply of porous blocks for a set below full dimension.

  1. theorem OAI.Falconer.scalar_nonporous_log_bound line 9
  2. theorem OAI.Falconer.scalar_porous_fraction line 20
  3. theorem OAI.Falconer.Regularization.scalar_porous_count_from_entropy line 46