The energy rate identity for w = u - v

For t > 0, d/dt ∫ w² = ∫ 2 w ∂ₜ w = -2κ ∫ |∇w|² - 2 ∫ f w (Laplacian integration by parts and cancellation of the divergence-free transport term).

theorem AVenhance.Infra.Section5.Integration.Energy.continuous_spaceGrad_component {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (i : Fin 2) : Continuous fun (x : Homogenization.Vec 2) => spaceGrad f x i

theorem AVenhance.Infra.Section5.Integration.Energy.continuous_spaceLap {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) : Continuous (spaceLap f)

theorem AVenhance.Infra.Section5.Integration.Energy.continuous_vecDot_of {f g : Homogenization.Vec 2 → Homogenization.Vec 2} (hf : Continuous f) (hg : Continuous g) : Continuous fun (x : Homogenization.Vec 2) => Homogenization.vecDot (f x) (g x)

theorem AVenhance.Infra.Section5.Integration.Energy.ForcedSetup.forcing_slice_continuous {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {u v : ℝ → Homogenization.Vec 2 → ℝ} (S : ForcedSetup φ κ θ₀ u v) {t : ℝ} (ht : 0 < t) : Continuous fun (x : Homogenization.Vec 2) => advDiffOp (streamVel φ) κ v t x

The slice of the forcing is continuous at positive times.

theorem AVenhance.Infra.Section5.Integration.Energy.ForcedSetup.energy_rate {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {u v : ℝ → Homogenization.Vec 2 → ℝ} (S : ForcedSetup φ κ θ₀ u v) {t : ℝ} (ht : 0 < 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 = (-(2 * κ) * ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, Homogenization.vecDot (spaceGrad (fun (y : Homogenization.Vec 2) => u t y - v t y) x) (spaceGrad (fun (y : Homogenization.Vec 2) => u t y - v t y) x)) - 2 * ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, advDiffOp (streamVel φ) κ v t x * (u t x - v t x)

Energy rate identity for the error w = u - v at positive times.