OAI/GroupTheory/PolycyclicRecognition/Algebra/SequenceSubsequences.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.HasSubexponentialLowerBoundSeq.comp line 13

   Source documentation

   Subexponential losses are unchanged on a subsequence tending to infinity.

   theorem HasSubexponentialLowerBoundSeq.comp {scale f : ℕ → ℝ} {v : ℕ → ℕ}
       (hf : HasSubexponentialLowerBoundSeq scale f) (hv : Tendsto v atTop atTop) :
       HasSubexponentialLowerBoundSeq (scale ∘ v) (f ∘ v) :=
   …

   Mentions: OAI.PolycyclicRecognition.HasSubexponentialLowerBoundSeq

2. theorem OAI.PolycyclicRecognition.HasSubexponentialUpperBoundSeq.comp line 18
3. theorem OAI.PolycyclicRecognition.exists_increasing_good_scale_subsequence line 26

   Source documentation

   The eventual cell and slack conditions can hold at every retained index, while the physical scales are strictly increasing. No interpolation of the profiles or of the group laws is needed.

   theorem exists_increasing_good_scale_subsequence {scale : ℕ → ℝ}
       (hscale : Tendsto scale atTop atTop) {P : ℕ → Prop} (hP : ∀ᶠ n in atTop, P n) :
       ∃ u : ℕ → ℕ, StrictMono u ∧ StrictMono (scale ∘ u) ∧ ∀ n, P (u n) := by
   …