OAI/MeasureTheory/Falconer/Geometry/ScalarNormalizedCoefficients.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Normalize a weak coefficient Frostman bound to a fixed constant in [1/3,1], including every radius down to the original fine resolution.

  1. theorem OAI.Falconer.scalar_normalized_coefficients_candidate line 9
  2. theorem OAI.Falconer.scalar_normalized_coefficients line 46