ScaleExtension.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Extending data from a strictly increasing sequence of scales

No regularity is imposed between the sampled scales. This bridge permits the uniform real-scale estimates to be applied to the original sequence data.

def OAI.PolycyclicRecognition.extendOnScales line 19
Source documentation
Extend the data by a fixed value outside the sampled scales.
```
def extendOnScales {α : Type*} (r : ℕ → ℝ) (f : ℕ → α) (z : α) (t : ℝ) : α := by
…
```
theorem OAI.PolycyclicRecognition.extendOnScales_apply line 23
theorem OAI.PolycyclicRecognition.eventually_extendOnScales line 33
Source documentation
Eventually true assertions on the indices hold at every sufficiently large scale in the range; off that range the fixed default is used.
```
theorem eventually_extendOnScales {α : Type*} {r : ℕ → ℝ} (hr : StrictMono r)
    (f : ℕ → α) (z : α) (P : ℝ → α → Prop)
    (hz : ∀ t, P t z) (hf : ∀ᶠ n in atTop, P (r n) (f n)) :
    ∀ᶠ t in atTop, P t (extendOnScales r f z t) := by
…
```
Mentions: OAI.PolycyclicRecognition.extendOnScales
theorem OAI.PolycyclicRecognition.tendsto_extendOnScales line 51