OAI/MeasureTheory/Falconer/Estimates/RegularizedCellCounts.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Actual descendant counts for a single regularized profile

  1. theorem OAI.Falconer.Regularization.RegularizedProfileData.cell_mass_upper line 12
  2. theorem OAI.Falconer.Regularization.RegularizedProfileData.descendant_count line 25
  3. theorem OAI.Falconer.Regularization.RegularizedProfileData.pair_count line 75
  4. theorem OAI.Falconer.Regularization.RegularizedProfileData.pair_count_two line 91