OAI/MeasureTheory/Falconer/Estimates/DyadicPolynomialBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Every fixed polynomial loss in the dyadic depth fits the available positive exponent. This is used for the finitely many scale-product steps.

  1. theorem OAI.Falconer.dyadic_polynomial_loss line 9
  2. theorem OAI.Falconer.dyadic_scale_loss_transfer line 36