Inner and top steps of the flip-flop

• inner_step: for a level m+1 ≥ 2, a diffusivity k with k ≤ C ε_{m+1}^{β+γ} and q_{m+1} ≤ C ε_m^{4δ}, the logarithms of the normalised KBar(k) and k have sum O(ε_m^δ);
• top_step: for k = t ε_{m+1}^{β-γ}, t ∈ [1/2, 2], log (KBar(k)/(√(9/80) ε_m^{β+γ})) is log (t √(80/9)) + O(ε_m^δ).

noncomputable def AVenhance.Infra.FullTheorem.FlipFlop.innerC (β C₀ C : ℝ) : ℝ

The relative error constant of the inner step.

Equations

• AVenhance.Infra.FullTheorem.FlipFlop.innerC β C₀ C = 80 / 9 * (C ^ 2 + AVenhance.Infra.Section3.lAmtOneStepConstant β C₀ * (C + 1))

theorem AVenhance.Infra.FullTheorem.FlipFlop.lAmt_ge_two {β C₀ : ℝ} (hC₀ : 0 ≤ C₀) : 2 ≤ Section3.lAmtOneStepConstant β C₀

theorem AVenhance.Infra.FullTheorem.FlipFlop.innerC_nonneg {β C₀ C : ℝ} (hC : 0 ≤ C) (hC₀ : 0 ≤ C₀) : 0 ≤ innerC β C₀ C

theorem AVenhance.Infra.FullTheorem.FlipFlop.sqrt_ninth_pos : 0 < √(9 / 80)

theorem AVenhance.Infra.FullTheorem.FlipFlop.sqrt_sq_ninth : √(9 / 80) * √(9 / 80) = 9 / 80

theorem AVenhance.Infra.FullTheorem.FlipFlop.sqrt_inv_mul : √(80 / 9) * √(9 / 80) = 1

theorem AVenhance.Infra.FullTheorem.FlipFlop.eps_two_gamma_le {β : ℝ} (I : Ingredients β) (m : ℕ) : epsilon β I.Λ (m + 1) ^ (2 * gamma β) ≤ epsilon β I.Λ m ^ delta β

ε_{m+1}^{2γ} ≤ ε_m^δ.

theorem AVenhance.Infra.FullTheorem.FlipFlop.eps_rpow_le_delta {β : ℝ} (I : Ingredients β) (m : ℕ) {s : ℝ} (hs : delta β ≤ s) : epsilon β I.Λ m ^ s ≤ epsilon β I.Λ m ^ delta β

ε^s ≤ ε^δ for s ≥ δ.

theorem AVenhance.Infra.FullTheorem.FlipFlop.inner_step {β C₀ C : ℝ} (I : Ingredients β) (hz : I.Czeta ≤ C₀) (hh : I.Chat ≤ C₀) (hC : 0 ≤ C) {m : ℕ} (hm : 1 ≤ m) {k : ℝ} (hk : 0 < k) (hkU : k ≤ C * epsilon β I.Λ (m + 1) ^ (β + gamma β)) (hq : epsilon β I.Λ (m + 1) ^ 2 / (k * tau β I.Λ (m + 1)) ≤ C * epsilon β I.Λ m ^ (4 * delta β)) (hr : innerC β C₀ C * epsilon β I.Λ m ^ delta β ≤ 1 / 2) (hsm : 2 * ksConst β * epsilon β I.Λ m ≤ 1) : |Real.log (I.KhomScalar k (m + 1) / (√(9 / 80) * epsilon β I.Λ m ^ (β + gamma β))) + Real.log (k / (√(9 / 80) * epsilon β I.Λ (m + 1) ^ (β + gamma β)))| ≤ (2 * innerC β C₀ C + 2 * (β - gamma β) * ksConst β) * epsilon β I.Λ m ^ delta β