OAI/MeasureTheory/Falconer/Geometry/FiniteWeightedProjectionSample.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A finite weighted projection contains an actual separated Frostman set. Sampling uses only the original finite labels, so every selected projected point has an original witness.

  1. theorem OAI.Falconer.finite_weighted_projection_sample line 15