OAI/MeasureTheory/Falconer/Recursion/FrostmanProfiles.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Frostman lower envelopes for the constructed all-dimensional profiles

The enclosing-ball constant is 2*sqrt d, and the numerical choice of block length is independent of dimension.

  1. theorem OAI.Falconer.Regularization.dyadic_rpow_scale line 19
  2. theorem OAI.Falconer.Regularization.dyadic_cell_frostman_bound line 26
  3. theorem OAI.Falconer.Regularization.dyadic_cell_frostman_profile_bound line 40
  4. theorem OAI.Falconer.Regularization.fixed_constant_absorbed line 56
  5. theorem OAI.Falconer.Regularization.retained_label_real_mass_lower line 62
  6. theorem OAI.Falconer.Regularization.sourceProfile_frostman_envelope line 73