Iterated spatial derivatives of the regularizing convolution

The coordinate derivatives in lem:reg-mollifier-bounds are evaluations of the iterated Fréchet derivative on tuples of coordinate vectors.

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

Scalar multiplication as a bilinear map on the real vector L² space.

Equations

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

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

The continuous bilinear scalar action on the real vector L² space.

Equations

• CKN.Leray.allDerivativeScalarVectorAction = CKN.Leray.allDerivativeScalarVectorActionLinear.mkContinuous₂ 1 CKN.Leray.allDerivativeScalarVectorAction._proof_1

theorem CKN.Leray.allDerivativeScalarVectorConvolution_hasFDerivAt (k : Foundation.Parabolic.L2Vec3 → ℝ) (hk : ContDiff ℝ 1 k) (hkc : HasCompactSupport k) {f : Foundation.Parabolic.L2Vec3 → Foundation.Parabolic.L2Vec3} (hf : MeasureTheory.LocallyIntegrable f MeasureTheory.volume) (x : Foundation.Parabolic.L2Vec3) : HasFDerivAt (MeasureTheory.convolution k f allDerivativeScalarVectorAction MeasureTheory.volume) (MeasureTheory.convolution (fderiv ℝ k) f (ContinuousLinearMap.precompL Foundation.Parabolic.L2Vec3 allDerivativeScalarVectorAction) MeasureTheory.volume x) x

A smooth compactly supported scalar kernel differentiates through vector convolution under local integrability.

theorem CKN.Leray.allDerivativeScalarVectorConvolution_directional_deriv (k : Foundation.Parabolic.L2Vec3 → ℝ) (hk : ContDiff ℝ 2 k) (hkc : HasCompactSupport k) {f : Foundation.Parabolic.L2Vec3 → Foundation.Parabolic.L2Vec3} (hf : MeasureTheory.LocallyIntegrable f MeasureTheory.volume) (x v : Foundation.Parabolic.L2Vec3) : (fderiv ℝ (MeasureTheory.convolution k f allDerivativeScalarVectorAction MeasureTheory.volume) x) v = ∫ (y : Foundation.Parabolic.L2Vec3), (fderiv ℝ k y) v • f (x - y)

The derivative of vector convolution is convolution with the directional derivative of the scalar kernel.

theorem CKN.Leray.regMollifierKernel_iteratedDerivative_eLpNorm_two (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (n : ℕ) (v : Fin n → Foundation.Parabolic.L2Vec3) : MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.L2Vec3) => (iteratedFDeriv ℝ n (regMollifierKernel ρ ε hε) y) v) 2 MeasureTheory.volume = ENNReal.ofReal (ε ^ (-(3 / 2) - ↑n)) * MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.L2Vec3) => (iteratedFDeriv ℝ n (⇑ρ.rho) y) v) 2 MeasureTheory.volume

The dilated kernel derivative in any ordered set of directions has the exact three-dimensional L² scaling for lem:reg-mollifier-bounds.