OAI/Analysis/CircleDomains/Modulus/ThresholdImagePayment.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Integrating the paid-threshold cover gives the local image payment. The bands here are the actual compact real fibers.

  1. theorem OAI.CircleDomainRigidity.interval_payment_of_ae_cover line 15
  2. theorem OAI.CircleDomainRigidity.real_band_fiber_volume line 32
  3. theorem OAI.CircleDomainRigidity.interval_band_payment_of_ae_cover line 41