OAI/Analysis/CircleDomains/Modulus/TerminalLimitPayment.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Limiting payment by source energy and band widths

For a fixed barrier the transfer errors vanish while the original source energy and band norm remain. This is the limit required before choosing successively smaller barriers in the unmarked-end argument.

  1. theorem OAI.CircleDomainRigidity.limiting_terminal_line_payment line 23