UniformBasepointHeight.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A uniform sublinear height error from stabilized basepoint labels

theorem OAI.PolycyclicRecognition.uniform_sublinear_height_of_stable_labels line 14

Source documentation

Scale stabilization and the proved basepoint comparison select one linear label per map, uniformly at all centers. The error is sublinear uniformly in the map and in the two centers.

theorem uniform_sublinear_height_of_stable_labels
    {P G L W : Type*} [Group G] [PseudoMetricSpace G]
    [NormedAddCommGroup W] [NormedSpace ℝ W]
    (label : P → G → ℝ → L) (A : L → W →L[ℝ] W)
    (J : P → G → W) (π : G → W)
    {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 : ℕ → P) (x y : ℕ → G), (∀ n, dist (x n) (y n) ≤ η * scale n) →
      (∀ᶠ n in atTop, label (p n) (x n) (scale n) = label (p n) (y n) (t * scale n)) ∧
      Tendsto (fun n => (scale n)⁻¹ • (J (p n) (y n) - J (p n) (x n) -
…

theorem OAI.PolycyclicRecognition.uniform_sublinear_of_local_radius_bound line 49

Source documentation

A uniform error bound on expanding metric balls has the usual global sublinear form, including an additive constant for the bounded initial range.

theorem uniform_sublinear_of_local_radius_bound
    {P X W : Type*} [PseudoMetricSpace X] [NormedAddCommGroup W]
    (error : P → X → X → W) {η : ℝ} (hη : 0 < η)
    (hlocal : ∀ ε : ℝ, 0 < ε → ∃ R : ℝ, 1 ≤ R ∧ ∀ p x y r,
      R ≤ r → dist x y ≤ η * r → ‖error p x y‖ ≤ ε * r) :
    ∀ ε : ℝ, 0 < ε → ∃ C : ℝ, 0 ≤ C ∧ ∀ p x y,
      ‖error p x y‖ ≤ ε * dist x y + C := by
…

theorem OAI.PolycyclicRecognition.centered_uniform_height_of_two_point_estimate line 73

Source documentation

The global two-center estimate gives exactly the centered height estimate used to construct the boundary maps, with one constant for all centers and all maps.

theorem centered_uniform_height_of_two_point_estimate
    {P G W : Type*} [Group G] [PseudoMetricSpace G] [IsIsometricSMul G G]
    [NormedAddCommGroup W] [NormedSpace ℝ W]
    (π : G →* Multiplicative W) (f : P → G → G) (A : P → W →L[ℝ] W)
    (hsub : ∀ ε : ℝ, 0 < ε → ∃ B : ℝ, 0 ≤ B ∧ ∀ p x y,
      ‖(π (f p y)).toAdd - (π (f p x)).toAdd - A p ((π (x⁻¹ * y)).toAdd)‖ ≤
        ε * dist x y + B) :
    ∀ ε : ℝ, 0 < ε → ∃ B : ℝ, 0 ≤ B ∧ ∀ p x g,
      ‖(π ((f p x)⁻¹ * f p (x * g))).toAdd - A p ((π g).toAdd)‖ ≤
        ε * dist 1 g + B := by
…