Documentation

LeanPool.CaffarelliKohnNirenberg.Foundation.Heat.CausalDistribution

The causal heat kernel as a distribution #

External Input ext:heat-kernel of paper/ckn.tex states that W₊(t,x) = 1_{t>0}(4πt)^{-3/2}e^{-|x|²/(4t)} is locally integrable on ℝ³ × ℝ, is supported in {t ≥ 0}, and satisfies (∂_t - Δ)W₊ = δ_{(0,0)} in 𝒟'(ℝ³ × ℝ). Writing that identity requires a distribution carrier for W₊. This file supplies it: the established local integrability of heatKernelPlus, stated for the ordinary product topology on Vec3 × ℝ rather than the parabolic one, the induced distribution, its action on every test function, and its causal support.

The fundamental-solution identity itself is the content of the external input and is not proved here.

source
theorem CKN.Foundation.Heat.heatKernelPlus_locallyIntegrable_prod_volume :
MeasureTheory.LocallyIntegrable (fun (z : Parabolic.Vec3 × ℝ) => heatKernelPlus z) MeasureTheory.volume

heatKernelPlus is locally integrable for the ordinary product topology on Vec3 × ℝ. The established statement is for the parabolic topology on ParabolicPoint; the two topologies agree, and a distribution on Vec3 × ℝ needs the product form.

source
noncomputable def CKN.Foundation.Heat.heatKernelPlusDistribution :
Distribution ⊤ ℝ ⊤

The causal heat kernel W₊ of External Input ext:heat-kernel, read as a distribution on all of ℝ³ × ℝ.

Equations
Instances For
    source
    theorem CKN.Foundation.Heat.heatKernelPlusDistribution_apply (ψ : TestFunction ⊤ ℝ ⊤) :
    heatKernelPlusDistribution ψ = ∫ (z : Parabolic.Vec3 × ℝ), ψ z • heatKernelPlus z

    The distribution of W₊ acts on every test function by integration against W₊; in particular it is not the zero map of the non-integrable branch.

    source
    theorem CKN.Foundation.Heat.heatKernelPlusDistribution_dsupport_subset :
    Distribution.dsupport ⇑heatKernelPlusDistribution ⊆ {z : Parabolic.Vec3 × ℝ | 0 ≤ z.2}

    The distributional support of W₊ lies in the closed half space {t ≥ 0}, the causality clause of External Input ext:heat-kernel.