OAI/Analysis/CircleDomains/Selection/ConcatenatedResidualPieces.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact old-parameter descriptions of the residual times in each open piece of a concatenated path, including a clipped global test interval.

  1. theorem OAI.CircleDomainRigidity.timeIncidence_congr_path line 16
  2. theorem OAI.CircleDomainRigidity.timeToll_congr_path line 26
  3. theorem OAI.CircleDomainRigidity.concatenated_piece_times line 33