OAI/MeasureTheory/Falconer/Incidence/BlockCellPower.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Normal and good cells have a common additive exponent. The gain is charged only on cells whose actual secant slope crosses the fixed threshold.

  1. theorem OAI.Falconer.blockProfileCell_gain_exponent line 12
  2. theorem OAI.Falconer.dyadic_good_power_weaken line 26
  3. theorem OAI.Falconer.block_cell_power line 39