OAI/MeasureTheory/Falconer/Incidence/IncidencePowerBudget.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Power bounds relating the original radius to the chosen block scale.

  1. theorem OAI.Falconer.incidence_inverse_scale_power line 9
  2. theorem OAI.Falconer.incidence_bucket_linear_bound line 25
  3. theorem OAI.Falconer.exists_incidence_absorption_parameters line 39