SlowPositiveSelection.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.PolycyclicRecognition.exists_slow_eventual_selection line 19
Source documentation
Countably many eventual properties can be followed at a slowly increasing index. This is used only for the shrinking profile neighborhoods.
```
theorem exists_slow_eventual_selection (P : ℕ → ℝ → Prop)
    (hP : ∀ j, ∀ᶠ r in atTop, P j r) :
    ∃ k : ℝ → ℕ, Tendsto k atTop atTop ∧ ∀ᶠ r in atTop, P (k r) r := by
…
```
theorem OAI.PolycyclicRecognition.exists_slow_subexponential_mass line 37
Source documentation
If every fixed good set has a positive eventual mass, the good set can shrink to its limiting profile slowly enough that its mass is exp(-o(r)).
```
theorem exists_slow_subexponential_mass (mass : ℕ → ℝ → ℝ)
    (hmass : ∀ j, ∃ c : ℝ, 0 < c ∧ ∀ᶠ r in atTop, c ≤ mass j r) :
    ∃ k : ℝ → ℕ, Tendsto k atTop atTop ∧
      HasSubexponentialLowerBound (fun r => mass (k r) r) := by
…
```
Mentions: OAI.PolycyclicRecognition.HasSubexponentialLowerBound