Documentation

LeanPool.CaffarelliKohnNirenberg.Leray.RegularisedBesselLaplacian

The second-order Bessel operator and the Laplacian #

At integer order two, the Bessel Fourier symbol is the sum of the identity and the quadratic frequency symbol. This identifies the complete Sobolev weight with physical second derivatives.

source
theorem CKN.Leray.regularised_besselPotential_two_eq_add_frequencySq (D : TemperedDistribution Foundation.Parabolic.L2Vec3 ComplexVec3) :
(TemperedDistribution.besselPotential Foundation.Parabolic.L2Vec3 ComplexVec3 2) D = D + (TemperedDistribution.fourierMultiplierCLM ComplexVec3 fun (ξ : Foundation.Parabolic.L2Vec3) => ↑(‖ξ‖ ^ 2)) D

The Bessel potential of order two is the identity plus the quadratic frequency multiplier on tempered distributions.

source
theorem CKN.Leray.regularised_besselPotential_two_laplacian_identity (D : TemperedDistribution Foundation.Parabolic.L2Vec3 ComplexVec3) :
(2 * Real.pi) ^ 2 • (TemperedDistribution.besselPotential Foundation.Parabolic.L2Vec3 ComplexVec3 2) D = (2 * Real.pi) ^ 2 • D - Laplacian.laplacian D

The second-order Bessel operator is the scaled identity minus the distributional Laplacian.