OAI/MeasureTheory/Falconer/Estimates/SamplingScales.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Rounding and scale budgets for planar sampling

The sample sizes are ceilings of the reciprocal dimension powers. Query counts grow at most cubically in the reciprocal scale, while the chosen exponential tail decays with the tenth power of that scale.

  1. theorem OAI.Falconer.sampling_ceil_size line 18
  2. theorem OAI.Falconer.sampling_query_card_bound line 33
  3. theorem OAI.Falconer.sampling_exponential_tail line 46
  4. theorem OAI.Falconer.sampling_failure_bound line 50
  5. theorem OAI.Falconer.sampling_log_budget line 63