The tail piece w = θ − θ_M (analytic case of r.LeBron.2)

Sup bound ‖w(t)‖ ≤ 2 C_t (1+A)^β ε_M^{a} ‖θ₀‖ (a = qβ − (β-γ) > 0) from the sup-in-time stream-difference estimate and the classical energy bound; Hölder bound ‖w(t) − w(s)‖ ≲ ε_M^{-(β-γ)/2} h^{1/4} ‖θ₀‖_{H¹} from Lemma U twice; interpolation by holder_step gives ‖w(t) − w(s)‖ ≤ K_w ‖θ₀‖_{H¹} h^{μ_w} uniformly in κ, M.

theorem AVenhance.Infra.FullTheorem.tail_ratio_le {Ct A E E' q β s κ : ℝ} (hE : 0 < E) (hE' : 0 ≤ E') (hE'le : E' ≤ (1 + A) * E ^ q) (hA : 0 ≤ A) (hCt : 0 ≤ Ct) (hβ : 0 ≤ β) (hκ : 1 / 2 * E ^ s ≤ κ) : Ct * E' ^ β / κ ≤ 2 * Ct * (1 + A) ^ β * E ^ (q * β - s)

Abstract real algebra of the tail ratio C ε_{M+1}^β / κ.

theorem AVenhance.Infra.FullTheorem.classical_sqrt_energy_le {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (M : ℕ) {κ : ℝ} (hκ : 0 < κ) {θ₀ : Homogenization.Vec 2 → ℝ} (hθ₀ : ContDiff ℝ (↑⊤) θ₀) {θM : ℝ → Homogenization.Vec 2 → ℝ} (hθM : IsClassicalSol (streamVel (Φ M)) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θM) : √κ * √(spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θM t) x) ≤ √(l2NormSq θ₀)

Classical energy bound √κ ‖∇θ_M‖ ≤ ‖θ₀‖.