OAI/Analysis/CircleDomains/Modulus/TimeIncidenceReparametrization.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Incidence and multiplicity-sensitive tolls under an injective change of path parameter. These formulas also apply to a restricted interval.

  1. theorem OAI.CircleDomainRigidity.timeIncidence_image line 17
  2. theorem OAI.CircleDomainRigidity.timeToll_image line 26
  3. theorem OAI.CircleDomainRigidity.image_preimage_inter_eq line 31
  4. theorem OAI.CircleDomainRigidity.timeIncidence_restrict line 40
  5. theorem OAI.CircleDomainRigidity.timeToll_restrict line 45