OAI/GroupTheory/PolycyclicRecognition/Analysis/SequenceBackwardAsymptotics.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.subexponential_backward_masses_sequence line 16

   Source documentation

   A fixed number of backward recurrence steps retains subexponential normalized mass. Both the initial mass and the enlargements may vary with the scale.

   theorem subexponential_backward_masses_sequence
       (scale : ℕ → ℝ) (hscale : Tendsto scale atTop atTop) (h : ℕ) (a D : ℕ → ℕ → ℝ)
       (hlast : HasSubexponentialLowerBoundSeq scale (a h))
       (hD : ∀ j, j < h → HasSubexponentialUpperBoundSeq scale (D j))
       (hDpos : ∀ j, j < h → ∀ᶠ r in atTop, 0 < D j r)
       (hstep : ∀ j, j < h → ∀ᶠ r in atTop,
         a (j + 1) r ^ 2 / (2 * D j r) ≤ a j r) :
       ∀ j, j ≤ h → HasSubexponentialLowerBoundSeq scale (a j) := by
   …

   Mentions: OAI.PolycyclicRecognition.HasSubexponentialLowerBoundSeq, OAI.PolycyclicRecognition.HasSubexponentialUpperBoundSeq

2. theorem OAI.PolycyclicRecognition.subexponential_switch_product_sequence line 48

   Source documentation

   A fixed ordered product of transition probabilities retains a subexponential lower bound.

   theorem subexponential_switch_product_sequence
       (scale : ℕ → ℝ) (hscale : Tendsto scale atTop atTop) (τ : ℕ → ℕ → ℝ≥0) (n k : ℕ)
       (hτ : ∀ j, n ≤ j → j < n + k →
         HasSubexponentialLowerBoundSeq scale (fun r => (τ j r : ℝ))) :
       HasSubexponentialLowerBoundSeq scale (fun r => (switchThresholdProduct (fun j => τ j r) n k).toReal) := by
   …

   Mentions: OAI.PolycyclicRecognition.HasSubexponentialLowerBoundSeq, OAI.PolycyclicRecognition.switchThresholdProduct

3. theorem OAI.PolycyclicRecognition.subexponential_backward_thresholds_sequence line 64

   Source documentation

   The normalized masses supplied by recurrence give the required lower bound on each threshold, with the same enlargement factors.

   theorem subexponential_backward_thresholds_sequence
       (scale : ℕ → ℝ) (hscale : Tendsto scale atTop atTop) (h : ℕ) (a D : ℕ → ℕ → ℝ)
       (hlast : HasSubexponentialLowerBoundSeq scale (a h))
       (hD : ∀ j, j < h → HasSubexponentialUpperBoundSeq scale (D j))
       (hDpos : ∀ j, j < h → ∀ᶠ r in atTop, 0 < D j r)
       (hstep : ∀ j, j < h → ∀ᶠ r in atTop,
         a (j + 1) r ^ 2 / (2 * D j r) ≤ a j r) :
       ∀ j, j < h → HasSubexponentialLowerBoundSeq scale (fun r => a (j + 1) r / (2 * D j r)) := by
   …

   Mentions: OAI.PolycyclicRecognition.HasSubexponentialLowerBoundSeq, OAI.PolycyclicRecognition.HasSubexponentialUpperBoundSeq