Differential inequalities for E, G = ‖∇θ‖², H = ‖∇²θ‖²

For a classical solution θ of the drift streamVel Ψ with |∂_i b_k| ≤ Lu:

• E' = -2κ G;
• G' = -2κ H - 2 C_G, |C_G| ≤ 2 Lu G;
• H' = -2κ D - 2 C_H, |C_H| ≤ (κ/2) D + 4 (Lu²/κ) G + 2 Lu H, D = ‖∇³θ‖².

theorem AVenhance.Infra.FullTheorem.Separation.integral_vecNormSq_eq {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (w : List (Fin 2)) : ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecNormSq (spaceGrad (Section4.classicalWordDerivative w f) x) = en (0 :: w) f + en (1 :: w) f

‖∇∂^w f‖² = ‖∂_0 ∂^w f‖² + ‖∂_1 ∂^w f‖².

theorem AVenhance.Infra.FullTheorem.Separation.wDiss_eq {θ : ℝ → Homogenization.Vec 2 → ℝ} {s : ℝ} (hs : ContDiff ℝ (↑⊤) (θ s)) (w : List (Fin 2)) : wDiss w θ s = wEnergy (0 :: w) θ s + wEnergy (1 :: w) θ s

theorem AVenhance.Infra.FullTheorem.Separation.drift_slice {Ψ : ℝ → Homogenization.Vec 2 → ℝ} (hΨ : IsAdmissibleStream Ψ) (s : ℝ) : ContDiff ℝ (↑⊤) (streamVel Ψ s) ∧ IsZ2Periodic (streamVel Ψ s)

Smoothness and periodicity of the drift slices.

noncomputable def AVenhance.Infra.FullTheorem.Separation.gradE (θ : ℝ → Homogenization.Vec 2 → ℝ) (s : ℝ) : ℝ

The gradient energy ‖∇θ(s)‖².

Equations

• AVenhance.Infra.FullTheorem.Separation.gradE θ s = AVenhance.Infra.FullTheorem.Separation.wDiss [] θ s

noncomputable def AVenhance.Infra.FullTheorem.Separation.hessE (θ : ℝ → Homogenization.Vec 2 → ℝ) (s : ℝ) : ℝ

The Hessian energy ∑_{j,i} ‖∂_j ∂_i θ(s)‖².

Equations

• AVenhance.Infra.FullTheorem.Separation.hessE θ s = ∑ j : Fin 2, ∑ i : Fin 2, AVenhance.Infra.FullTheorem.Separation.wEnergy [j, i] θ s

noncomputable def AVenhance.Infra.FullTheorem.Separation.thirdD (θ : ℝ → Homogenization.Vec 2 → ℝ) (s : ℝ) : ℝ

The third-derivative dissipation ∑_{j,i} ‖∇∂_j∂_i θ(s)‖².

Equations

• AVenhance.Infra.FullTheorem.Separation.thirdD θ s = ∑ j : Fin 2, ∑ i : Fin 2, AVenhance.Infra.FullTheorem.Separation.wDiss [j, i] θ s

theorem AVenhance.Infra.FullTheorem.Separation.slice_smooth {Ψ θ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} (hsol : IsClassicalSol (streamVel Ψ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ) {s : ℝ} (hs : 0 ≤ s) : ContDiff ℝ (↑⊤) (θ s) ∧ IsZ2Periodic (θ s)

theorem AVenhance.Infra.FullTheorem.Separation.gradE_eq {Ψ θ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} (hsol : IsClassicalSol (streamVel Ψ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ) {s : ℝ} (hs : 0 ≤ s) : gradE θ s = en [0] (θ s) + en [1] (θ s)

theorem AVenhance.Infra.FullTheorem.Separation.gradE_nonneg {Ψ θ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} (hsol : IsClassicalSol (streamVel Ψ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ) {s : ℝ} (hs : 0 ≤ s) : 0 ≤ gradE θ s

theorem AVenhance.Infra.FullTheorem.Separation.hessE_nonneg {θ : ℝ → Homogenization.Vec 2 → ℝ} {s : ℝ} : 0 ≤ hessE θ s

theorem AVenhance.Infra.FullTheorem.Separation.thirdD_nonneg {Ψ θ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} (hsol : IsClassicalSol (streamVel Ψ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ) {s : ℝ} (hs : 0 ≤ s) : 0 ≤ thirdD θ s

theorem AVenhance.Infra.FullTheorem.Separation.hasDerivAt_E {Ψ θ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} (hΨ : IsAdmissibleStream Ψ) (hsol : IsClassicalSol (streamVel Ψ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ) {t : ℝ} (ht : 0 < t) : HasDerivAt (wEnergy [] θ) (-2 * κ * gradE θ t) t

theorem AVenhance.Infra.FullTheorem.Separation.hasDerivAt_G {Ψ θ : ℝ → Homogenization.Vec 2 → ℝ} {κ Lu : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} (hΨ : IsAdmissibleStream Ψ) (hsol : IsClassicalSol (streamVel Ψ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ) {t : ℝ} (ht : 0 < t) (hLu : ∀ (x : Homogenization.Vec 2) (i k : Fin 2), |spaceGrad (fun (y : Homogenization.Vec 2) => streamVel Ψ t y k) x i| ≤ Lu) : ∃ (C : ℝ), HasDerivAt (gradE θ) (-2 * κ * hessE θ t - 2 * C) t ∧ |C| ≤ 2 * Lu * gradE θ t

theorem AVenhance.Infra.FullTheorem.Separation.hasDerivAt_H {Ψ θ : ℝ → Homogenization.Vec 2 → ℝ} {κ Lu : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} (hΨ : IsAdmissibleStream Ψ) (hsol : IsClassicalSol (streamVel Ψ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ) {t : ℝ} (ht : 0 < t) (hκ : 0 < κ) (hLu : ∀ (x : Homogenization.Vec 2) (i k : Fin 2), |spaceGrad (fun (y : Homogenization.Vec 2) => streamVel Ψ t y k) x i| ≤ Lu) : ∃ (C : ℝ), HasDerivAt (hessE θ) (-2 * κ * thirdD θ t - 2 * C) t ∧ |C| ≤ κ / 2 * thirdD θ t + 4 * (Lu ^ 2 / κ) * gradE θ t + 2 * Lu * hessE θ t