OAI/MeasureTheory/Falconer/Fourier/BorelSymbols.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Borel spatial restrictions preserve the angular symbol bounds

This permits the finite coarse-filter product pieces to enter the same graph estimate as dyadic cells. Only angular derivatives occur there.

  1. def OAI.Falconer.spatialRestrictionSymbol line 15
  2. theorem OAI.Falconer.spatialRestrictionSymbol_measurable line 19
  3. theorem OAI.Falconer.endpointTransform_spatialRestrictionSymbol line 25
  4. theorem OAI.Falconer.ChartSymbolControl.spatialRestriction line 37