Uniform bound

noncomputable def CIV.mollifySlice (m : ℕ) (ε : ℝ) (q : CKN.Vec m × ℝ → ℝ) (z : CKN.Vec m × ℝ) : ℝ

The spatial mollification of a time-dependent function, at a fixed time slice.

mollifySlice m ε q (x, τ) = ∫_y η_ε(x - y) q(y, τ) dy where η_ε is the rescaled mollifier kernel of radius ε.

Equations

• CIV.mollifySlice m ε q z = ∫ (y : CKN.Vec m), CIV.mollifierKernel m ε (z.1 - y) * q (y, z.2)

theorem CIV.abs_mollifySlice_le {m : ℕ} {ε : ℝ} (hε : 0 < ε) {τ : ℝ} {q : CKN.Vec m × ℝ → ℝ} {M : ℝ} (h_meas : MeasureTheory.AEStronglyMeasurable (fun (y : CKN.Vec m) => q (y, τ)) MeasureTheory.volume) (h_bdd : ∀ᵐ (y : CKN.Vec m), |q (y, τ)| ≤ M) (x : CKN.Vec m) : |mollifySlice m ε q (x, τ)| ≤ M

Bridge to the convolution API

theorem CIV.mollifySlice_eq_convolution {m : ℕ} (ε τ : ℝ) (q : CKN.Vec m × ℝ → ℝ) (x : CKN.Vec m) : mollifySlice m ε q (x, τ) = MeasureTheory.convolution (fun (y : CKN.Vec m) => q (y, τ)) (mollifierKernel m ε) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x

The mollified slice equals the convolution of the time-slice with the kernel. The kernel sits in the right slot because ∫ η_ε(x - y) q(y, τ) dy has the kernel evaluated at x - y.

Local integrability of bounded a.e.-measurable functions

theorem CIV.locallyIntegrable_of_bounded {m : ℕ} {f : CKN.Vec m → ℝ} {M : ℝ} (hf_meas : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) (hf_bdd : ∀ᵐ (y : CKN.Vec m), |f y| ≤ M) : MeasureTheory.LocallyIntegrable f MeasureTheory.volume

A bounded a.e.-measurable function on Vec m is locally integrable.

Smoothness in the spatial variable

theorem CIV.contDiff_mollifySlice {m : ℕ} {ε : ℝ} (hε : 0 < ε) (τ : ℝ) (q : CKN.Vec m × ℝ → ℝ) (M : ℝ) (h_meas : MeasureTheory.AEStronglyMeasurable (fun (y : CKN.Vec m) => q (y, τ)) MeasureTheory.volume) (h_bdd : ∀ᵐ (y : CKN.Vec m), |q (y, τ)| ≤ M) : ContDiff ℝ ↑⊤ fun (x : CKN.Vec m) => mollifySlice m ε q (x, τ)

Derivative formula

theorem CIV.fderiv_mollifySlice {m : ℕ} {ε : ℝ} (hε : 0 < ε) (τ : ℝ) (q : CKN.Vec m × ℝ → ℝ) (M : ℝ) (h_meas : MeasureTheory.AEStronglyMeasurable (fun (y : CKN.Vec m) => q (y, τ)) MeasureTheory.volume) (h_bdd : ∀ᵐ (y : CKN.Vec m), |q (y, τ)| ≤ M) (x v : CKN.Vec m) : (fderiv ℝ (fun (x' : CKN.Vec m) => mollifySlice m ε q (x', τ)) x) v = ∫ (y : CKN.Vec m), (fderiv ℝ (mollifierKernel m ε) (x - y)) v * q (y, τ)