FiniteProjectionSublevels.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Finite Kaufman sublevel bound for the actual slope projections. This is the geometric estimate used to find regular projections inside the coarse tube packet, before extracting its product rows.

theorem OAI.Falconer.finite_projection_sublevel line 13