OAI/GroupTheory/PolycyclicRecognition/Algebra/PerturbedInversePairs.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.inverse_error_of_bounded_perturbations line 13

   Source documentation

   Perturbing a coarse inverse pair preserves its inverse error with a constant determined only by the original controls and perturbation radii.

   theorem inverse_error_of_bounded_perturbations
       (f f' : X → Y) (g g' : Y → X)
       {Kg Cg Df Dg E : ℝ} (hKg : 0 ≤ Kg)
       (hg : ∀ y z, dist (g y) (g z) ≤ Kg * dist y z + Cg)
       (hfclose : ∀ x, dist (f' x) (f x) ≤ Df)
       (hgclose : ∀ y, dist (g' y) (g y) ≤ Dg)
       (hinv : ∀ x, dist (g (f x)) x ≤ E) (x : X) :
       dist (g' (f' x)) x ≤ Dg + (Kg * Df + Cg) + E := by
   …