OAI/Analysis/CircleDomains/Modulus/RealBandPhysicalPayment.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The singleton-contact argument gives a physical payment inequality on every retained parameter interval.

  1. theorem OAI.CircleDomainRigidity.real_band_interval_physical_payment line 19