OAI/Analysis/CircleDomains/Modulus/RealBandIntervalPayment.lean

GitHub source file

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.

  1. theorem OAI.CircleDomainRigidity.real_band_interval_image_payment line 18