OAI/MeasureTheory/Falconer/Incidence/ScalarBlockPruning.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

One bottom-up scalar regularization step. Every surviving parent has the same branching and intermediate scale, with an explicit quadratic-in-block-width loss and unchanged deeper fibers.

  1. theorem OAI.Falconer.Regularization.scalar_block_pruning line 11