PolynomialTripling.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Polynomial upper growth supplies arbitrarily large tripling scales

Only an upper polynomial estimate is needed for the Haar averaging step: there are arbitrarily large radii where tripling the radius has bounded volume ratio. No full volume asymptotic or lower polynomial estimate is used.

theorem OAI.PolycyclicRecognition.exists_adjacent_nonincrease_of_tendsto_zero line 20
Source documentation
A positive sequence tending to zero cannot increase at every step.
```
theorem exists_adjacent_nonincrease_of_tendsto_zero
    (a : ℕ → ℝ) (ha : 0 < a 0) (hlim : Tendsto a atTop (𝓝 0)) :
    ∃ n, a (n + 1) ≤ a n := by
…
```

theorem OAI.PolycyclicRecognition.exists_geometric_growth_ratio line 30

Source documentation

An exponential upper bound forces one adjacent growth ratio below any fixed larger exponential rate.

theorem exists_geometric_growth_ratio
    (v : ℕ → ℝ) {C B : ℝ} (hB : 0 < B)
    (hv : ∀ n, 0 ≤ v n) (hv0 : 0 < v 0)
    (hbound : ∀ n, v n ≤ C * B ^ n) :
    ∃ n, v (n + 1) ≤ (2 * B) * v n := by
…

theorem OAI.PolycyclicRecognition.polynomial_tripling_at_arbitrarily_large_radii line 61

Source documentation

Positive polynomial volume growth admits a tripling estimate at some radius above every prescribed threshold.

theorem polynomial_tripling_at_arbitrarily_large_radii
    (v : ℝ → ℝ) {C : ℝ} (d : ℕ)
    (hv : ∀ r, 1 ≤ r → 0 < v r)
    (hbound : ∀ r, 1 ≤ r → v r ≤ C * r ^ d) :
    ∀ R : ℝ, ∃ T : ℝ, R ≤ T ∧ 1 ≤ T ∧ v (3 * T) ≤ (2 * (3 : ℝ) ^ d) * v T := by
…