LinearMeanBudgetsFromBounds.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Actual mean budgets in a linear phase chart, with all geometric constants specified by operator norms and supplied field bounds.