Space-time mollification on ℝ³ × ℝ

A normalized smooth bump kernel on Vec3 × ℝ, convolution with it, and its basic properties: smoothness of the mollified function, control of its support, the L² contraction bound, and L² convergence as the radius tends to zero. These are used to extend the Carleman inequalities from smooth compactly supported fields to Sobolev fields (lem:carleman-sobolev of the Escauriaza–Seregin–Šverák manuscript).

theorem CKN.spaceTimeVolumeIsAddHaarMeasure : MeasureTheory.volume.IsAddHaarMeasure

theorem CKN.spaceTimeVolumeIsAddLeftInvariant : MeasureTheory.volume.IsAddLeftInvariant

theorem CKN.spaceTimeVolumeIsAddRightInvariant : MeasureTheory.volume.IsAddRightInvariant

noncomputable def CKN.spaceTimeStandardBump (δ : ℝ) (hδ : 0 < δ) : ContDiffBump 0

The normalized bump of radius δ on space-time.

Equations

• CKN.spaceTimeStandardBump δ hδ = { rIn := δ / 2, rOut := δ, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }

noncomputable def CKN.spaceTimeMollifier (δ : ℝ) (hδ : 0 < δ) : Foundation.Parabolic.Vec3 × ℝ → ℝ

The nonnegative normalized space-time kernel with outer radius δ.

Equations

• CKN.spaceTimeMollifier δ hδ = (CKN.spaceTimeStandardBump δ hδ).normed MeasureTheory.volume

noncomputable def CKN.spaceTimeMollify (f : Foundation.Parabolic.Vec3 × ℝ → ℝ) (δ : ℝ) (hδ : 0 < δ) : Foundation.Parabolic.Vec3 × ℝ → ℝ

Convolution with the normalized space-time kernel of radius δ.

Equations

• CKN.spaceTimeMollify f δ hδ = MeasureTheory.convolution (CKN.spaceTimeMollifier δ hδ) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume

theorem CKN.spaceTimeMollifier_nonneg {δ : ℝ} (hδ : 0 < δ) (z : Foundation.Parabolic.Vec3 × ℝ) : 0 ≤ spaceTimeMollifier δ hδ z

The space-time kernel is pointwise nonnegative.

theorem CKN.spaceTimeMollifier_integral_one {δ : ℝ} (hδ : 0 < δ) : ∫ (z : Foundation.Parabolic.Vec3 × ℝ), spaceTimeMollifier δ hδ z = 1

The space-time kernel has integral one.

theorem CKN.spaceTimeMollifier_hasCompactSupport {δ : ℝ} (hδ : 0 < δ) : HasCompactSupport (spaceTimeMollifier δ hδ)

The space-time kernel has compact support.

theorem CKN.spaceTimeMollifier_support {δ : ℝ} (hδ : 0 < δ) : Function.support (spaceTimeMollifier δ hδ) = Metric.ball 0 δ

The support of the kernel lies in the open ball of radius δ.

theorem CKN.spaceTimeMollifier_contDiff {δ : ℝ} (hδ : 0 < δ) {n : ℕ∞} : ContDiff ℝ (↑n) (spaceTimeMollifier δ hδ)

The space-time kernel is smooth to every finite or infinite order.

theorem CKN.spaceTimeMollify_contDiff {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} {δ : ℝ} (hδ : 0 < δ) {n : ℕ∞} (hf : MeasureTheory.LocallyIntegrable f MeasureTheory.volume) : ContDiff ℝ (↑n) (spaceTimeMollify f δ hδ)

Convolution with the space-time kernel is smooth for locally integrable data.

theorem CKN.spaceTimeMollify_hasCompactSupport {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} {δ : ℝ} (hδ : 0 < δ) (hf : HasCompactSupport f) : HasCompactSupport (spaceTimeMollify f δ hδ)

Convolution with the space-time kernel preserves compact support.

theorem CKN.spaceTimeMollify_support_subset {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} {δ : ℝ} (hδ : 0 < δ) : Function.support (spaceTimeMollify f δ hδ) ⊆ Metric.ball 0 δ + Function.support f

The support after mollification lies within distance δ of the original support.

noncomputable def CKN.spaceTimeMollifyPi {ι : Type u_1} (f : Foundation.Parabolic.Vec3 × ℝ → ι → ℝ) (δ : ℝ) (hδ : 0 < δ) : Foundation.Parabolic.Vec3 × ℝ → ι → ℝ

Componentwise mollification of fields with scalar components. This includes Vec3 values and fields with values Fin 3 → Vec3.

Equations

• CKN.spaceTimeMollifyPi f δ hδ x i = CKN.spaceTimeMollify (fun (y : CKN.Foundation.Parabolic.Vec3 × ℝ) => f y i) δ hδ x

theorem CKN.spaceTimeMollifyPi_contDiff {ι : Type u_1} [Fintype ι] {f : Foundation.Parabolic.Vec3 × ℝ → ι → ℝ} {δ : ℝ} (hδ : 0 < δ) {n : ℕ∞} (hf : ∀ (i : ι), MeasureTheory.LocallyIntegrable (fun (y : Foundation.Parabolic.Vec3 × ℝ) => f y i) MeasureTheory.volume) : ContDiff ℝ (↑n) (spaceTimeMollifyPi f δ hδ)

Componentwise mollification preserves smoothness.

theorem CKN.spaceTimeMollifyPi_support_subset {ι : Type u_1} {f : Foundation.Parabolic.Vec3 × ℝ → ι → ℝ} {δ : ℝ} (hδ : 0 < δ) : Function.support (spaceTimeMollifyPi f δ hδ) ⊆ Metric.ball 0 δ + Function.support f

The support of a componentwise mollification lies within distance δ of the field support.

theorem CKN.spaceTimeMollifyPi_hasCompactSupport {ι : Type u_1} {f : Foundation.Parabolic.Vec3 × ℝ → ι → ℝ} {δ : ℝ} (hδ : 0 < δ) (hf : HasCompactSupport f) : HasCompactSupport (spaceTimeMollifyPi f δ hδ)

Componentwise mollification has compact support when the input field does.

theorem CKN.spaceTimeVolumeIsAddHaarMeasure' : MeasureTheory.volume.IsAddHaarMeasure

theorem CKN.spaceTimeVolumeIsAddLeftInvariant' : MeasureTheory.volume.IsAddLeftInvariant

theorem CKN.spaceTimeMollify_eLpNorm_le {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} {δ : ℝ} (hδ : 0 < δ) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) : MeasureTheory.eLpNorm (spaceTimeMollify f δ hδ) 2 MeasureTheory.volume ≤ MeasureTheory.eLpNorm f 2 MeasureTheory.volume

Convolution by the space-time kernel is a contraction on L².

theorem CKN.tendsto_eLpNorm_sub_zero_spaceTimeMollify {g : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) {ε : ℕ → ℝ} (hε : Filter.Tendsto ε Filter.atTop (nhds 0)) (hε_pos : ∀ (n : ℕ), 0 < ε n) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3 × ℝ) => spaceTimeMollify g (ε n) ⋯ x - g x) 2 MeasureTheory.volume) Filter.atTop (nhds 0)

Mollification converges in L² for every square-integrable space-time function.