A fixed radial regularizing kernel

The profile and its dilates used by eq:reg-mollifier on the Euclidean three dimensional L² carrier.

structure CKN.Leray.RegMollifierProfile : Type

Smooth compactly supported radial data for the kernel in lem:reg-mollifier-bounds.

• rho : SchwartzMap Foundation.Parabolic.L2Vec3 ℝ

  The fixed real scalar kernel.

• smooth : ContDiff ℝ ↑⊤ ⇑self.rho

  The kernel is smooth.

• compact : HasCompactSupport ⇑self.rho

  The kernel has compact support.

• support_unit : tsupport ⇑self.rho ⊆ Metric.ball 0 1

  The support is contained in the unit ball.

• radial (x y : Foundation.Parabolic.L2Vec3) : ‖x‖ = ‖y‖ → self.rho x = self.rho y

  Radiality of the profile.

• nonneg (x : Foundation.Parabolic.L2Vec3) : 0 ≤ self.rho x

  The profile is nonnegative.

• integral_eq_one : ∫ (x : Foundation.Parabolic.L2Vec3), self.rho x = 1

  The profile has total mass one.

noncomputable def CKN.Leray.regMollifierKernel (ρ : RegMollifierProfile) (ε : ℝ) (_hε : 0 < ε) (x : Foundation.Parabolic.L2Vec3) : ℝ

The normalized spatial dilate of the fixed profile.

Equations

• CKN.Leray.regMollifierKernel ρ ε _hε x = (ε ^ 3)⁻¹ * ρ.rho (ε⁻¹ • x)

theorem CKN.Leray.regMollifierKernel_radial (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {x y : Foundation.Parabolic.L2Vec3} (hxy : ‖x‖ = ‖y‖) : regMollifierKernel ρ ε hε x = regMollifierKernel ρ ε hε y

The dilated profile remains radial.

theorem CKN.Leray.regMollifierKernel_nonneg (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (x : Foundation.Parabolic.L2Vec3) : 0 ≤ regMollifierKernel ρ ε hε x

The dilated profile is nonnegative.

theorem CKN.Leray.regMollifierKernel_integral_eq_one (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) : ∫ (x : Foundation.Parabolic.L2Vec3), regMollifierKernel ρ ε hε x = 1

The normalized dilate has total mass one.

theorem CKN.Leray.regMollifierKernel_memLp_two (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) : MeasureTheory.MemLp (regMollifierKernel ρ ε hε) 2 MeasureTheory.volume

Every dilated profile belongs to L²; this supplies the convolution kernel in the pointwise estimate of lem:reg-mollifier-bounds.

theorem CKN.Leray.regMollifierKernel_integrable (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) : MeasureTheory.Integrable (regMollifierKernel ρ ε hε) MeasureTheory.volume

The dilated kernel is integrable, as required for probability averaging in lem:reg-mollifier-bounds.

theorem CKN.Leray.regMollifierKernel_eLpNorm_two (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) : MeasureTheory.eLpNorm (regMollifierKernel ρ ε hε) 2 MeasureTheory.volume = ENNReal.ofReal (ε ^ (-(3 / 2))) * MeasureTheory.eLpNorm (⇑ρ.rho) 2 MeasureTheory.volume

The normalized spatial dilate has the expected three dimensional L² scaling, used in the derivative bounds of lem:reg-mollifier-bounds.

def CKN.Leray.scalarVectorActionLinear : ℝ →ₗ[ℝ] Foundation.Parabolic.L2Vec3 →ₗ[ℝ] Foundation.Parabolic.L2Vec3

Componentwise convolution by the dilated radial profile.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CKN.Leray.scalarVectorAction : ℝ →L[ℝ] Foundation.Parabolic.L2Vec3 →L[ℝ] Foundation.Parabolic.L2Vec3

The continuous scalar multiplication map on Hilbert vectors used by convolution.

Equations

• CKN.Leray.scalarVectorAction = CKN.Leray.scalarVectorActionLinear.mkContinuous₂ 1 CKN.Leray.scalarVectorAction._proof_1

noncomputable def CKN.Leray.regMollifyVector (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (f : Foundation.Parabolic.L2Vec3 → Foundation.Parabolic.L2Vec3) : Foundation.Parabolic.L2Vec3 → Foundation.Parabolic.L2Vec3

Componentwise convolution by the dilated radial profile.

Equations

• CKN.Leray.regMollifyVector ρ ε hε f = MeasureTheory.convolution (CKN.Leray.regMollifierKernel ρ ε hε) f CKN.Leray.scalarVectorAction MeasureTheory.volume

theorem CKN.Leray.regMollifyVector_pointwise_enorm_le (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {f : Foundation.Parabolic.L2Vec3 → Foundation.Parabolic.L2Vec3} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (x : Foundation.Parabolic.L2Vec3) : ‖regMollifyVector ρ ε hε f x‖ₑ ≤ MeasureTheory.eLpNorm (regMollifierKernel ρ ε hε) 2 MeasureTheory.volume * MeasureTheory.eLpNorm f 2 MeasureTheory.volume

The L² × L² → L∞ estimate for the pointwise vector convolution by the fixed regularizing kernel.

theorem CKN.Leray.regMollifyVector_pointwise_enorm_le_scaled (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {f : Foundation.Parabolic.L2Vec3 → Foundation.Parabolic.L2Vec3} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (x : Foundation.Parabolic.L2Vec3) : ‖regMollifyVector ρ ε hε f x‖ₑ ≤ ENNReal.ofReal (ε ^ (-(3 / 2))) * MeasureTheory.eLpNorm (⇑ρ.rho) 2 MeasureTheory.volume * MeasureTheory.eLpNorm f 2 MeasureTheory.volume

The pointwise estimate with the scale factor displayed in lem:reg-mollifier-bounds.

theorem CKN.Leray.regMollifyVector_aestronglyMeasurable (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {f : Foundation.Parabolic.L2Vec3 → Foundation.Parabolic.L2Vec3} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) : MeasureTheory.AEStronglyMeasurable (regMollifyVector ρ ε hε f) MeasureTheory.volume

The convolution by a dilated profile is measurable for every L² representative.

theorem CKN.Leray.regMollifyVector_eLpNorm_top_le (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {f : Foundation.Parabolic.L2Vec3 → Foundation.Parabolic.L2Vec3} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) : MeasureTheory.eLpNorm (regMollifyVector ρ ε hε f) ⊤ MeasureTheory.volume ≤ ENNReal.ofReal (ε ^ (-(3 / 2))) * MeasureTheory.eLpNorm (⇑ρ.rho) 2 MeasureTheory.volume * MeasureTheory.eLpNorm f 2 MeasureTheory.volume

The order-zero L² to L∞ estimate for arbitrary profiles in lem:reg-mollifier-bounds.