OAI/MeasureTheory/Falconer/Fourier/DistanceSincSpectralIdentity.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.PlanarFalconer.distanceSincKernel_integrableline 8 - theorem
OAI.PlanarFalconer.charFun_sq_integrable_finiteline 17 - theorem
OAI.PlanarFalconer.distanceSincKernel_spectral_identityline 26 - theorem
OAI.PlanarFalconer.distanceSincKernel_frequency_boundline 39