OAI/Analysis/CircleDomains/Modulus/TerminalSourcePayment.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Line payment charged to the physical source

The target energy in the finite-hole inequality is bounded by the actual source metric energy. Boundary tolls are the physical terminal-boundary diameters, as in the real-coordinate finite transfer.

  1. theorem OAI.CircleDomainRigidity.TerminalComponentAssignment.parallel_line_payment_source_energy line 23