Consequences of the flip-flop at a fixed level

For the two chains topped at ½ ε_M^p and 2 ε_M^p and a level 1 ≤ m ≤ M-1, with ε_m small: both diffusivities are ≍ ε_m^{β+γ} (explicit constants ffk0, ffK0) and their ratio is within [3,5] in one order or the other.

noncomputable def AVenhance.Infra.FullTheorem.NoSel.ffB : ℝ

Bound for |log (t √(80/9))| over t ∈ {1/2, 2}.

Equations

• AVenhance.Infra.FullTheorem.NoSel.ffB = |Real.log (1 / 2 * √(80 / 9))| + |Real.log (2 * √(80 / 9))|

noncomputable def AVenhance.Infra.FullTheorem.NoSel.ffk0 : ℝ

Lower constant: κ ≥ ffk0 · ε^{β+γ}.

Equations

• AVenhance.Infra.FullTheorem.NoSel.ffk0 = √(9 / 80) * Real.exp (-(AVenhance.Infra.FullTheorem.NoSel.ffB + 1))

noncomputable def AVenhance.Infra.FullTheorem.NoSel.ffK0 : ℝ

Upper constant: κ ≤ ffK0 · ε^{β+γ}.

Equations

• AVenhance.Infra.FullTheorem.NoSel.ffK0 = √(9 / 80) * Real.exp (AVenhance.Infra.FullTheorem.NoSel.ffB + 1)

theorem AVenhance.Infra.FullTheorem.NoSel.ffk0_pos : 0 < ffk0

theorem AVenhance.Infra.FullTheorem.NoSel.ffk0_le_ffK0 : ffk0 ≤ ffK0

theorem AVenhance.Infra.FullTheorem.NoSel.ffK0_pos : 0 < ffK0

theorem AVenhance.Infra.FullTheorem.NoSel.log_t_le (t : ℝ) (ht : t = 1 / 2 ∨ t = 2) : |Real.log (t * √(80 / 9))| ≤ ffB

theorem AVenhance.Infra.FullTheorem.NoSel.abs_sign_mul (k : ℕ) (x : ℝ) : |(-1) ^ k * x| = |x|

theorem AVenhance.Infra.FullTheorem.NoSel.kappa_facts (β C₀ : ℝ) : ∃ (Λ₁ : ℝ) (ρ : ℝ) (Cff : ℝ), 0 < ρ ∧ 0 ≤ Cff ∧ ∀ (I : Ingredients β), I.Czeta ≤ C₀ → I.Cxi ≤ C₀ → I.Chat ≤ C₀ → Λ₁ ≤ ↑I.Λ → ∀ (M : ℕ), 2 ≤ M → ∀ (m : ℕ), 1 ≤ m → m ≤ M - 1 → Cff * epsilon β I.Λ m ^ ρ ≤ Real.log (5 / 4) / 2 → 0 < I.kappaSeq (1 / 2 * epsilon β I.Λ M ^ (2 * β / (q β + 1))) M m → 0 < I.kappaSeq (2 * epsilon β I.Λ M ^ (2 * β / (q β + 1))) M m → (ffk0 * epsilon β I.Λ m ^ (β + gamma β) ≤ I.kappaSeq (1 / 2 * epsilon β I.Λ M ^ (2 * β / (q β + 1))) M m ∧ I.kappaSeq (1 / 2 * epsilon β I.Λ M ^ (2 * β / (q β + 1))) M m ≤ ffK0 * epsilon β I.Λ m ^ (β + gamma β)) ∧ (ffk0 * epsilon β I.Λ m ^ (β + gamma β) ≤ I.kappaSeq (2 * epsilon β I.Λ M ^ (2 * β / (q β + 1))) M m ∧ I.kappaSeq (2 * epsilon β I.Λ M ^ (2 * β / (q β + 1))) M m ≤ ffK0 * epsilon β I.Λ m ^ (β + gamma β)) ∧ (3 * I.kappaSeq (1 / 2 * epsilon β I.Λ M ^ (2 * β / (q β + 1))) M m ≤ I.kappaSeq (2 * epsilon β I.Λ M ^ (2 * β / (q β + 1))) M m ∧ I.kappaSeq (2 * epsilon β I.Λ M ^ (2 * β / (q β + 1))) M m ≤ 5 * I.kappaSeq (1 / 2 * epsilon β I.Λ M ^ (2 * β / (q β + 1))) M m ∨ 3 * I.kappaSeq (2 * epsilon β I.Λ M ^ (2 * β / (q β + 1))) M m ≤ I.kappaSeq (1 / 2 * epsilon β I.Λ M ^ (2 * β / (q β + 1))) M m ∧ I.kappaSeq (1 / 2 * epsilon β I.Λ M ^ (2 * β / (q β + 1))) M m ≤ 5 * I.kappaSeq (2 * epsilon β I.Λ M ^ (2 * β / (q β + 1))) M m)

Constants and level facts of the two chains.