RestartSectionUpper.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Upper bounds from measurable random sections of the independent fresh driver law. The past state is allowed to vary without countable certificates.