ProfileLowerBound.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Convert the actual finite block-count bounds into a lower bound for the whole normalized branching profile, including between the block depths.

theorem OAI.Falconer.Regularization.regularizedProfile_lower_from_ratios line 11