OAI/MeasureTheory/Falconer/Measures/FrostmanDischarge.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The application-level Frostman input proved in every ambient dimension

Finite dyadic capacities give probability approximants carried by the compact set. The finite cube count gives uniform ball bounds; a compact weak limit preserves them. Only exponents strictly above half the dimension are selected in the published-input discharge.

  1. theorem OAI.Falconer.frostman_probability line 17
  2. theorem OAI.Falconer.published_frostman_above_half line 32