OAI/Analysis/CircleDomains/Selection/PreterminalTolls.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

True boundary tolls with exactly the final parameter omitted, retaining all multiplicities at earlier times. Positive added weights control code mass.

  1. def OAI.CircleDomainRigidity.preterminalToll line 18
  2. theorem OAI.CircleDomainRigidity.preterminalToll_eq_visits line 21
  3. theorem OAI.CircleDomainRigidity.preterminalToll_eq_support line 32
  4. theorem OAI.CircleDomainRigidity.preterminalToll_add_terminal line 42
  5. theorem OAI.CircleDomainRigidity.preterminalToll_mono line 51
  6. theorem OAI.CircleDomainRigidity.weighted_preterminal_sum_le line 60
  7. theorem OAI.CircleDomainRigidity.finite_preterminal_sum_of_positive_tolls line 70
  8. theorem OAI.CircleDomainRigidity.measurable_preterminalToll line 84