Quantitative viscous error for weak solutions

For a weak solution with divergence-free drift and diffusivity κ > 0, |∫∫ (-θ ∂ₜφ - θ b·∇φ) - ∫ θ₀ φ(0)| ≤ (√κ/2) (‖θ₀‖²/2 + ∑ᵢ V Cᵢ²), where Cᵢ bounds ∂ᵢφ on the cell and V is the volume of the space-time cell.

theorem AVenhance.Infra.FullTheorem.TransportLimit.solution_viscous_error {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (h : DriftHyp b) {κ : ℝ} (hκ : 0 < κ) {θ₀ : Homogenization.Vec 2 → ℝ} (hθ₀ : Homogenization.MemL2On unitCube θ₀) {θ : ℝ → Homogenization.Vec 2 → ℝ} {Dθ : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hu : IsWeakSolutionGrad b κ θ₀ θ Dθ) {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsTestFunction φ) {Cg : Fin 2 → ℝ} (hCg : ∀ (i : Fin 2), ∀ p ∈ timeCube, |spaceGrad (φ p.1) p.2 i| ≤ Cg i) : |(∫ (p : ℝ × Homogenization.Vec 2) in timeCube, -θ p.1 p.2 * deriv (fun (s : ℝ) => φ s p.2) p.1 - θ p.1 p.2 * Homogenization.vecDot (b p.1 p.2) (spaceGrad (φ p.1) p.2)) - ∫ (x : Homogenization.Vec 2) in unitCube, θ₀ x * φ 0 x| ≤ √κ / 2 * (l2NormSq θ₀ / 2 + ∑ i : Fin 2, (MeasureTheory.volume.restrict timeCube).real Set.univ * Cg i ^ 2)