The classical forced energy estimate

forced_energy_estimate: the energy-estimate form of the classical forced bound for the error w = u - v between a classical solution u with zero forcing and an arbitrary jointly C² periodic comparison function v, in terms of the L²(0,1; HDot⁻¹) norm of the defect advDiffOp b κ v.

Proof chain (each step a separate module): Energy/TimeDerivative (energy differentiable), Energy/Rate (rate identity, IBP and transport cancellation), Energy/Duality (HDot⁻¹ pairing), Energy/Inequality (Young), Energy/Abstract (integration of the a.e. differential inequality), Energy/FiniteNorm (consequences of hfin), Energy/Integrated (assembly), and the elementary square-root step below.

theorem AVenhance.Infra.Section5.Integration.sqrt_energy_arith {a b E₀ F κ : ℝ} (hκ : 0 < κ) (hE₀ : 0 ≤ E₀) (hF : 0 ≤ F) (ha : a ≤ E₀ + F ^ 2 / κ) (hb : κ * b ≤ E₀ + F ^ 2 / κ) : √a + √κ * √b ≤ 2 * (√E₀ + F / √κ)

The elementary square-root arithmetic of the final step.

theorem AVenhance.Infra.Section5.Integration.forced_energy_estimate {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsAdmissibleStream φ) {κ : ℝ} (hκ : 0 < κ) {θ₀ : Homogenization.Vec 2 → ℝ} {u v : ℝ → Homogenization.Vec 2 → ℝ} (hu : IsClassicalSol (streamVel φ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ u) (hv : ContDiffOn ℝ 2 (fun (p : ℝ × Homogenization.Vec 2) => v p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) (hvs : ∀ (t : ℝ), 0 ≤ t → ContDiff ℝ (↑⊤) (v t)) (hvp : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (v t)) (hfin : (timeHMinusOneNorm fun (s : ℝ) (x : Homogenization.Vec 2) => advDiffOp (streamVel φ) κ v s x) ≠ ⊤) (t : ℝ) : t ∈ Set.Icc 0 1 → √(l2NormSq fun (x : Homogenization.Vec 2) => u t x - v t x) + √κ * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (u s) x - spaceGrad (v s) x) ≤ 2 * (√(l2NormSq fun (x : Homogenization.Vec 2) => u 0 x - v 0 x) + (timeHMinusOneNorm fun (s : ℝ) (x : Homogenization.Vec 2) => advDiffOp (streamVel φ) κ v s x).toReal / √κ)

The classical forced energy estimate (standard: test the equation of w = u - v with w, the divergence-free drift drops out, pair the forcing -advDiffOp b κ v by HDot⁻¹ duality with ‖∇w(t)‖, Young, integrate in time). u is a classical solution with zero forcing; v is any jointly C² periodic function with smooth slices. The finiteness premise is essential: the toReal of an infinite norm is 0.