OAI/GroupTheory/PolycyclicRecognition/Analysis/SublinearRayIdentification.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.sublinear_error_on_linear_ray line 12

   Source documentation

   A metric sublinear error restricts to a sublinear error on every ray of at most linear metric growth. The additive constant may depend on the ray.

   theorem sublinear_error_on_linear_ray
       {X W : Type*} [PseudoMetricSpace X] [NormedAddCommGroup W]
       (base : X) (error : X → W) (ray : ℝ → X)
       (herror : ∀ ε : ℝ, 0 < ε → ∃ B : ℝ, ∀ x,
         ‖error x‖ ≤ ε * dist base x + B)
       {L C : ℝ} (hL : 0 ≤ L)
       (hmetric : ∀ t : ℝ, 0 ≤ t → dist base (ray t) ≤ L * t + C) :
       ∀ ε : ℝ, 0 < ε → ∃ R : ℝ, ∀ t : ℝ, R ≤ t → 0 ≤ t →
         ‖error (ray t)‖ ≤ ε * t := by
   …

2. theorem OAI.PolycyclicRecognition.uniform_transversal_affine_bound_of_ray_traces line 39

   Source documentation

   Averaging gives bounded trace errors with the source character. A sublinear comparison along height rays identifies each source character with the corresponding target character composed with the affine label.

   theorem uniform_transversal_affine_bound_of_ray_traces
       {P G D W I : Type*} [NormedAddCommGroup W] [NormedSpace ℝ W]
       [FiniteDimensional ℝ W] [Fintype I]
       (α β : I → Module.Dual ℝ W)
       (hsep : ∀ w, (∀ i, β i w = 0) → w = 0)
       (height : G → W) (η : P → G → W) (A : P → W →ₗ[ℝ] W)
       (d : D → G) (j₀ : D) (ray : W → ℝ → D)
       (hray : ∀ w t, height (d (ray w t)) = t • w)
       {B : ℝ} (hB : 0 ≤ B)
       (htrace : ∀ p j i,
         |β i (η p (d j) - η p (d j₀)) - α i (height (d j))| ≤ B)
       (hsub : ∀ p w ε, 0 < ε → ∃ R : ℝ, ∀ t, R ≤ t → 0 ≤ t →
   …