OAI/MeasureTheory/Falconer/Estimates/ScalarInitialRegularization.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Initial scalar tree regularization with actual separated child cells, exact dyadic branching, and a quadratic loss per block.

  1. theorem OAI.Falconer.Regularization.scalar_initial_regularization line 10