OAI/Analysis/CircleDomains/Modulus/VerticalCirclePayment.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The finite-circle payment estimate in the second Cartesian direction.

  1. def OAI.CircleDomainRigidity.verticalLine line 14
  2. theorem OAI.CircleDomainRigidity.axisSwap_horizontalLine line 16
  3. theorem OAI.CircleDomainRigidity.vertical_line_payment_on_finite_disk_complement line 20