OAI/Analysis/CircleDomains/Modulus/LocalBandPathPayment.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Integrating the actual paid-threshold conclusion yields the local variation estimate in image-measure form. Only the generic singleton statement from the independent-level argument is used.

  1. theorem OAI.CircleDomainRigidity.local_band_path_image_payment line 18
  2. theorem OAI.CircleDomainRigidity.local_band_path_abs_payment line 66