OAI/MeasureTheory/Falconer/Estimates/MaskedNested.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Support of all old masks controls the positive low-frequency child

The old weighted law is dominated by the unweighted child restriction. This comparison takes place before applying the scalar real-line bin bound.

  1. theorem OAI.Falconer.maskedCellDistance_le_tested line 17