OAI/MeasureTheory/Falconer/Recursion/ContactLossBudget.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Uniform comparison of contact-profile losses with the middle angular scale

  1. theorem OAI.Falconer.dyadic_rpow_div_depth line 9
  2. theorem OAI.Falconer.inverse_dyadic_neg_power line 15
  3. theorem OAI.Falconer.contact_loss_le line 19
  4. theorem OAI.Falconer.contact_loss_relative_budget line 27
  5. theorem OAI.Falconer.eventually_contact_frostman_coefficient line 42
  6. theorem OAI.Falconer.eventually_contact_outer_coefficient line 61
  7. theorem OAI.Falconer.middle_scale_power_decay line 86