OAI/Analysis/CircleDomains/Modulus/RotatedLocalizedPayment.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Localized line payment in any fixed direction, with unchanged source energy and hole costs.

  1. def OAI.CircleDomainRigidity.rotatedLine line 16

    Source documentation

    A line in the direction chosen by a unit complex multiplier.

    def rotatedLine (a : Circle) (y x : ℝ) : ℂ := rotation a (horizontalLine y x)

    Mentions: OAI.CircleDomainRigidity.horizontalLine

  2. theorem OAI.CircleDomainRigidity.rotated_line_payment_in_region line 18