OAI/MeasureTheory/Falconer/Fourier/NonstationaryPhase.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform nonstationary phase in one angular coordinate

A smooth reciprocal of the phase derivative is constructed from a scalar bump. A lower bound on the phase derivative and normalized bounds on its higher derivatives give the required power of D / (Λ * τ).

  1. theorem OAI.Falconer.phase_nonstationary_from_derivative_bounds line 19