OAI/Analysis/CircleDomains/Modulus/PhysicalTagPayment.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The local payment measure is formed from actual physical time length and the flagged visit toll. Its total mass is bounded by the selected path law’s cost.

  1. def OAI.CircleDomainRigidity.physicalTagPayment line 20
  2. theorem OAI.CircleDomainRigidity.physicalTagPayment_univ line 25
  3. theorem OAI.CircleDomainRigidity.physicalTagPayment_finite line 32
  4. theorem OAI.CircleDomainRigidity.physicalTagPayment_null_free line 41
  5. theorem OAI.CircleDomainRigidity.physicalTagPayment_interval line 49