Energy balance for the difference of two classical solutions with the same drift

w = θ - θ' solves ∂ₜ w + b·∇w - κ Δ w = div ((κ-κ') ∇θ'), hence d/dt ‖w‖² = -2κ ‖∇w‖² - 2(κ-κ') ⟨∇w, ∇θ'⟩.

theorem AVenhance.Infra.FullTheorem.NoSelectionInputs.cont_vecDot_grad {f g : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) : Continuous fun (x : Homogenization.Vec 2) => Homogenization.vecDot (spaceGrad f x) (spaceGrad g x)

theorem AVenhance.Infra.FullTheorem.NoSelectionInputs.vecDot_smul_right (a : Homogenization.Vec 2) (δ : ℝ) (b : Homogenization.Vec 2) : Homogenization.vecDot a (δ • b) = δ * Homogenization.vecDot a b

theorem AVenhance.Infra.FullTheorem.NoSelectionInputs.spaceGrad_const_mul {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (δ : ℝ) : (spaceGrad fun (y : Homogenization.Vec 2) => δ * f y) = fun (x : Homogenization.Vec 2) (i : Fin 2) => δ * spaceGrad f x i

theorem AVenhance.Infra.FullTheorem.NoSelectionInputs.vecDiv_smul_grad {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (δ : ℝ) (x : Homogenization.Vec 2) : vecDiv (fun (y : Homogenization.Vec 2) => δ • spaceGrad f y) x = δ * spaceLap f x

theorem AVenhance.Infra.FullTheorem.NoSelectionInputs.diff_energy_hasDerivAt {Ψ θ θ' : ℝ → Homogenization.Vec 2 → ℝ} {κ κ' : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} (hΨ : IsAdmissibleStream Ψ) (hθ : IsClassicalSol (streamVel Ψ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ) (hθ' : IsClassicalSol (streamVel Ψ) κ' (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ') {t : ℝ} (ht : 0 < t) : HasDerivAt (fun (s : ℝ) => ∫ (x : Homogenization.Vec 2) in unitCube, (θ s x - θ' s x) ^ 2) ((-2 * κ * ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecNormSq (spaceGrad (fun (y : Homogenization.Vec 2) => θ t y - θ' t y) x)) - 2 * (κ - κ') * ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (spaceGrad (fun (y : Homogenization.Vec 2) => θ t y - θ' t y) x) (spaceGrad (θ' t) x)) t