OAI/GroupTheory/PolycyclicRecognition/Geometry/SmallHeightSamplingBall.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_small_height_sampling_ball line 18

   Source documentation

   Continuity at zero supplies the positive sampling radius; it is not an extra geometric hypothesis.

   theorem exists_small_height_sampling_ball (q : U →L[ℝ] W)
       (α : I → W →L[ℝ] ℝ) (hα : ∀ i, α i ≠ 0)
       {a : ℝ} (ha : 0 < a) :
       ∃ R : ℝ, 0 < R ∧ ∀ z ∈ Metric.closedBall (0 : U) R,
         q z ∈ (fun w : W => a • w) '' interior (weightSamplingPolytope α) := by
   …

   Mentions: OAI.PolycyclicRecognition.weightSamplingPolytope