Second-order transport identities for translated mollifier kernels

This module records the mixed-second-order analogues of the first-order mollifier transport identities of CKN.Foundation.Measure.SliceDistributionTransport. In the elliptic-regularity analysis of Caffarelli--Kohn--Nirenberg (1982), the pairing of a distribution with the countable family of translated mollifier bumps is integrated by parts; the first-order identities handle the divergence-form (first-derivative) slots, while the identities here handle the second-derivative slots of eq:leibniz-lap and eq:commute.

Concretely, we differentiate under the reflected convolution: the integral of a smooth ψ against the mixed second derivative ∂_i ∂_j of the reflected kernel mollifier ε (x - ·) equals the mollification of the corresponding mixed second derivative of ψ. The translation identities spatialDeriv_sub_const and mixedSecond_sub_const reduce the reflected derivative to the translate of the derivative, and the kernel vanishes outside its support ball.

theorem CKN.spatialDeriv_sub_const {g : Foundation.Parabolic.Vec3 → ℝ} (hg : Differentiable ℝ g) (y x : Foundation.Parabolic.Vec3) (i : Fin 3) : spatialDeriv (fun (z : Foundation.Parabolic.Vec3) => g (z - y)) i x = spatialDeriv g i (x - y)

Spatial derivative of a translate: ∂_i (z ↦ g (z - y)) (x) = ∂_i g (x - y). This is the chain rule for the translation z ↦ z - y, used to move the derivative of a reflected mollifier kernel back onto the kernel.

theorem CKN.mixedSecond_sub_const {g : Foundation.Parabolic.Vec3 → ℝ} (hg : ContDiff ℝ (↑⊤) g) (y x : Foundation.Parabolic.Vec3) (i j : Fin 3) : mixedSecond (fun (z : Foundation.Parabolic.Vec3) => g (z - y)) i j x = mixedSecond g i j (x - y)

Mixed second derivative of a translate: ∂_i ∂_j (z ↦ g (z - y)) (x) = ∂_i ∂_j g (x - y). This iterates the translation chain rule spatialDeriv_sub_const on the smooth function g.

theorem CKN.integral_mul_spatialDeriv_sub {ψ g : Foundation.Parabolic.Vec3 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) (i : Fin 3) (x : Foundation.Parabolic.Vec3) : ∫ (y : Foundation.Parabolic.Vec3), ψ y * spatialDeriv g i (x - y) = ∫ (y : Foundation.Parabolic.Vec3), spatialDeriv ψ i y * g (x - y)

Integration by parts against a translated derivative: for smooth ψ and smooth compactly supported g, the pairing of ψ with the reflected ith partial derivative of g equals the pairing of the ith partial derivative of ψ with the reflected g. This is the weak partial-derivative identity for ψ tested against the smooth compactly supported translate w ↦ g (x - w).

theorem CKN.continuous_mixedSecond_mollifier {ε : ℝ} (hε : 0 < ε) (i j : Fin 3) : Continuous (mixedSecond (mollifier ε hε) i j)

The mixed second derivative of the radius-ε mollifier is continuous; it is a second partial derivative of a smooth compactly supported kernel.

theorem CKN.mixedSecond_mollifier_eq_zero {ε : ℝ} (hε : 0 < ε) (i j : Fin 3) {z : Foundation.Parabolic.Vec3} (hz : ε < ‖z‖) : mixedSecond (mollifier ε hε) i j z = 0

The mixed second derivative of the mollifier vanishes outside the support ball: for ε < ‖z‖, ∂_i ∂_j mollifier ε z = 0. This is because the topological support of a coordinate derivative is contained in that of the kernel, which is the closed ball of radius ε.

theorem CKN.integral_mul_mixedSecond_mollifier_sub {ψ : Foundation.Parabolic.Vec3 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (i j : Fin 3) {ε : ℝ} (hε : 0 < ε) (x : Foundation.Parabolic.Vec3) : ∫ (y : Foundation.Parabolic.Vec3), ψ y * mixedSecond (mollifier ε hε) i j (x - y) = mollify (mixedSecond ψ i j) ε hε x

Integration by parts against the reflected mixed second derivative of the mollifier: for smooth ψ, the pairing of ψ with ∂_i ∂_j mollifier ε (x - ·) equals the mollification of the mixed second derivative ∂_i ∂_j ψ. This is the second-order analogue of the first-order identity integral_mul_fderiv_mollifier_sub, obtained by applying integral_mul_spatialDeriv_sub twice and using symmetry of the mixed partials.