OAI/Analysis/CircleDomains/Modulus/OrderedHolePayment.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Line payment for an actual finite family of closed intervals

The removed intervals are ordered and disjoint. Smoothness is required only on their complement. Endpoint cluster bounds pay for the jumps; absolute continuity of the individual domain intervals is derived.

  1. theorem OAI.CircleDomainRigidity.line_payment_of_ordered_holes line 19