Source consequences for the magnitudes of the time scales.

theorem AVenhance.Infra.Ingredients.TimeScaleBounds.epsilon_le_one {β : ℝ} {Λ m : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) : epsilon β Λ m ≤ 1

theorem AVenhance.Infra.Ingredients.TimeScaleBounds.rpow_ceil_bounds {x : ℝ} (hx : 1 ≤ x) : x ≤ ↑⌈x⌉₊ ∧ ↑⌈x⌉₊ ≤ 2 * x

theorem AVenhance.Infra.Ingredients.TimeScaleBounds.tauPP_rpow_bounds {β : ℝ} {Λ m : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (_hm : 1 ≤ m) : 2 ^ (-26) * epsilon β Λ (m - 1) ^ (2 - β + 2 * delta β) ≤ tauPP β Λ m ∧ tauPP β Λ m ≤ 2 ^ (-25) * epsilon β Λ (m - 1) ^ (2 - β + 2 * delta β)

theorem AVenhance.Infra.Ingredients.tauPP_bounds {β : ℝ} {Λ m : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (hm : 1 ≤ m) : 2 ^ (-26) * epsilon β Λ (m - 1) ^ (2 - β + 2 * delta β) ≤ tauPP β Λ m ∧ tauPP β Λ m ≤ 2 ^ (-25) * epsilon β Λ (m - 1) ^ (2 - β + 2 * delta β)

e.taubounds (1153-1168), corrected: the τ'' lower constant is 2⁻²⁶; its upper constant is 2⁻²⁵.

theorem AVenhance.Infra.Ingredients.tau_bounds {β : ℝ} {Λ m : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (hm : 1 ≤ m) : 2 ^ (-33) * epsilon β Λ (m - 1) ^ (2 - β + 4 * delta β) ≤ tau β Λ m ∧ tau β Λ m ≤ 2 ^ (-28) * epsilon β Λ (m - 1) ^ (2 - β + 4 * delta β)

e.taubounds (1153-1168): the stated τ_m bounds.