OAI/GroupTheory/PolycyclicRecognition/Geometry/NetSmoothing.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolycyclicRecognition.netSmoothedMap line 19
2. theorem OAI.PolycyclicRecognition.net_union_support_diameter line 23
3. theorem OAI.PolycyclicRecognition.exists_uniform_net_smoothing line 44

   Source documentation

   The same constants work for every map with the prescribed coarse upper bound. All interpolation data are constructed from the fixed net.

   theorem exists_uniform_net_smoothing (c : ControlledContraction Y) (p₀ : Y)
       (hcover : ∀ x : X, ∃ v ∈ V, dist x v ≤ 1)
       (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) →
         LipschitzWith L (netSmoothedMap hV c p₀ f) ∧
           ∀ x, dist (netSmoothedMap hV c p₀ f x) (f x) ≤ E := by
   …

   Mentions: OAI.PolycyclicRecognition.ControlledContraction, OAI.PolycyclicRecognition.netSmoothedMap