OAI/Analysis/CircleDomains/Selection/ExtendedAtomicToll.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Extend a prescribed countable atomic metric by zero on the quotient. Both its square norm and the full preterminal visit payment are preserved.

  1. def OAI.CircleDomainRigidity.extendAtomicToll line 14
  2. theorem OAI.CircleDomainRigidity.extendAtomicToll_apply line 17
  3. theorem OAI.CircleDomainRigidity.extendAtomicToll_zero line 21
  4. theorem OAI.CircleDomainRigidity.support_extendAtomicToll_subset line 25
  5. theorem OAI.CircleDomainRigidity.countingSquareNorm_extendAtomicToll line 31
  6. theorem OAI.CircleDomainRigidity.preterminalToll_extendAtomicToll line 47
  7. theorem OAI.CircleDomainRigidity.extendAtomicToll_eq_zero_on_disjoint line 64
  8. theorem OAI.CircleDomainRigidity.perturbed_endpoint_cost_ge_one line 72