OAI/MeasureTheory/Falconer/Radial/WeakRadialLocalBudget.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Profile cancellation in the weak radial tube-counting budget

  1. theorem OAI.Falconer.real_rpow_nat_power line 11
  2. theorem OAI.Falconer.weak_radial_profile_cancel line 15
  3. theorem OAI.Falconer.weak_radial_local_count_power line 34
  4. theorem OAI.Falconer.eventually_weak_radial_local_budget line 54