OAI/GroupTheory/PolycyclicRecognition/Analysis/LipschitzReplacement.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_lipschitz_replacement_constants line 16

   Source documentation

   Construct a uniformly close Lipschitz representative of every map with the given coarse upper bound. The net and its order are chosen here.

   theorem exists_lipschitz_replacement_constants
       {X Y : Type*} [Group X] [MetricSpace X] [ProperSpace X]
       [IsIsometricSMul X X] [MetricSpace Y]
       (c : ControlledContraction Y) (p₀ : Y)
       (hpath : ∀ g : X, ∃ γ : ℝ → X, γ 0 = 1 ∧ γ 1 = g ∧
         ∀ t ∈ Icc (0 : ℝ) 1, ∀ u ∈ Icc (0 : ℝ) 1,
           dist (γ t) (γ u) ≤ dist 1 g * |t - u|)
       {K C : ℝ} (hK : 0 ≤ K) (hC : 0 ≤ C) :
       ∃ L : ℝ≥0, ∃ E : ℝ, 0 ≤ E ∧ ∀ f : X → Y,
         (∀ x y, dist (f x) (f y) ≤ K * dist x y + C) →
         ∃ f' : C(X, Y), LipschitzWith L f' ∧ ∀ x, dist (f' x) (f x) ≤ E := by
   …

   Mentions: OAI.PolycyclicRecognition.ControlledContraction