OAI/MeasureTheory/Falconer/Estimates/ScalarDyadicPowers.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact conversion between the dyadic scale and the exponential budgets used in the scalar projection proof.

  1. theorem OAI.Falconer.scalar_dyadic_power line 10
  2. theorem OAI.Falconer.scalar_exp_dyadic_product line 18
  3. theorem OAI.Falconer.Regularization.scalar_leaf_cells_card line 27