TransferredAction.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Transferring translations across a coarse inverse pair

For maps f : H → X and r : X → H, the maps x ↦ f (h * r x) form the uniform quasi-action used in Proposition recognition-from-height of the manuscript. These estimates retain the errors of the coarse inverse pair and require only the stated metric inequalities.

def OAI.PolycyclicRecognition.transferredMap line 23
Source documentation
The left translation by h, transferred using f and r.
```
def transferredMap (f : H → X) (r : X → H) (h : H) (x : X) : X :=
…
```
theorem OAI.PolycyclicRecognition.transferredMap_apply line 27
theorem OAI.PolycyclicRecognition.transferredMap_normalized line 31
Source documentation
A normalized inverse sends the distinguished point to the original orbit.
```
theorem transferredMap_normalized (f : H → X) (r : X → H) (x₀ : X)
    (hr₀ : r x₀ = 1) (h : H) : transferredMap f r h x₀ = f h := by
…
```
Mentions: OAI.PolycyclicRecognition.transferredMap
theorem OAI.PolycyclicRecognition.transferredMap_one_close line 38
Source documentation
The transferred identity has the same error as f ∘ r.
```
theorem transferredMap_one_close (f : H → X) (r : X → H) (E' : ℝ)
    (hfr : ∀ x, dist (f (r x)) x ≤ E') (x : X) :
    dist (transferredMap f r 1 x) x ≤ E' := by
…
```
Mentions: OAI.PolycyclicRecognition.transferredMap

theorem OAI.PolycyclicRecognition.transferredMap_mul_close line 46

Source documentation

The error in the transferred action law is uniform in both group elements.

theorem transferredMap_mul_close (f : H → X) (r : X → H)
    (hleft : ∀ h a b : H, dist (h * a) (h * b) = dist a b)
    (K C E : ℝ) (hK : 0 ≤ K)
    (hf : ∀ a b, dist (f a) (f b) ≤ K * dist a b + C)
    (hrf : ∀ a, dist (r (f a)) a ≤ E) (h k : H) (x : X) :
    dist (transferredMap f r h (transferredMap f r k x))
      (transferredMap f r (h * k) x) ≤ K * E + C := by
…

Mentions: OAI.PolycyclicRecognition.transferredMap

theorem OAI.PolycyclicRecognition.transferredMap_orbit_close line 63

Source documentation

The transferred action agrees coarsely with left translation on orbit points.

theorem transferredMap_orbit_close (f : H → X) (r : X → H)
    (hleft : ∀ h a b : H, dist (h * a) (h * b) = dist a b)
    (K C E : ℝ) (hK : 0 ≤ K)
    (hf : ∀ a b, dist (f a) (f b) ≤ K * dist a b + C)
    (hrf : ∀ a, dist (r (f a)) a ≤ E) (h k : H) :
    dist (transferredMap f r h (f k)) (f (h * k)) ≤ K * E + C := by
…

Mentions: OAI.PolycyclicRecognition.transferredMap

theorem OAI.PolycyclicRecognition.transferredMap_coarse_upper line 78

Source documentation

Both coarse upper inequalities give one upper inequality for every transferred translation. The constants do not depend on the translating element.

theorem transferredMap_coarse_upper (f : H → X) (r : X → H)
    (hleft : ∀ h a b : H, dist (h * a) (h * b) = dist a b)
    (Kf Cf Kr Cr : ℝ) (hKf : 0 ≤ Kf)
    (hf : ∀ a b, dist (f a) (f b) ≤ Kf * dist a b + Cf)
    (hr : ∀ x y, dist (r x) (r y) ≤ Kr * dist x y + Cr)
    (h : H) (x y : X) :
    dist (transferredMap f r h x) (transferredMap f r h y) ≤
      (Kf * Kr) * dist x y + (Kf * Cr + Cf) := by
…

Mentions: OAI.PolycyclicRecognition.transferredMap

theorem OAI.PolycyclicRecognition.orbit_right_increment_bound line 96

Source documentation

A generator step has a uniform image length even when the word is in a subgroup equipped with its own generating set.

theorem orbit_right_increment_bound (f : H → X)
    (hleft : ∀ h a b : H, dist (h * a) (h * b) = dist a b)
    (K C : ℝ) (hf : ∀ a b, dist (f a) (f b) ≤ K * dist a b + C)
    (h t : H) :
    dist (f h) (f (h * t)) ≤ K * dist 1 t + C := by
…