OAI/MeasureTheory/Falconer/Estimates/ParentPrefixRetention.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A recursive restriction pays for its loss within the current parent, not for the number of unrelated parents in the original configuration.

  1. theorem OAI.Falconer.Regularization.blockClass_parent_prefix_retention line 10