NormalizedPairPacking.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Separation and paths under an actual normalized pair

theorem OAI.PolycyclicRecognition.normalizedPair_image_dist_gt_one line 19
Source documentation
The lower metric inequality turns this fixed source separation into unit separation in the image.
```
theorem normalizedPair_image_dist_gt_one (p : NormalizedPair G Λ)
    (hΛ : 0 < (Λ : ℝ)) {x y : G}
    (hxy : (Λ : ℝ) * ((Λ : ℝ) + 1) < dist x y) :
    1 < dist (p.val.1 x) (p.val.1 y) := by
…
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair

theorem OAI.PolycyclicRecognition.normalizedPair_card_image line 34

Source documentation

The image of a sufficiently separated finite set has the same cardinality.

theorem normalizedPair_card_image (p : NormalizedPair G Λ)
    (hΛ : 0 < (Λ : ℝ)) (s : Finset G)
    (hsep : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → (Λ : ℝ) * ((Λ : ℝ) + 1) < dist x y) :
    (s.image p.val.1).card = s.card := by
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair

theorem OAI.PolycyclicRecognition.normalizedPair_image_separated line 47

Source documentation

Unit separation is preserved on the image finite set.

theorem normalizedPair_image_separated (p : NormalizedPair G Λ)
    (hΛ : 0 < (Λ : ℝ)) (s : Finset G)
    (hsep : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → (Λ : ℝ) * ((Λ : ℝ) + 1) < dist x y) :
    ∀ x ∈ s.image p.val.1, ∀ y ∈ s.image p.val.1, x ≠ y → 1 ≤ dist x y := by
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair

theorem OAI.PolycyclicRecognition.normalizedPair_map_path line 62
Source documentation
The image path is based at the identity by normalization, and both coarse metric constants are multiplied by the same Lipschitz constant.
```
theorem normalizedPair_map_path (p : NormalizedPair G Λ) {g : G}
    (γ : Path (1 : G) g) {L κ : ℝ} (hγ : PathMetricBound γ L κ) :
    ∃ η : Path (1 : G) (p.val.1 g),
      (∀ t, η t = p.val.1 (γ t)) ∧ PathMetricBound η (Λ * L) (Λ * κ) := by
…
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.PathMetricBound