Slice-wise spatial mollification of space-time fields

Mollifying every time slice in space along the radii 1 / (n + 1) converges in every space-time L^p, 1 ≤ p < ∞, on the slab. This removes the mollification in the cross-testing identity of lem:pv-serrin-uniqueness.

noncomputable def ESS.serrinRadius (n : ℕ) : ℝ

The mollification radii 1 / (n + 1).

Equations

• ESS.serrinRadius n = 1 / ↑(n + 1)

theorem ESS.serrinRadius_pos (n : ℕ) : 0 < serrinRadius n

theorem ESS.serrinRadius_tendsto : Filter.Tendsto serrinRadius Filter.atTop (nhds 0)

noncomputable def ESS.serrinKernel (n : ℕ) : CKN.Foundation.Parabolic.Vec3 → ℝ

The mollification kernel of radius 1 / (n + 1).

Equations

• ESS.serrinKernel n = CKN.mollifier (ESS.serrinRadius n) ⋯

theorem ESS.serrin_mollify_eq_integral (g : CKN.Foundation.Parabolic.Vec3 → ℝ) {ε : ℝ} (hε : 0 < ε) (y : CKN.Foundation.Parabolic.Vec3) : CKN.mollify g ε hε y = ∫ (x : CKN.Foundation.Parabolic.Vec3), g x * CKN.mollifier ε hε (y - x)

Mollification written as an integral against the translated kernel.

noncomputable def ESS.serrinSM (f : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (n : ℕ) : CKN.Foundation.Parabolic.ParabolicPoint → ℝ

Slice-wise spatial mollification of a scalar space-time field.

Equations

• ESS.serrinSM f n z = CKN.mollify (fun (x : CKN.Foundation.Parabolic.Vec3) => f (x, z.2)) (ESS.serrinRadius n) ⋯ z.1

theorem ESS.serrinSM_eq_integral (f : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (n : ℕ) (y : CKN.Foundation.Parabolic.Vec3) (τ : ℝ) : serrinSM f n (y, τ) = ∫ (x : CKN.Foundation.Parabolic.Vec3), f (x, τ) * serrinKernel n (y - x)

theorem ESS.serrinMol_kernel_eq (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (n : ℕ) (k : Fin 3) (y : CKN.Foundation.Parabolic.Vec3) (τ : ℝ) : serrinMol u (serrinKernel n) k y τ = serrinSM (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => u z k) n (y, τ)

The mollified component equals the slice-wise mollification of the component.

theorem ESS.serrinSM_aestronglyMeasurable {T : ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (n : ℕ) : MeasureTheory.AEStronglyMeasurable (serrinSM f n) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))

Slice-wise mollification preserves almost everywhere strong measurability on the slab.

theorem ESS.serrinSM_tendsto_prod {T : ℝ} {g : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {p : ENNReal} (hp : 1 ≤ p) (hptop : p ≠ ⊤) (hg : MeasureTheory.MemLp g p (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T)))) (hSM : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.mollify (fun (x : CKN.Foundation.Parabolic.Vec3) => g (x, z.2)) (serrinRadius n) ⋯ z.1) (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T)))) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.mollify (fun (x : CKN.Foundation.Parabolic.Vec3) => g (x, z.2)) (serrinRadius n) ⋯ z.1 - g z) p (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T)))) Filter.atTop (nhds 0)

Slice-wise spatial mollification converges in space-time L^p on the slab, product-coordinate form.

theorem ESS.serrin_slab_measure_eq (T : ℝ) : MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)) = MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T))

The parabolic slab measure is the product of Lebesgue measure in space with Lebesgue measure on the time interval.

theorem ESS.serrinSM_tendsto {T : ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {p : ENNReal} (hp : 1 ≤ p) (hptop : p ≠ ⊤) (hf : MeasureTheory.MemLp f p (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => serrinSM f n z - f z) p (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) Filter.atTop (nhds 0)

Slice-wise spatial mollification converges in space-time L^p on the slab.