Change of variables for mollifier pairings

This module records the two reflection identities that move the mollifier weight off a function and onto the other factor of an integral. In the elliptic-regularity analysis of Caffarelli--Kohn--Nirenberg (1982), the convolution mollify u ε hε x is the pairing of u against the reflected kernel y ↦ mollifier ε hε (x - y); identifying the two presentations of this pairing, with u replaced by a weak partial derivative, is what lets a weak derivative be moved from the function onto the test kernel.

Integrating against the volume measure, the change of variables y ↦ x - y (the ε-ball reflection) converts the pairing into the convolution itself. The second identity combines this reflection with the already-proved integral form of the weak partial derivative, so that a smooth ψ may be differentiated inside the pairing.

theorem CKN.integral_mul_mollifier_sub {d : ℕ} (ψ : Vec d → ℝ) {ε : ℝ} (hε : 0 < ε) (x : Vec d) : ∫ (y : Vec d), ψ y * mollifier ε hε (x - y) = mollify ψ ε hε x

Integrating a function against the reflected mollifier reproduces its mollification: the convolution pairing mollify ψ ε hε x equals the integral of ψ y against mollifier ε hε (x - y) over the ambient volume measure. This is the change of variables y ↦ x - y for the (reflected) mollifier pairing of Caffarelli--Kohn--Nirenberg (1982).

theorem CKN.integral_mul_fderiv_mollifier_sub {d : ℕ} {ψ : Vec d → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (i : Fin d) {ε : ℝ} (hε : 0 < ε) (x : Vec d) : ∫ (y : Vec d), ψ y * (fderiv ℝ (mollifier ε hε) (x - y)) (basisVec i) = mollify (fun (z : Vec d) => (fderiv ℝ ψ z) (basisVec i)) ε hε x

Differentiating a smooth function inside the reflected mollifier pairing: for ContDiff ψ, the integral of ψ y against the ith partial derivative of the reflected kernel equals the mollification of the ith partial derivative of ψ. The change of variables y ↦ x - y reduces the claim to the integral form of the weak partial derivative of ψ on all of space (Caffarelli--Kohn--Nirenberg, 1982).