OAI/MeasureTheory/Falconer/Measures/ScalarBunchPruning.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The entire greedy ledger is realized by successive prunings of the original finite paths. All losses multiply exactly, and each retained bunch keeps its proved separation and branching count.

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