OAI/MeasureTheory/Falconer/Geometry/ProjectionPowerBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The explicit quadratic depth loss in projection sampling fits into any prescribed positive dyadic power, uniformly over a fixed exponent gap.

  1. theorem OAI.Falconer.dyadic_quadratic_loss line 9
  2. theorem OAI.Falconer.projection_sample_power_budget line 36