LocalBandIntervalPayment.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Absolute variation on an actual parameter interval, paid by domain image length and the atomic measure of flagged visits.

theorem OAI.CircleDomainRigidity.local_band_interval_image_payment line 18