OAI/GroupTheory/PolycyclicRecognition/Analysis/SequenceScaleExtraction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_strictMono_scale_subsequence line 14

   Source documentation

   A divergent real scale can be made strictly increasing and at least one by restricting the original sequence.

   theorem exists_strictMono_scale_subsequence (scale : ℕ → ℝ)
       (hs : Tendsto scale atTop atTop) :
       ∃ u : ℕ → ℕ, StrictMono u ∧ StrictMono (scale ∘ u) ∧
         ∀ n, 1 ≤ scale (u n) := by
   …

2. theorem OAI.PolycyclicRecognition.exists_constant_mode_strict_scale line 32

   Source documentation

   Fix a finite mode first, then make the real scales strictly increasing. This applies in particular to the finite family of word-basis selections.

   theorem exists_constant_mode_strict_scale {I : Type*} [Finite I]
       (mode : ℕ → I) (scale : ℕ → ℝ) (hs : Tendsto scale atTop atTop) :
       ∃ (i : I) (u : ℕ → ℕ), StrictMono u ∧ StrictMono (scale ∘ u) ∧
         (∀ n, 1 ≤ scale (u n)) ∧ ∀ n, mode (u n) = i := by
   …