SequenceRealExtension.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Extending a scale sequence without regularity assumptions

The geometric box lemmas use real scales. Arbitrary data on a strictly increasing scale sequence extend by zero off that sequence, preserving vanishing errors and subexponential upper bounds.

def OAI.PolycyclicRecognition.sequenceRealExtension line 19
Source documentation
No interpolation or regularity of the envelope is required.
```
def sequenceRealExtension (scale : ℕ → ℝ) (f : ℕ → ℝ) (r : ℝ) : ℝ := by
…
```
theorem OAI.PolycyclicRecognition.sequenceRealExtension_apply line 23
theorem OAI.PolycyclicRecognition.sequenceRealExtension_nonneg line 29
theorem OAI.PolycyclicRecognition.tendsto_sequenceRealExtension_zero line 39
Source documentation
A vanishing sequence of errors remains vanishing on the real scale.
```
theorem tendsto_sequenceRealExtension_zero (scale : ℕ → ℝ) (hs : StrictMono scale)
    (f : ℕ → ℝ) (hf : Tendsto f atTop (𝓝 0)) :
    Tendsto (sequenceRealExtension scale f) atTop (𝓝 0) := by
…
```
Mentions: OAI.PolycyclicRecognition.sequenceRealExtension
theorem OAI.PolycyclicRecognition.HasSubexponentialUpperBoundSeq.realExtension line 56
Source documentation
A sequential subexponential envelope is enough for the real-scale box estimates. Its zero extension imposes no restriction between samples.
```
theorem HasSubexponentialUpperBoundSeq.realExtension
    {scale f : ℕ → ℝ} (hf : HasSubexponentialUpperBoundSeq scale f)
    (hs : StrictMono scale) : HasSubexponentialUpperBound (sequenceRealExtension scale f) := by
…
```
Mentions: OAI.PolycyclicRecognition.HasSubexponentialUpperBoundSeq, OAI.PolycyclicRecognition.HasSubexponentialUpperBound, OAI.PolycyclicRecognition.sequenceRealExtension

theorem OAI.PolycyclicRecognition.sequenceRealExtension_eventually_abs_le_exp line 71

Source documentation

The same extension transports the exponentially bounded inside-letter parameters, together with their actual vanishing errors.

theorem sequenceRealExtension_eventually_abs_le_exp
    (scale : ℕ → ℝ) (hs : StrictMono scale) (t ε : ℕ → ℝ) (a : ℝ)
    (ht : ∀ᶠ n in atTop, |t n| ≤ Real.exp ((a + ε n) * scale n)) :
    ∀ᶠ r in atTop, |sequenceRealExtension scale t r| ≤
      Real.exp ((a + sequenceRealExtension scale ε r) * r) := by
…

Mentions: OAI.PolycyclicRecognition.sequenceRealExtension