OAI/MeasureTheory/Falconer/Estimates/DominatedBand.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A positive dominated-measure bound on a real frequency band

Scalar real-line binning and sinc estimates control the frequency band.

  1. theorem OAI.Falconer.dominated_real_frequency_band line 15