OAI/GroupTheory/PolycyclicRecognition/Geometry/RootIntervalPadding.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.rootIntervalSupport_of_le line 17

   Source documentation

   Padding the fixed endpoint word does not enlarge any recurrence cell.

   theorem rootIntervalSupport_of_le (Exp : L → N) (hzero : Exp 0 = 1)
       {m : ℕ} (letters : Fin m → I) (X : I → L) (s : I → ℝ)
       (r R : ℝ) (j : ℕ) (hj : m ≤ j) (hR : 0 ≤ R) :
       rootIntervalSupport Exp letters X s r R j = {1} := by
   …

   Mentions: OAI.PolycyclicRecognition.rootIntervalSupport

2. theorem OAI.PolycyclicRecognition.rootIntervalSupport_mul_mem_padded line 32

   Source documentation

   A finite collection of denominator bounds covers the padded family.

   theorem rootIntervalSupport_mul_mem_padded (Exp : L → N) (hzero : Exp 0 = 1)
       {m : ℕ} (letters : Fin m → I) (X : I → L) (s : I → ℝ)
       (r R : ℝ) (hR : 0 ≤ R) {Q Q' : Set N} (hQQ : Q ⊆ Q')
       (hfinite : ∀ j : Fin m, ∀ x ∈ Q,
         ∀ u ∈ rootIntervalSupport Exp letters X s r R j.val, x * u ∈ Q') :
       ∀ j : ℕ, ∀ x ∈ Q, ∀ u ∈ rootIntervalSupport Exp letters X s r R j, x * u ∈ Q' := by
   …

   Mentions: OAI.PolycyclicRecognition.rootIntervalSupport