OAI/MeasureTheory/Falconer/Recursion/UniformScaleBudgets.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform depth bounds for the actual scale-product costs. Each pencil is separated individually; separation of their entire union is not assumed.

  1. theorem OAI.Falconer.separated_pencil_configuration_logs line 12
  2. theorem OAI.Falconer.uniform_scale_cost_bounds line 31
  3. theorem OAI.Falconer.rescaled_pencil_size_ratio line 71
  4. theorem OAI.Falconer.coarse_pencil_size_ratio line 77