The viscous remainder vanishes with the diffusivity

|κ ∫∫ D·G| ≤ (√κ/2) (κ ∫∫ |D|² + ∑ᵢ ∫∫ Gᵢ²) by a pointwise weighted Young inequality, so together with the energy bound κ ∫∫ |D|² ≤ ‖θ₀‖²/2 the remainder is O(√κ).

theorem AVenhance.Infra.FullTheorem.TransportLimit.abs_young_weighted (e x y : ℝ) (he : 0 ≤ e) : |e ^ 2 * (x * y)| ≤ e / 2 * (e ^ 2 * x ^ 2 + y ^ 2)

theorem AVenhance.Infra.FullTheorem.TransportLimit.kappa_term_bound {D G : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2} (hD : ∀ (i : Fin 2), MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => D p i) 2 (MeasureTheory.volume.restrict timeCube)) (hG : ∀ (i : Fin 2), MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => G p i) 2 (MeasureTheory.volume.restrict timeCube)) {κ : ℝ} (hκ : 0 < κ) : |κ * ∫ (p : ℝ × Homogenization.Vec 2) in timeCube, Homogenization.vecDot (D p) (G p)| ≤ √κ / 2 * ((κ * ∫ (p : ℝ × Homogenization.Vec 2) in timeCube, Homogenization.vecNormSq (D p)) + ∑ i : Fin 2, ∫ (p : ℝ × Homogenization.Vec 2) in timeCube, G p i ^ 2)