OAI/MeasureTheory/Falconer/Geometry/ScalarNormalizedLogBudget.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The normalization cost grows at most polynomially with the weak Frostman constant and the original projection bound.

  1. def OAI.Falconer.scalarNormalizedBaseConstant line 9
  2. theorem OAI.Falconer.scalar_normalized_base_bound line 11
  3. theorem OAI.Falconer.scalar_normalized_base_one_le line 33
  4. theorem OAI.Falconer.scalar_normalized_log_budget line 43