OAI/MeasureTheory/Falconer/Estimates/ChildRetention.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Local retention also controls the number of endpoint cells, not just the fine mass. This is needed when the next incidence argument uses centers.

  1. theorem OAI.Falconer.Regularization.prefix_children_mass_bounds line 12
  2. theorem OAI.Falconer.Regularization.blockClass_child_retention line 30