OAI/MeasureTheory/Falconer/Estimates/PositiveDistanceOriginalSpatial.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.PlanarFalconer.PositiveDistanceData.fourCellsline 10 - instance
OAI.PlanarFalconer.PositiveDistanceData.fourCells_finiteline 14 - theorem
OAI.PlanarFalconer.PositiveDistanceData.fourCells_preservingline 19 - theorem
OAI.PlanarFalconer.PositiveDistanceData.coincidence_original_fourline 24 - theorem
OAI.PlanarFalconer.PositiveDistanceData.original_spatial_kernel_maxline 41