FrameRegularity.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Boundedness on the compact frame space supplies the weighted Lipschitz condition required by the proved discrete-to-continuous radial comparison.