The regularity of the vorticity on a product box

The time derivative of a solution of a heat equation in divergence form, from the second spatial derivatives and the derivative of the flux, and the conclusions of thm:vorticity-regularity on the product box B_{1/2} × (t₀ - 1/4, t₀): a continuous bounded representative of the vorticity, its space-time weak derivatives in L², and the pointwise differential inequality.

theorem ESS.vorticityHeat_timeDeriv {W : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} {w : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {g h F Fd : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hw : MeasureTheory.IntegrableOn w W MeasureTheory.volume) (hh : ∀ (j : Fin 3), MeasureTheory.IntegrableOn (h j) W MeasureTheory.volume) (hF : ∀ (j : Fin 3), MeasureTheory.IntegrableOn (F j) W MeasureTheory.volume) (hFd : ∀ (j : Fin 3), MeasureTheory.IntegrableOn (Fd j) W MeasureTheory.volume) (heq : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, w y * (-CKN.timePartial ψ y - ∑ j : Fin 3, CKN.spatialSecondPartial ψ j j y) = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, ∑ j : Fin 3, F j y * CKN.spatialPartial ψ j y) (hdw : ∀ (j : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, w y * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, g j y * ψ y) (hdg : ∀ (j : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, g j y * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, h j y * ψ y) (hdF : ∀ (j : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, F j y * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, Fd j y * ψ y) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) : ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, w y * CKN.timePartial ψ y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, (∑ j : Fin 3, h j y + ∑ j : Fin 3, Fd j y) * ψ y

The weak time derivative of a solution of a heat equation in divergence form.

theorem ESS.vorticity_abs_neg_sub_le (a b c d : ℝ) : |(-(a + b - (c + d)))| ≤ |a| + |b| + |c| + |d|

The absolute value of the negated difference of two sums of two terms.