OAI/MeasureTheory/Falconer/Estimates/PlanarWeakParameters.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The linear auxiliary-depth inequalities imply the exact multiplicative budgets needed by the original planar graph obstruction.

  1. theorem OAI.Falconer.planar_weak_parameters line 9