OAI/MeasureTheory/Falconer/Estimates/ScalarPorousLevel.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The scalar porous one-level gain for actual finite sets. This combines separated children, the original coefficient ball bound, and logarithmic averaging with its explicit exceptional-set loss.

  1. theorem OAI.Falconer.scalar_sum_cells_pos line 12
  2. theorem OAI.Falconer.scalar_porous_level_log_gain line 23