BasedImagePaths.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Image paths centered at their actual common starting point

def OAI.PolycyclicRecognition.basedImage line 17
theorem OAI.PolycyclicRecognition.basedImage_dist line 20
theorem OAI.PolycyclicRecognition.basedImage_height line 25
theorem OAI.PolycyclicRecognition.basedImage_map_path line 33
Source documentation
Centering the image gives a path based at the identity, preserves all relative heights, and multiplies both coarse metric constants by the same Lipschitz constant.
```
theorem basedImage_map_path (F : G → G) {K : ℝ≥0} (hF : LipschitzWith K F)
    {a g : G} (γ : Path a g) {L κ : ℝ} (hγ : PathMetricBound γ L κ) :
    ∃ η : Path (1 : G) (basedImage F a g),
      (∀ t, η t = basedImage F a (γ t)) ∧ PathMetricBound η (K * L) (K * κ) := by
…
```
Mentions: OAI.PolycyclicRecognition.PathMetricBound, OAI.PolycyclicRecognition.basedImage

theorem OAI.PolycyclicRecognition.basedImage_separated_card line 52

Source documentation

A based image of a separated source set has the same cardinality and unit-separated points, by the actual lower quasi-isometry inequality.

theorem basedImage_separated_card [DecidableEq G] {Λ : ℝ≥0} (p : NormalizedPair G Λ)
    (hΛ : 0 < (Λ : ℝ)) (a : G) (s : Finset G)
    (hsep : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → (Λ : ℝ) * ((Λ : ℝ) + 1) < dist x y) :
    (s.image (basedImage p.val.1 a)).card = s.card ∧
      ∀ x ∈ s.image (basedImage p.val.1 a),
        ∀ y ∈ s.image (basedImage p.val.1 a), x ≠ y → 1 ≤ dist x y := by
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.basedImage