OAI/MeasureTheory/Falconer/Estimates/ScalarCoefficientBudget.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Explicit polynomial losses for finitely many scalar sum-product operations. No generation or density assertion is assumed here.

  1. def OAI.Falconer.scalarCoefficientBudget line 9
  2. theorem OAI.Falconer.scalar_coefficient_step_bounds line 13
  3. theorem OAI.Falconer.scalarCoefficientBudget_one_le line 34
  4. theorem OAI.Falconer.scalarCoefficientBudget_zero_le line 40
  5. theorem OAI.Falconer.scalarCoefficientBudget_factor line 48