The energy inequality for the time primitive of a kernel convolution #
For a weak heat solution and a smooth compact kernel k, the time primitive
W(t) = k ⋆ w₀ + ∫ₐᵗ G of the convolved source is square integrable in space
for every t ∈ [a, τ], and
‖W(t)‖² + ∫ₐᵗ ‖∇(k ⋆ w)‖² ≤ ‖k ⋆ w₀‖² + ∫ₐᵗ (‖k ⋆ H‖² + ‖k ⋆ w‖² + ‖k ⋆ f‖²)
(lem:localized-vorticity-energy of the Escauriaza–Seregin–Šverák manuscript).
theorem
CKN.vlSource_intervalIntegrable
{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)
(x : Foundation.Parabolic.Vec3)
{t : ℝ}
(ht : t ∈ Set.Icc a τ)
:
IntervalIntegrable (fun (s : ℝ) => vlSource k w H f x s) MeasureTheory.volume a t
theorem
CKN.vlPrim_sq_eq
{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)
(x : Foundation.Parabolic.Vec3)
{t : ℝ}
(ht : t ∈ Set.Icc a τ)
:
The squared primitive at a point, with the primitive replaced inside the time integral by the convolution itself.
theorem
CKN.vlPrim_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)
{t : ℝ}
(ht : a ≤ t)
:
MeasureTheory.StronglyMeasurable fun (x : Foundation.Parabolic.Vec3) => vlPrim a k w₀ w H f x t
theorem
CKN.vlPrim_energy_le
{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)
{t : ℝ}
(ht : t ∈ Set.Icc a τ)
:
MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => vlPrim a k w₀ w H f x t) 2 MeasureTheory.volume ∧ (∫ (x : Foundation.Parabolic.Vec3), vlPrim a k w₀ w H f x t ^ 2) + ∫ (s : ℝ) in Set.Ioo a t, ∑ j : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), vlConvT (vlDeriv k j) w x s ^ 2 ≤ (∫ (x : Foundation.Parabolic.Vec3), vlConv k w₀ x ^ 2) + ∫ (s : ℝ) in Set.Ioo a t, ((∑ 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
The kernel energy inequality.