PDE

The Fréchet derivative x ↦ (∂ˢψ(x))(unitSeq s) of a test function ψ ∈ Cc^∞(U) again lies in Cc^∞(U). This is used to compose the weak derivative definition with itself.

Swap the second spatial derivative $\partial_{xx}$ with the integral $\int$. -/ lemma swap_xx_heatKernel {α : ℝ} {x t : ℝ} (g : ℝ → ℝ) (ht : 0 < t) (hα : 0 < α) (hg : Integrable g) : HasDerivAt (fun x' => ∫ y, HKx α (x' - y) t * g y ∂volume) (∫ y, HKxx α (x - y) t * g y ∂volume) x := by have mem_nhds : Metric.ball x 1 ∈ 𝓝 x := Metric.ball_mem_nhds x (by...

Derivative of the exponential term exp(-(x²)/(4αt)) with respect to x.

Derivative of 1/√x at a positive point.

Key Gaussian tail bound: This is the analytical estimate that allows us to bound Gaussian tail integrals and prove convergence as t → 0.

The time derivative of the heat kernel ∂/∂t heatKernel(α, x, t).