OAI/Analysis/CircleDomains/Modulus/LocalizedCirclePayment.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Parallel-line payment charges only a measurable region containing the actual domain segments.

  1. theorem OAI.CircleDomainRigidity.parallel_line_payment_in_region line 14
  2. theorem OAI.CircleDomainRigidity.parallel_line_payment_in_region_square_norm line 81