OAI/Analysis/CircleDomains/Modulus/OpenGapPayment.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Payment from smooth functions on open gaps

Finite energy supplies the endpoint traces, even when the function has no prescribed values on the removed intervals. Bounds on the endpoint traces are used only for the jumps across those intervals.

  1. theorem OAI.CircleDomainRigidity.line_payment_from_open_gaps line 19