OAI/Analysis/CircleDomains/Modulus/RealBandPathPayment.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.real_band_path_image_payment line 18
  2. theorem OAI.CircleDomainRigidity.real_band_path_abs_payment line 64