Documentation

LeanPool.CaffarelliKohnNirenberg.Foundation.Harmonic.NewtonianRepresentation

Newtonian Representation #

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

The Newtonian kernel representation obtained from the heat semigroup.

source
noncomputable def CKN.Foundation.Heat.newtonianKernel (z : Parabolic.Vec3) :
ℝ

The positive three-dimensional Newtonian kernel.

Equations
Instances For
    source
    theorem CKN.Foundation.Heat.newtonianKernel_locallyIntegrable :
    MeasureTheory.LocallyIntegrable newtonianKernel MeasureTheory.volume
    source
    theorem CKN.Foundation.Heat.newtonian_representation_smooth {u : Parabolic.Vec3 → ℝ} (hu : ContDiff ℝ (↑⊤) u) (huSupport : HasCompactSupport u) (x : Parabolic.Vec3) :
    u x = -∫ (y : Parabolic.Vec3), newtonianKernel (x - y) * spatialLaplacian u y

    For a compactly supported smooth function, the heat representation gives the Newtonian potential of its Laplacian, with the displayed sign convention.