OAI/MeasureTheory/Falconer/Incidence/BlockCellNormalPower.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The normal cell contributes its baseline exponent, minus three times its own chord error and the common weak loss.

  1. theorem OAI.Falconer.block_cell_normal_power line 10