OAI/MeasureTheory/Falconer/Estimates/PrefixRetention.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A large uniform subset retains mass in every one of its occupied parent cells. This makes the original profile estimates hereditary after thinning.

  1. theorem OAI.Falconer.Regularization.prefix_fiber_local_retention line 11