OAI/MeasureTheory/Falconer/Geometry/ProjectionSampleBudget.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Uniform polynomial costs for the robust projection step. These bounds keep every loss explicit before the dyadic exponential absorption.

  1. def OAI.Falconer.projectionGapConstant line 9
  2. theorem OAI.Falconer.projectionGapConstant_pos line 12
  3. theorem OAI.Falconer.planarPotentialConstant_gap line 19
  4. theorem OAI.Falconer.projectionEnergyBudget_upper line 38
  5. theorem OAI.Falconer.projection_sample_log_budget line 63
  6. theorem OAI.Falconer.projectedSubsetSampleConstant_upper line 75