OAI/MeasureTheory/Falconer/Estimates/RegularizationCount.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Polynomial class count and discarded mass in every dimension

  1. theorem OAI.Falconer.Regularization.regularization_count_polynomial line 13
  2. theorem OAI.Falconer.Regularization.block_polynomial_exponent line 26
  3. theorem OAI.Falconer.Regularization.regularization_discarded_global line 36