Positivity and spacing facts for the time scales.

theorem AVenhance.Infra.Cutoff.q_eq_beta_div_four_sub_one {β : ℝ} (hβ : 1 < β) : q β = β / (4 * (β - 1))

theorem AVenhance.Infra.Cutoff.q_gt_one {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : 1 < q β

theorem AVenhance.Infra.Cutoff.delta_pos {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : 0 < delta β

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

theorem AVenhance.Infra.Cutoff.a_pos {β : ℝ} {Λ m : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) : 0 < a β Λ m

theorem AVenhance.Infra.Cutoff.tauPP_pos {β : ℝ} {Λ m : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) : 0 < tauPP β Λ m

theorem AVenhance.Infra.Cutoff.tauP_pos {β : ℝ} {Λ m : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) : 0 < tauP β Λ m

theorem AVenhance.Infra.Cutoff.four_tauP_le_tauPP {β : ℝ} {Λ m : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) : 4 * tauP β Λ m ≤ tauPP β Λ m