OAI/MeasureTheory/Falconer/Estimates/ScalarUniformTrim.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A complete bunch-trimming step on the original regularized paths: exact cardinal loss, retained branch count, separation, and common mass.

  1. theorem OAI.Falconer.Regularization.scalar_trimmed_uniform_block line 9