Exponent lemmas for the leading-error estimate (e.leadingord)

Abstract-real arithmetic on the exponents q, γ, δ: the exponent of the χTilde · ∇G term dominates 2δ, so ε_m / ε_{m-1}^{1+γ/2} ≤ K ε_{m-1}^{2δ} follows from monotonicity of ε ↦ ε^s on (0, 1].

theorem AVenhance.Infra.Section5.RelativeError.one_lt_q_of_lt_four_thirds {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : 1 < q β

For 1 < β < 4/3 we have q > 1.

theorem AVenhance.Infra.Section5.RelativeError.corrector_second_term_exponent {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : 2 * delta β ≤ q β - 1 - gamma β / 2

Exponent of the χTilde · ∇G term dominates 2δ: ε_m/ε_{m-1}^{1+γ/2} ≤ K ε_{m-1}^{2δ} holds at the level of exponents, 2 δ ≤ q - 1 - γ/2.