OAI/MeasureTheory/Falconer/Fourier/GoodSupportedKernelMajorant.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.PlanarFalconer.distanceDifferenceKernelline 10 - theorem
OAI.PlanarFalconer.distanceDifferenceKernel_measurableline 13 - def
OAI.PlanarFalconer.fourPairGoodline 17 - theorem
OAI.PlanarFalconer.measurable_fourPairGoodline 20 - theorem
OAI.PlanarFalconer.enorm_setIntegral_le_good_kernelline 24 - theorem
OAI.PlanarFalconer.PositiveDistanceData.original_complex_kernel_maxline 45