OAI/MeasureTheory/Falconer/Estimates/EvenPreparation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Even-dimensional starting pairs in the original compact set

This is the even-dimensional branch of prep:starting-pairs, not the all-dimensional distance theorem. The cap and exceptional-set conclusions refer to the original marginal laws in Space (2*h).

  1. theorem OAI.Falconer.even_starting_pairs_of_published line 15