Reusable test duality for divergence terms with either sign.

theorem AVenhance.Infra.Section5.hMinusOneNorm_neg_vecDiv_le {F : Homogenization.Vec 2 → Homogenization.Vec 2} (hF : ContDiff ℝ (↑⊤) F) (hper : IsZ2Periodic F) : (hMinusOneNorm fun (x : Homogenization.Vec 2) => -vecDiv F x) ≤ ENNReal.ofReal √(gradNormSq F)

The sign of a divergence does not affect its homogeneous norm.

theorem AVenhance.Infra.Section5.timeHMinusOneNorm_neg_vecDiv_le {F : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hF : ∀ t ∈ Set.Ioo 0 1, ContDiff ℝ (↑⊤) (F t)) (hper : ∀ t ∈ Set.Ioo 0 1, IsZ2Periodic (F t)) : (timeHMinusOneNorm fun (t : ℝ) (x : Homogenization.Vec 2) => -vecDiv (F t) x) ≤ (∫⁻ (t : ℝ) in Set.Ioo 0 1, ENNReal.ofReal √(gradNormSq (F t)) ^ 2) ^ (1 / 2)

Time-integrated version of signed divergence duality.