AffineClippedIntervals.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Affine time coordinates commute with clipping to an overlapping interval. This permits length estimates across collar junctions.

theorem OAI.CircleDomainRigidity.affine_rescale_eq_clip line 15
theorem OAI.CircleDomainRigidity.timeClip_comp_of_overlap line 45
theorem OAI.CircleDomainRigidity.affine_clip_rescaled line 52
Source documentation
The overlap assumption excludes the case of two disjoint clipping intervals.
```
theorem affine_clip_rescaled {a b : PathTime} (hab : a < b) {c d : PathTime}
    (hc : c ≤ b) (hd : a ≤ d) (t : PathTime) :
    affinePathTime a b (timeClip (rescalePathTime a b c) (rescalePathTime a b d) t) =
      timeClip c d (affinePathTime a b t) := by
…
```
Mentions: OAI.CircleDomainRigidity.PathTime, OAI.CircleDomainRigidity.affinePathTime, OAI.CircleDomainRigidity.timeClip, OAI.CircleDomainRigidity.rescalePathTime
theorem OAI.CircleDomainRigidity.rescalePathTime_monotone line 64