CoarsePathRadius.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Radius control for logarithmic-error paths

The support-path parameter bounds imply a single linear ambient ball bound for every sample, uniformly at all scales at least one.

theorem OAI.PolycyclicRecognition.PathMetricBound.dist_source_le line 17
Source documentation
A coarse path stays within its speed plus its additive error of its source.
```
theorem PathMetricBound.dist_source_le {p : Path x y} {L κ : ℝ}
    (h : PathMetricBound p L κ) (hL : 0 ≤ L) (t : unitInterval) :
    dist x (p t) ≤ L + κ := by
…
```
Mentions: OAI.PolycyclicRecognition.PathMetricBound

theorem OAI.PolycyclicRecognition.PathMetricBound.dist_source_le_linear line 26

Source documentation

The logarithmic error is uniformly at most a linear error for r ≥ 1.

theorem PathMetricBound.dist_source_le_linear {p : Path x y} {C r : ℝ}
    (h : PathMetricBound p (C * r) (C * (1 + Real.log (2 + r))))
    (hC : 0 ≤ C) (hr : 1 ≤ r) (t : unitInterval) :
    dist x (p t) ≤ (4 * C) * r := by
…

Mentions: OAI.PolycyclicRecognition.PathMetricBound