The energy inequality for a kernel convolution of a weak heat solution #
For a weak solution of ∂ₜ w - Δw = div H + f with initial trace w₀, and a
smooth compact kernel k, the primitive W = k ⋆ w from
CKN.vlConvT_ae_eq_prim satisfies, for every t ∈ [a, τ],
‖W(t)‖² + ∫ₐᵗ ‖∇(k ⋆ w)‖² ≤ ‖k ⋆ w₀‖² + ∫ₐᵗ (‖k ⋆ H‖² + ‖k ⋆ w‖² + ‖k ⋆ f‖²).
It is the energy identity of the pointwise time primitive, integrated in
space, with the whole-space integration by parts and Young's inequality
(lem:localized-vorticity-energy of the Escauriaza–Seregin–Šverák manuscript).
theorem
CKN.vlSource_stronglyMeasurable
{a τ : ℝ}
{w f : Foundation.Parabolic.Vec3 × ℝ → ℝ}
{H : Fin 3 → Foundation.Parabolic.Vec3 × ℝ → ℝ}
{w₀ : Foundation.Parabolic.Vec3 → ℝ}
(sol : VlHeatSolution a τ w H f w₀)
{k : Foundation.Parabolic.Vec3 → ℝ}
(hk : IsVlKernel k)
:
MeasureTheory.StronglyMeasurable fun (p : Foundation.Parabolic.Vec3 × ℝ) => vlSource k w H f p.1 p.2
theorem
CKN.vlSource_memLp
{a τ : ℝ}
{w f : Foundation.Parabolic.Vec3 × ℝ → ℝ}
{H : Fin 3 → Foundation.Parabolic.Vec3 × ℝ → ℝ}
{w₀ : Foundation.Parabolic.Vec3 → ℝ}
(sol : VlHeatSolution a τ w H f w₀)
{k : Foundation.Parabolic.Vec3 → ℝ}
(hk : IsVlKernel k)
:
MeasureTheory.MemLp (fun (p : Foundation.Parabolic.Vec3 × ℝ) => vlSource k w H f p.1 p.2) 2
(MeasureTheory.volume.restrict (vlSlab a τ))
theorem
CKN.vlSource_slice_pairing
{w f : Foundation.Parabolic.Vec3 × ℝ → ℝ}
{H : Fin 3 → Foundation.Parabolic.Vec3 × ℝ → ℝ}
{k : Foundation.Parabolic.Vec3 → ℝ}
(hk : IsVlKernel k)
{s : ℝ}
(hws : MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => w (y, s)) 2 MeasureTheory.volume)
(hHs : ∀ (j : Fin 3), MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => H j (y, s)) 2 MeasureTheory.volume)
(hfs : MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => f (y, s)) 2 MeasureTheory.volume)
:
∫ (x : Foundation.Parabolic.Vec3), vlConvT k w x s * vlSource k w H f x s = ((-∑ j : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), vlConvT (vlDeriv k j) w x s ^ 2) - ∑ j : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), vlConvT (vlDeriv k j) w x s * vlConvT k (H j) x s) + ∫ (x : Foundation.Parabolic.Vec3), vlConvT k w x s * vlConvT k f x s
The slice identity: whole-space integration by parts of the pairing of
k ⋆ w with the convolved source.
theorem
CKN.vlSource_slice_pairing_le
{w f : Foundation.Parabolic.Vec3 × ℝ → ℝ}
{H : Fin 3 → Foundation.Parabolic.Vec3 × ℝ → ℝ}
{k : Foundation.Parabolic.Vec3 → ℝ}
(hk : IsVlKernel k)
{s : ℝ}
(hws : MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => w (y, s)) 2 MeasureTheory.volume)
(hHs : ∀ (j : Fin 3), MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => H j (y, s)) 2 MeasureTheory.volume)
(hfs : MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => f (y, s)) 2 MeasureTheory.volume)
:
2 * ∫ (x : Foundation.Parabolic.Vec3), vlConvT k w x s * vlSource k w H f x s ≤ (-∑ j : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), vlConvT (vlDeriv k j) w x s ^ 2) + (((∑ j : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), vlConvT k (H j) x s ^ 2) + ∫ (x : Foundation.Parabolic.Vec3), vlConvT k w x s ^ 2) + ∫ (x : Foundation.Parabolic.Vec3), vlConvT k f x s ^ 2)
Young's inequality for the slice pairing.