OAI/MeasureTheory/Falconer/Shells/PublishedClassicalDistance.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The published strict classical threshold, only for compact sets

Mattila–Sjölin, Regularity of Distance Measures and Sets, Mathematische Nachrichten 204 (1999), 157–162, DOI 10.1002/mana.19992040110. The corollary stated in the publisher's abstract says that a Suslin set in R^n of Hausdorff dimension greater than (n+1)/2 has a distance set with nonempty interior. Here only its weaker compact positive-measure specialization is used.

https://onlinelibrary.wiley.com/doi/abs/10.1002/mana.19992040110

  1. def OAI.Falconer.PublishedClassicalDistance line 20
  2. theorem OAI.Falconer.classical_distance_of_frostman line 24