OAI/MeasureTheory/Falconer/Estimates/ScalarBunchBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A single explicit parameter choice controls the exceptional-pair budget in both the short and long porous bunches.

  1. theorem OAI.Falconer.scalar_bunch_log_weight line 9
  2. theorem OAI.Falconer.scalar_bunch_uniform_budget line 28