OAI/GroupTheory/PolycyclicRecognition/Geometry/OrderedInterpolationWeights.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolycyclicRecognition.InterpolationWeightControl line 11
2. theorem OAI.PolycyclicRecognition.exists_interpolation_weight_control line 22

   Source documentation

   On lists of bounded length and bounded image diameter, ordered interpolation is uniformly Lipschitz on probability weights. The stronger weighted estimate also covers vanishing tail masses in the recursion.

   theorem exists_interpolation_weight_control (c : ControlledContraction G)
       {D : ℝ} (hD : 0 ≤ D) (n : ℕ) :
       ∃ K : ℝ, 0 ≤ K ∧ InterpolationWeightControl (I := I) c D n K := by
   …

   Mentions: OAI.PolycyclicRecognition.ControlledContraction, OAI.PolycyclicRecognition.InterpolationWeightControl