The time derivative of a spatial convolution of a weak heat solution

Let w solve ∂ₜ w - Δw = div H + f in distributions on ℝ³ × (a, τ), with w, H, f ∈ L², and let its pairings with spatial tests have continuous versions whose value at a is the pairing with w₀. Then for every smooth compact kernel k and every point x, the convolution (k ⋆ w(s))(x) agrees for almost every s with the primitive (k ⋆ w₀)(x) + ∫ₐˢ ((Δk) ⋆ w + (∂ⱼk) ⋆ Hⱼ + k ⋆ f)(x). This is the time step of lem:localized-vorticity-energy of the Escauriaza–Seregin–Šverák manuscript.

def CKN.vlSlab (a τ : ℝ) : Set (Foundation.Parabolic.Vec3 × ℝ)

The space-time slab ℝ³ × (a, τ).

Equations

• CKN.vlSlab a τ = Set.univ ×ˢ Set.Ioo a τ

structure CKN.VlHeatSolution (a τ : ℝ) (w : Foundation.Parabolic.Vec3 × ℝ → ℝ) (H : Fin 3 → Foundation.Parabolic.Vec3 × ℝ → ℝ) (f : Foundation.Parabolic.Vec3 × ℝ → ℝ) (w₀ : Foundation.Parabolic.Vec3 → ℝ) : Prop

A distributional solution of ∂ₜ w - Δw = div H + f on ℝ³ × (a, τ) with square-integrable data, whose initial trace is w₀: every pairing with a spatial test has a continuous version on [a, τ] whose value at a is the pairing with w₀.

• lt : a < τ
• w_meas : MeasureTheory.StronglyMeasurable w
• H_meas (j : Fin 3) : MeasureTheory.StronglyMeasurable (H j)
• f_meas : MeasureTheory.StronglyMeasurable f
• w_L2 : MeasureTheory.MemLp w 2 (MeasureTheory.volume.restrict (vlSlab a τ))
• H_L2 (j : Fin 3) : MeasureTheory.MemLp (H j) 2 (MeasureTheory.volume.restrict (vlSlab a τ))
• f_L2 : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (vlSlab a τ))
• w₀_L2 : MeasureTheory.MemLp w₀ 2 MeasureTheory.volume
• weak (φ : Foundation.Parabolic.Vec3 × ℝ → ℝ) : φ ∈ spaceTimeTestFunction Set.univ (Set.Ioo a τ) → ∫ (p : Foundation.Parabolic.Vec3 × ℝ) in vlSlab a τ, w p * (-timePartial φ p - ∑ j : Fin 3, spatialSecondPartial φ j j p) = ∫ (p : Foundation.Parabolic.Vec3 × ℝ) in vlSlab a τ, -∑ j : Fin 3, H j p * spatialPartial φ j p + f p * φ p
• trace (ψ : Foundation.Parabolic.Vec3 → ℝ) : ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∃ (c : ℝ → ℝ), ContinuousOn c (Set.Icc a τ) ∧ c a = ∫ (x : Foundation.Parabolic.Vec3), w₀ x * ψ x ∧ ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a τ), c t = ∫ (x : Foundation.Parabolic.Vec3), w (x, t) * ψ x

noncomputable def CKN.vlConvT (k : Foundation.Parabolic.Vec3 → ℝ) (w : Foundation.Parabolic.Vec3 × ℝ → ℝ) (x : Foundation.Parabolic.Vec3) (s : ℝ) : ℝ

The convolution of the time slice at s.

Equations

• CKN.vlConvT k w x s = CKN.vlConv k (fun (y : CKN.Foundation.Parabolic.Vec3) => w (y, s)) x

noncomputable def CKN.vlSource (k : Foundation.Parabolic.Vec3 → ℝ) (w : Foundation.Parabolic.Vec3 × ℝ → ℝ) (H : Fin 3 → Foundation.Parabolic.Vec3 × ℝ → ℝ) (f : Foundation.Parabolic.Vec3 × ℝ → ℝ) (x : Foundation.Parabolic.Vec3) (s : ℝ) : ℝ

The convolved source ((Δk) ⋆ w + (∂ⱼk) ⋆ Hⱼ + k ⋆ f)(x, s).

Equations

• CKN.vlSource k w H f x s = ∑ j : Fin 3, CKN.vlConvT (CKN.vlDeriv (CKN.vlDeriv k j) j) w x s + ∑ j : Fin 3, CKN.vlConvT (CKN.vlDeriv k j) (H j) x s + CKN.vlConvT k f x s

noncomputable def CKN.vlPrim (a : ℝ) (k w₀ : Foundation.Parabolic.Vec3 → ℝ) (w : Foundation.Parabolic.Vec3 × ℝ → ℝ) (H : Fin 3 → Foundation.Parabolic.Vec3 × ℝ → ℝ) (f : Foundation.Parabolic.Vec3 × ℝ → ℝ) (x : Foundation.Parabolic.Vec3) (t : ℝ) : ℝ

The primitive from the convolved initial trace.

Equations

• CKN.vlPrim a k w₀ w H f x t = CKN.vlConv k w₀ x + ∫ (s : ℝ) in a..t, CKN.vlSource k w H f x s

theorem CKN.vlConv_apply_swap (k h : Foundation.Parabolic.Vec3 → ℝ) (x : Foundation.Parabolic.Vec3) : vlConv k h x = ∫ (y : Foundation.Parabolic.Vec3), h y * k (x - y)

theorem CKN.vlSlab_measure (a τ : ℝ) : MeasureTheory.volume.restrict (vlSlab a τ) = MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo a τ))

theorem CKN.vlSlab_memLp_shift {k : Foundation.Parabolic.Vec3 → ℝ} (hk : IsVlKernel k) (x : Foundation.Parabolic.Vec3) (a τ : ℝ) : MeasureTheory.MemLp (fun (p : Foundation.Parabolic.Vec3 × ℝ) => k (x - p.1)) 2 (MeasureTheory.volume.restrict (vlSlab a τ))

A shifted kernel is square integrable on the slab.

theorem CKN.vlSlab_integral_sep {a τ : ℝ} {g : Foundation.Parabolic.Vec3 × ℝ → ℝ} {k : Foundation.Parabolic.Vec3 → ℝ} (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (vlSlab a τ))) (hk : IsVlKernel k) (x : Foundation.Parabolic.Vec3) {η : ℝ → ℝ} (hη : Continuous η) (hηb : ∃ (C : ℝ), ∀ (s : ℝ), |η s| ≤ C) : MeasureTheory.Integrable (fun (p : Foundation.Parabolic.Vec3 × ℝ) => g p * (k (x - p.1) * η p.2)) (MeasureTheory.volume.restrict (vlSlab a τ)) ∧ ∫ (p : Foundation.Parabolic.Vec3 × ℝ) in vlSlab a τ, g p * (k (x - p.1) * η p.2) = ∫ (s : ℝ) in Set.Ioo a τ, η s * vlConvT k g x s

Fubini for a slab field against a separated weight.

theorem CKN.vlConvT_integrableOn {a τ : ℝ} {g : Foundation.Parabolic.Vec3 × ℝ → ℝ} {k : Foundation.Parabolic.Vec3 → ℝ} (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (vlSlab a τ))) (hk : IsVlKernel k) (x : Foundation.Parabolic.Vec3) : MeasureTheory.IntegrableOn (fun (s : ℝ) => vlConvT k g x s) (Set.Ioo a τ) MeasureTheory.volume

The convolved time slice is integrable in time.

theorem CKN.vlSource_integrableOn {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) : MeasureTheory.IntegrableOn (fun (s : ℝ) => vlSource k w H f x s) (Set.Ioo a τ) MeasureTheory.volume

theorem CKN.vlConvT_hasWeakDeriv {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) : HasWeakDerivOn (Set.Ioo a τ) (fun (s : ℝ) => vlConvT k w x s) fun (s : ℝ) => vlSource k w H f x s

The convolution of a weak heat solution has the convolved source as its weak time derivative.

theorem CKN.vlConvT_ae_eq_prim {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 : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a τ), vlConvT k w x t = vlPrim a k w₀ w H f x t

The convolution of a weak heat solution is, for almost every time, the primitive from its convolved initial trace.