OAI/MeasureTheory/Falconer/Geometry/ScalarWeakRadiusProjection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Scalar projection gain when the coefficient radius is allowed the same small power loss as the ball and projection estimates. Normalization uses an actual maximal coefficient and costs only a fixed polynomial.

  1. theorem OAI.Falconer.Regularization.scalar_weak_radius_projection line 13