Scale comparison for the flip-flop

|log (ε_{n+1}^{β-γ} / ε_n^{β+γ})| ≤ 2 (β-γ) K_s ε_n for n ≥ 1, where K_s = max 10 (supergeoConstant β); and the identity a_n² ε_n⁴ = ε_n^{2β}.

noncomputable def AVenhance.Infra.FullTheorem.FlipFlop.ksConst (β : ℝ) : ℝ

The constant of the two-sided supergeometric comparison.

Equations

• AVenhance.Infra.FullTheorem.FlipFlop.ksConst β = max 10 (AVenhance.Infra.Ingredients.supergeoConstant β)

theorem AVenhance.Infra.FullTheorem.FlipFlop.ksConst_ge_ten (β : ℝ) : 10 ≤ ksConst β

theorem AVenhance.Infra.FullTheorem.FlipFlop.beta_sub_gamma_pos {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : 0 < β - gamma β

theorem AVenhance.Infra.FullTheorem.FlipFlop.log_eps_ratio {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {n : ℕ} (hn : 1 ≤ n) (hsmall : 2 * ksConst β * epsilon β Λ n ≤ 1) : |Real.log (epsilon β Λ (n + 1) ^ (β - gamma β) / epsilon β Λ n ^ (β + gamma β))| ≤ 2 * (β - gamma β) * ksConst β * epsilon β Λ n

theorem AVenhance.Infra.FullTheorem.FlipFlop.a_sq_mul_eps_four {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (n : ℕ) : a β Λ n ^ 2 * epsilon β Λ n ^ 4 = epsilon β Λ n ^ (2 * β)

a_n² ε_n⁴ = ε_n^{2β}.