OAI/MeasureTheory/Falconer/Estimates/RegularizationSelection.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Selecting the regular classes with their original masses

Classes are disjoint unions of original leaves. Discarding small leaves costs 2^(-2N), and discarding small classes costs their number times the class threshold. No lower density of the original law is required.

  1. def OAI.Falconer.Regularization.regularizationIndex line 18
  2. def OAI.Falconer.Regularization.regularizationSet line 23
  3. theorem OAI.Falconer.Regularization.regularizationSet_measurable line 27
  4. theorem OAI.Falconer.Regularization.regularizationIndex_card line 31
  5. theorem OAI.Falconer.Regularization.regularizationSet_disjoint line 36
  6. theorem OAI.Falconer.Regularization.regularizationSet_mass line 44
  7. theorem OAI.Falconer.Regularization.regularization_small_leaves_mass line 49
  8. theorem OAI.Falconer.Regularization.regularization_discarded_mass line 56