OAI/GroupTheory/PolycyclicRecognition/Algebra/OrderedInterpolationRadius.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform radius of interpolation on a bounded number of vertices

  1. theorem OAI.PolycyclicRecognition.listMass_tail_fraction_mem line 11
  2. def OAI.PolycyclicRecognition.InterpolationRadius line 23
  3. theorem OAI.PolycyclicRecognition.exists_interpolation_radius line 31

    Source documentation

    With at most n input vertices of bounded diameter, interpolation stays within a radius depending only on n, the diameter, and the contraction.

    theorem exists_interpolation_radius (c : ControlledContraction G) {D : ℝ} (hD : 0 ≤ D) (n : ℕ) :
    ∃ R : ℝ, 0 ≤ R ∧ InterpolationRadius (I := I) c D n R := by
…

    Mentions: OAI.PolycyclicRecognition.ControlledContraction, OAI.PolycyclicRecognition.InterpolationRadius