OAI/GroupTheory/PolycyclicRecognition/Algebra/BasepointLabelStabilization.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.stable_label_independent_of_center line 15

   Source documentation

   A label already stable in scale is independent of the center once nearby-center comparisons hold along all diverging scales.

   theorem stable_label_independent_of_center
       {P X L : Type*} [PseudoMetricSpace X]
       (label : P → X → ℝ → L) {r₀ t η : ℝ} (ht : 0 < t) (hη : 0 < η)
       (hstable : ∀ p x r, r₀ ≤ r → label p x r = label p x r₀)
       (hcompare : ∀ (scale : ℕ → ℝ), Tendsto scale atTop atTop → StrictMono scale →
         (∀ n, 1 ≤ scale n) → (∀ n, 1 ≤ t * scale n) →
         ∀ p x y, (∀ n, dist x y ≤ η * scale n) →
           ∀ᶠ n in atTop, label p x (scale n) = label p y (t * scale n)) :
       ∀ p x y, label p x r₀ = label p y r₀ := by
   …

2. theorem OAI.PolycyclicRecognition.uniform_local_norm_bound_of_sequences line 52

   Source documentation

   Uniform control in a scale parameter follows from tests along arbitrary strictly increasing scales, with the same local-distance constraint.

   theorem uniform_local_norm_bound_of_sequences
       {P X W : Type*} [PseudoMetricSpace X] [NormedAddCommGroup W] [NormedSpace ℝ W]
       (error : P → X → X → W) {t η : ℝ} (ht : 0 < t)
       (hseq : ∀ (scale : ℕ → ℝ), Tendsto scale atTop atTop → StrictMono scale →
         (∀ n, 1 ≤ scale n) → (∀ n, 1 ≤ t * scale n) →
         ∀ (p : ℕ → P) (x y : ℕ → X), (∀ n, dist (x n) (y n) ≤ η * scale n) →
         Tendsto (fun n => (scale n)⁻¹ • error (p n) (x n) (y n)) atTop (𝓝 0)) :
       ∀ ε : ℝ, 0 < ε → ∃ R : ℝ, 1 ≤ R ∧ ∀ p x y r,
         R ≤ r → dist x y ≤ η * r → ‖error p x y‖ ≤ ε * r := by
   …