dissipation lower bound for classical solutions

For an admissible stream φ, κ > 0, and a classical solution θ with zero forcing and smooth periodic mean-zero datum g: min (1/4) (2π²κ) ‖g‖² ≤ κ ‖∇θ‖²_{L²_{t,x}}.

theorem AVenhance.Infra.Section5.RelativeError.classical_poincare {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {g : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsAdmissibleStream φ) (hsol : IsClassicalSol (streamVel φ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g θ) (hg : Homogenization.MeanZeroOn unitCube g) {t : ℝ} (ht : 0 ≤ t) : 4 * Real.pi ^ 2 * l2NormSq (θ t) ≤ gradNormSq (spaceGrad (θ t))

Mean-zero Poincaré along a classical solution, in multiplicative form.

theorem AVenhance.Infra.Section5.RelativeError.classical_dissipation_lower {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {g : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsAdmissibleStream φ) (hκ : 0 < κ) (hsol : IsClassicalSol (streamVel φ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g θ) (hg : Homogenization.MeanZeroOn unitCube g) : min (1 / 4) (2 * Real.pi ^ 2 * κ) * l2NormSq g ≤ κ * spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θ t) x

The dissipation lower bound for classical solutions with mean-zero datum.