CoarsePathConcatenation.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Coarse metric bounds under path concatenation

The additive error is retained explicitly. This allows logarithmic-diameter switches and coarse-speed one-parameter legs to use a fixed finite mesh.

def OAI.PolycyclicRecognition.PathMetricBound line 19
theorem OAI.PolycyclicRecognition.PathMetricBound.mono line 22
theorem OAI.PolycyclicRecognition.PathMetricBound.symm line 28
theorem OAI.PolycyclicRecognition.PathMetricBound.cast line 35
theorem OAI.PolycyclicRecognition.pathMetricBound_trans_ordered line 38
theorem OAI.PolycyclicRecognition.PathMetricBound.trans line 76
Source documentation
Concatenation doubles the common speed and additive error. For a fixed number of pieces these constants stay independent of the height scale.
```
theorem PathMetricBound.trans {p : Path x y} {q : Path y z} {L κ : ℝ}
    (hκ : 0 ≤ κ) (hp : PathMetricBound p L κ) (hq : PathMetricBound q L κ) :
    PathMetricBound (p.trans q) (2 * L) (2 * κ) := by
…
```
Mentions: OAI.PolycyclicRecognition.PathMetricBound
theorem OAI.PolycyclicRecognition.path_trans_range_mem line 85

theorem OAI.PolycyclicRecognition.continuous_path_trans_sample line 94

Source documentation

Fixed-time continuity survives concatenation even when endpoints vary.

theorem continuous_path_trans_sample {Y : Type*} [TopologicalSpace Y]
    {a b c : Y → X} (p : ∀ y, Path (a y) (b y)) (q : ∀ y, Path (b y) (c y))
    (hp : ∀ t, Continuous (fun y => p y t)) (hq : ∀ t, Continuous (fun y => q y t))
    (t : unitInterval) : Continuous (fun y => ((p y).trans (q y)) t) := by
…