Backward space-time mollification

The regularity bootstrap of thm:vorticity-regularity of the Escauriaza–Seregin–Šverák manuscript works on cylinders whose top is the terminal time of the hypotheses. A space-time mollification evaluated 5ε earlier in time only uses values of the field strictly below the top, so smooth approximations are available up to the top face. This file records the derivative formulas for kernels, the pairing identities with the reflected kernel, and the resulting pointwise form of constant-coefficient weak identities.

theorem CKN.vorticityBackVolumeIsAddHaarMeasure : MeasureTheory.volume.IsAddHaarMeasure

theorem CKN.vorticityKernelDeriv_contDiff {k : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hk : ContDiff ℝ (↑⊤) k) (v : Foundation.Parabolic.Vec3 × ℝ) : ContDiff ℝ ↑⊤ fun (t : Foundation.Parabolic.Vec3 × ℝ) => (fderiv ℝ k t) v

A directional derivative of a smooth compactly supported kernel is again smooth.

theorem CKN.vorticityKernelDeriv_hasCompactSupport {k : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hkc : HasCompactSupport k) (v : Foundation.Parabolic.Vec3 × ℝ) : HasCompactSupport fun (t : Foundation.Parabolic.Vec3 × ℝ) => (fderiv ℝ k t) v

A directional derivative of a compactly supported kernel is compactly supported.

theorem CKN.vorticityConvolution_eq_integral (k g : Foundation.Parabolic.Vec3 × ℝ → ℝ) (c : Foundation.Parabolic.Vec3 × ℝ) : MeasureTheory.convolution k g (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume c = ∫ (y : Foundation.Parabolic.Vec3 × ℝ), k (c - y) * g y

A scalar convolution is the integral of the reflected kernel against the function.

theorem CKN.vorticityKernel_convolution_fderiv {k f : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hk : ContDiff ℝ (↑⊤) k) (hkc : HasCompactSupport k) (hf : MeasureTheory.LocallyIntegrable f MeasureTheory.volume) (x v : Foundation.Parabolic.Vec3 × ℝ) : (fderiv ℝ (MeasureTheory.convolution k f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume) x) v = MeasureTheory.convolution (fun (t : Foundation.Parabolic.Vec3 × ℝ) => (fderiv ℝ k t) v) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x

The directional derivative of a convolution with a smooth compactly supported kernel is the convolution with the directional derivative of the kernel.

def CKN.vorticityBackShift (ε : ℝ) : Foundation.Parabolic.Vec3 × ℝ

The time shift (0, 5ε) of the backward mollifier.

Equations

• CKN.vorticityBackShift ε = (0, 5 * ε)

noncomputable def CKN.vorticityBackMollify (W : Set (Foundation.Parabolic.Vec3 × ℝ)) (f : Foundation.Parabolic.Vec3 × ℝ → ℝ) (ε : ℝ) (hε : 0 < ε) : Foundation.Parabolic.Vec3 × ℝ → ℝ

Backward mollification on W: the zero extension of f outside W, convolved with the space-time kernel of radius ε and evaluated at the earlier time t - 5ε.

Equations

• CKN.vorticityBackMollify W f ε hε z = CKN.spaceTimeMollify (W.indicator f) ε hε (z - CKN.vorticityBackShift ε)

noncomputable def CKN.vorticityBackTest (ε : ℝ) (hε : 0 < ε) (z : Foundation.Parabolic.Vec3 × ℝ) : Foundation.Parabolic.Vec3 × ℝ → ℝ

The reflected kernel centred at the shifted point: pairing a field with it evaluates the backward mollification at z.

Equations

• CKN.vorticityBackTest ε hε z y = CKN.spaceTimeMollifier ε hε (z - CKN.vorticityBackShift ε - y)

theorem CKN.vorticityBackMollify_contDiff {W : Set (Foundation.Parabolic.Vec3 × ℝ)} {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} {ε : ℝ} (hε : 0 < ε) (hf : MeasureTheory.LocallyIntegrable (W.indicator f) MeasureTheory.volume) : ContDiff ℝ (↑⊤) (vorticityBackMollify W f ε hε)

Backward mollification of an integrable zero extension is smooth.

theorem CKN.vorticityBackMollify_fderiv {W : Set (Foundation.Parabolic.Vec3 × ℝ)} {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} {ε : ℝ} (hε : 0 < ε) (hf : MeasureTheory.LocallyIntegrable (W.indicator f) MeasureTheory.volume) (z v : Foundation.Parabolic.Vec3 × ℝ) : (fderiv ℝ (vorticityBackMollify W f ε hε) z) v = MeasureTheory.convolution (fun (t : Foundation.Parabolic.Vec3 × ℝ) => (fderiv ℝ (spaceTimeMollifier ε hε) t) v) (W.indicator f) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume (z - vorticityBackShift ε)

The first derivative of a backward mollification is the backward convolution with the derivative of the kernel.

theorem CKN.vorticityBackMollify_fderiv_fderiv {W : Set (Foundation.Parabolic.Vec3 × ℝ)} {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} {ε : ℝ} (hε : 0 < ε) (hf : MeasureTheory.LocallyIntegrable (W.indicator f) MeasureTheory.volume) (z v w : Foundation.Parabolic.Vec3 × ℝ) : (fderiv ℝ (fun (y : Foundation.Parabolic.Vec3 × ℝ) => (fderiv ℝ (vorticityBackMollify W f ε hε) y) v) z) w = MeasureTheory.convolution (fun (t : Foundation.Parabolic.Vec3 × ℝ) => (fderiv ℝ (fun (t' : Foundation.Parabolic.Vec3 × ℝ) => (fderiv ℝ (spaceTimeMollifier ε hε) t') v) t) w) (W.indicator f) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume (z - vorticityBackShift ε)

The second derivative of a backward mollification is the backward convolution with the second derivative of the kernel.

theorem CKN.vorticityBackTest_contDiff {ε : ℝ} (hε : 0 < ε) (z : Foundation.Parabolic.Vec3 × ℝ) : ContDiff ℝ (↑⊤) (vorticityBackTest ε hε z)

The backward test is smooth.

theorem CKN.vorticityBackTest_tsupport_subset {ε : ℝ} (hε : 0 < ε) (z : Foundation.Parabolic.Vec3 × ℝ) : tsupport (vorticityBackTest ε hε z) ⊆ Metric.closedBall (z - vorticityBackShift ε) ε

The backward test is supported in the closed ball of radius ε about the shifted point.

theorem CKN.vorticityBackTest_hasCompactSupport {ε : ℝ} (hε : 0 < ε) (z : Foundation.Parabolic.Vec3 × ℝ) : HasCompactSupport (vorticityBackTest ε hε z)

The backward test has compact support.

theorem CKN.vorticityReflectedKernel_fderiv {k : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hk : ContDiff ℝ (↑⊤) k) (c y v : Foundation.Parabolic.Vec3 × ℝ) : (fderiv ℝ (fun (q : Foundation.Parabolic.Vec3 × ℝ) => k (c - q)) y) v = -(fderiv ℝ k (c - y)) v

Derivative of a reflected kernel.

theorem CKN.vorticityBackTest_pairing {W : Set (Foundation.Parabolic.Vec3 × ℝ)} (hW : MeasurableSet W) {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} {ε : ℝ} (hε : 0 < ε) (z : Foundation.Parabolic.Vec3 × ℝ) : ∫ (y : Foundation.Parabolic.Vec3 × ℝ) in W, f y * vorticityBackTest ε hε z y = vorticityBackMollify W f ε hε z

Pairing the zero extension with the backward test evaluates the backward mollification.

theorem CKN.vorticityBackTest_pairing_fderiv {W : Set (Foundation.Parabolic.Vec3 × ℝ)} (hW : MeasurableSet W) {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} {ε : ℝ} (hε : 0 < ε) (hf : MeasureTheory.LocallyIntegrable (W.indicator f) MeasureTheory.volume) (z v : Foundation.Parabolic.Vec3 × ℝ) : ∫ (y : Foundation.Parabolic.Vec3 × ℝ) in W, f y * (fderiv ℝ (vorticityBackTest ε hε z) y) v = -(fderiv ℝ (vorticityBackMollify W f ε hε) z) v

Pairing the zero extension with a first derivative of the backward test gives minus the corresponding derivative of the backward mollification.

theorem CKN.vorticityBackTest_pairing_fderiv_fderiv {W : Set (Foundation.Parabolic.Vec3 × ℝ)} (hW : MeasurableSet W) {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} {ε : ℝ} (hε : 0 < ε) (hf : MeasureTheory.LocallyIntegrable (W.indicator f) MeasureTheory.volume) (z v w : Foundation.Parabolic.Vec3 × ℝ) : ∫ (y : Foundation.Parabolic.Vec3 × ℝ) in W, f y * (fderiv ℝ (fun (q : Foundation.Parabolic.Vec3 × ℝ) => (fderiv ℝ (vorticityBackTest ε hε z) q) v) y) w = (fderiv ℝ (fun (y : Foundation.Parabolic.Vec3 × ℝ) => (fderiv ℝ (vorticityBackMollify W f ε hε) y) v) z) w

Pairing the zero extension with a second derivative of the backward test gives the corresponding second derivative of the backward mollification.

theorem CKN.vorticity_translate_tendsto {g : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) {h : ℕ → Foundation.Parabolic.Vec3 × ℝ} (hh : Filter.Tendsto h Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (z : Foundation.Parabolic.Vec3 × ℝ) => g (z - h n) - g z) 2 MeasureTheory.volume) Filter.atTop (nhds 0)

Translation is continuous in L².

theorem CKN.vorticityBackMollify_tendsto {W : Set (Foundation.Parabolic.Vec3 × ℝ)} {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : MeasureTheory.MemLp (W.indicator f) 2 MeasureTheory.volume) {ε : ℕ → ℝ} (hε : Filter.Tendsto ε Filter.atTop (nhds 0)) (hεpos : ∀ (n : ℕ), 0 < ε n) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (z : Foundation.Parabolic.Vec3 × ℝ) => vorticityBackMollify W f (ε n) ⋯ z - W.indicator f z) 2 MeasureTheory.volume) Filter.atTop (nhds 0)

Backward mollifications converge in L² to the zero extension.

theorem CKN.vorticityBackMollify_abs_le {W : Set (Foundation.Parabolic.Vec3 × ℝ)} {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} {ε : ℝ} (hε : 0 < ε) {M : ℝ} (hbound : ∀ᵐ (y : Foundation.Parabolic.Vec3 × ℝ), |W.indicator f y| ≤ M) (z : Foundation.Parabolic.Vec3 × ℝ) : |vorticityBackMollify W f ε hε z| ≤ M

Backward mollification preserves a pointwise bound of the zero extension.