OAI/MeasureTheory/Falconer/Fourier/FourierPairing.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.PlanarFalconer.integral_charFun_swapline 11 - def
OAI.PlanarFalconer.reflectedMeasureline 21 - instance
OAI.PlanarFalconer.reflectedMeasure_finiteline 23 - theorem
OAI.PlanarFalconer.charFun_reflectedline 26 - theorem
OAI.PlanarFalconer.charFun_self_convolution_reflectedline 31 - theorem
OAI.PlanarFalconer.gaussian_charFun_square_integralline 37