Lean 4 · 37 reusable claim declarations
Heat flow for rough initial data
Gaussian kernels and heat flow for positive and signed Gaussian-tempered measures, including data of infinite mass.
Mathematical interface
- One-dimensional Gaussian kernel: mass, semigroup, exact Lq norms, derivatives, L1 increments and a uniform quarter-Hölder Gaussian envelope.
- Gaussian-tempered positive measures: convergent heat flow, joint positive-time continuity and weighted bounds.
- Signed Jordan-pair data: total-variation domination, finite SignedMeasure interoperability and nontrivial examples.
- Chen–Dalang, squared-kernel, heat-flow semigroup and doubled-profile convolution estimates.
Find your way
Use the libraryPins, build and the public dependency.Find a theorem37 reusable claim declarations and source links.Read the boundaryVerified statement scope and what is not established.Inspect the trust modelKernel checks, domains, axioms and evidence.Work with an agentAuthority order, exact APIs and machine context.Credit the workCitation, provenance, license and acknowledgments.