OAI/GroupTheory/PolycyclicRecognition/Analysis/TranslatedNegativeChains.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.left_translate_negative_chains line 17

   Source documentation

   A fixed left translate preserves a negative linear height margin, linear radius, and all unit-step bounds.

   theorem left_translate_negative_chains
       (η : G →* Multiplicative ℝ) (m : ℕ → ℕ) (z : ℕ → ℕ → G)
       {R gap : ℝ} (hR : 0 ≤ R) (hgap : 0 < gap)
       (hnegative : ∀ᶠ n : ℕ in atTop, ∀ i ≤ m n, (η (z n i)).toAdd ≤ -gap * n)
       (hball : ∀ᶠ n : ℕ in atTop, ∀ i ≤ m n, dist 1 (z n i) ≤ R * n)
       (hstep : ∀ᶠ n : ℕ in atTop, ∀ i < m n, dist (z n i) (z n (i + 1)) ≤ 1)
       (g : G) :
       ∃ B : ℝ, 0 ≤ B ∧
         (∀ᶠ n : ℕ in atTop, ∀ i ≤ m n, (η (g * z n i)).toAdd ≤ -(gap / 2) * n) ∧
         (∀ᶠ n : ℕ in atTop, ∀ i ≤ m n, dist 1 (g * z n i) ≤ B * n) ∧
         ∀ᶠ n : ℕ in atTop, ∀ i < m n, dist (g * z n i) (g * z n (i + 1)) ≤ 1 := by
   …

2. theorem OAI.PolycyclicRecognition.translated_negative_chain_endpoint_limit line 55

   Source documentation

   Apply a negative-chain contraction criterion after a fixed left translation, retaining the actual endpoint sequences.

   theorem translated_negative_chain_endpoint_limit
       {Q : Type*} [Group Q] [TopologicalSpace Q]
       (η : G →* Multiplicative ℝ) (observe : G → Q)
       (m : ℕ → ℕ) (z : ℕ → ℕ → G) {R gap : ℝ} (hR : 0 ≤ R) (hgap : 0 < gap)
       (hnegative : ∀ᶠ n : ℕ in atTop, ∀ i ≤ m n, (η (z n i)).toAdd ≤ -gap * n)
       (hball : ∀ᶠ n : ℕ in atTop, ∀ i ≤ m n, dist 1 (z n i) ≤ R * n)
       (hstep : ∀ᶠ n : ℕ in atTop, ∀ i < m n, dist (z n i) (z n (i + 1)) ≤ 1)
       (base target : ℕ → G) (hbase : ∀ n, z n 0 = base n)
       (htarget : ∀ᶠ n in atTop, z n (m n) = target n)
       (g : G)
       (criterion : ∀ (z' : ℕ → ℕ → G) (R' gap' : ℝ), 0 ≤ R' → 0 < gap' →
         (∀ᶠ n : ℕ in atTop, ∀ i ≤ m n, (η (z' n i)).toAdd ≤ -gap' * n) →
   …