OAI/MeasureTheory/Falconer/Slicing/GaussianChartPairKernel.lean
1 declarations, 0 contain sorry, 0 declared as axioms
The normalized pair kernel in the bounded gnomonic chart
- theorem
OAI.Falconer.gaussian_chart_pair_kernelline 13