OAI/MeasureTheory/Falconer/Estimates/RegularClassSmallTrouble.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform small troublesome-pair mass for the original regularized class

  1. theorem OAI.Falconer.Regularization.regular_class_small_troublesome line 13