OAI/MeasureTheory/Falconer/Estimates/FirstExclusionShift.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Earlier-scale exclusions disappear from every later first-loss set

  1. theorem OAI.Falconer.firstExclusion_shift_subset line 12