BackwardRecurrenceAsymptotics.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Subexponential mass and success probability in backward recurrence

theorem OAI.PolycyclicRecognition.subexponential_backward_masses 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 (h : ℕ) (a D : ℕ → ℝ → ℝ)
    (hlast : HasSubexponentialLowerBound (a h))
    (hD : ∀ j, j < h → HasSubexponentialUpperBound (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 → HasSubexponentialLowerBound (a j) := by
…

Mentions: OAI.PolycyclicRecognition.HasSubexponentialLowerBound, OAI.PolycyclicRecognition.HasSubexponentialUpperBound

theorem OAI.PolycyclicRecognition.subexponential_switch_product line 47

Source documentation

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

theorem subexponential_switch_product (τ : ℕ → ℝ → ℝ≥0) (n k : ℕ)
    (hτ : ∀ j, n ≤ j → j < n + k →
      HasSubexponentialLowerBound (fun r => (τ j r : ℝ))) :
    HasSubexponentialLowerBound (fun r => (switchThresholdProduct (fun j => τ j r) n k).toReal) := by
…

Mentions: OAI.PolycyclicRecognition.HasSubexponentialLowerBound, OAI.PolycyclicRecognition.switchThresholdProduct

theorem OAI.PolycyclicRecognition.subexponential_backward_thresholds line 62

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 (h : ℕ) (a D : ℕ → ℝ → ℝ)
    (hlast : HasSubexponentialLowerBound (a h))
    (hD : ∀ j, j < h → HasSubexponentialUpperBound (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 → HasSubexponentialLowerBound (fun r => a (j + 1) r / (2 * D j r)) := by
…

Mentions: OAI.PolycyclicRecognition.HasSubexponentialLowerBound, OAI.PolycyclicRecognition.HasSubexponentialUpperBound