Test duality for the divergence-form part of the tiny residual. The separate nondivergence summand needs the mean-zero and L² estimates, which are proved elsewhere; this file does not assume them.

theorem AVenhance.Infra.Section5.hMinusOneNorm_tiny_divergencePart_le (d e : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (t : ℝ) (hF : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => d t x + e t x) (hper : IsZ2Periodic fun (x : Homogenization.Vec 2) => d t x + e t x) : (hMinusOneNorm fun (x : Homogenization.Vec 2) => vecDiv (fun (y : Homogenization.Vec 2) => d t y + e t y) x) ≤ ENNReal.ofReal √(gradNormSq fun (x : Homogenization.Vec 2) => d t x + e t x)

At each time, the divergence part of tiny has the HDot⁻¹ bound given by the L² norm of its vector flux.