OAI/Analysis/CircleDomains/Topology/ClippedPaths.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Constant extension of a closed path portion. Its arclength is exactly the variation of that portion; this is used to assemble local physical lifts.

  1. def OAI.CircleDomainRigidity.timeClip line 15
  2. theorem OAI.CircleDomainRigidity.monotone_timeClip line 19
  3. theorem OAI.CircleDomainRigidity.range_timeClip line 22
  4. theorem OAI.CircleDomainRigidity.variation_timeClip line 32
  5. def OAI.CircleDomainRigidity.clippedPath line 38
  6. theorem OAI.CircleDomainRigidity.continuous_clippedPath line 44
  7. theorem OAI.CircleDomainRigidity.pathLengthMeasure_clipped_univ line 48
  8. theorem OAI.CircleDomainRigidity.pathLengthMeasure_clipped_Ioc line 54