OAI/MeasureTheory/Falconer/Estimates/ScalarCoefficientLogBudget.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Logarithmic bounds for the fixed number of scalar coefficient operations. They keep the normalization cost polynomial in both numerical parameters.

  1. theorem OAI.Falconer.scalar_coefficient_radius_bound line 9
  2. theorem OAI.Falconer.scalar_coefficient_radius_log line 24
  3. theorem OAI.Falconer.scalar_coefficient_log_budget line 31