OAI/Analysis/CircleDomains/Modulus/RotatedRealPayment.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Arbitrary-direction localized payment for the actual assigned finite models and their limit.

  1. theorem OAI.CircleDomainRigidity.TerminalComponentAssignment.rotated_line_payment_in_region line 16
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealTransferStage.rotated_localized_line_payment line 84
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.AssignedRealModelLimit.rotated_localized_line_payment line 131
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.AssignedRealModelLimit.rotated_line_payment_away_from_compact line 196