OAI/Analysis/CircleDomains/Modulus/AdmissiblePathCost.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A positive perturbation of an admissible coding metric gives a genuine physical-plus-preterminal cost lower bound on every allowed path.

  1. def OAI.CircleDomainRigidity.physicalAtomicCost line 20
  2. theorem OAI.CircleDomainRigidity.nonTupleCost_le_physicalAtomicCost line 26
  3. theorem OAI.CircleDomainRigidity.finite_code_of_physicalAtomicCost line 40
  4. theorem OAI.CircleDomainRigidity.physicalAtomicCost_ge_one line 50