OAI/MeasureTheory/Falconer/Geometry/CellNormalization.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual cell normalization used by the middle radial interval

  1. theorem OAI.Falconer.Regularization.cell_normalization_map line 14
  2. theorem OAI.Falconer.Regularization.cell_normalization_support line 23
  3. theorem OAI.Falconer.Regularization.cell_normalization_quarter_point line 31
  4. theorem OAI.Falconer.Regularization.conditional_frostman_coefficient_ge_one line 41
  5. theorem OAI.Falconer.Regularization.sourceClass_normalized_conditional_frostman line 53
  6. theorem OAI.Falconer.Regularization.sourceClass_scaled_dyadic_ball line 79