The differential energy inequality

For t > 0 with ‖f t‖_{HDot⁻¹} < ∞, where f = advDiffOp b κ v, d/dt ∫ w² + κ ∫ |∇w|² ≤ ‖f t‖²_{HDot⁻¹} / κ.

theorem AVenhance.Infra.Section5.Integration.Energy.young_energy {κ N G : ℝ} (hκ : 0 < κ) : 2 * (N * G) ≤ κ * G ^ 2 + N ^ 2 / κ

Young's inequality in the form used by the energy estimate.

theorem AVenhance.Infra.Section5.Integration.Energy.ForcedSetup.energy_inequality {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {u v : ℝ → Homogenization.Vec 2 → ℝ} (S : ForcedSetup φ κ θ₀ u v) {t : ℝ} (ht : 0 < t) (hfin : hMinusOneNorm (advDiffOp (streamVel φ) κ v t) ≠ ⊤) : (∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, 2 * (u t x - v t x) * deriv (fun (s : ℝ) => u s x - v s x) t) + κ * gradNormSq (spaceGrad fun (y : Homogenization.Vec 2) => u t y - v t y) ≤ (hMinusOneNorm (advDiffOp (streamVel φ) κ v t)).toReal ^ 2 / κ