RoughHeatKernel
Documentation · API · Verification
Verified revision 00b39962d332: the source adds deterministic causal heat-kernel L² continuity and weighted continuity, with 160 public theorems and 56 curated claims. A fresh native verification receipt binds source 00b39962d332; all 56 curated statements passed the official three-kernel comparison. The published release records below retain their original source scope.
The one-dimensional heat kernel and the heat flow of rough positive and signed measures, formalized in Lean 4.
This library treats measures with Gaussian-tempered total variation: they may have infinite total mass, but their integral against every decaying Gaussian is finite. Dirac masses, finite signed measures and Lebesgue measure are examples. The results are standard analysis; no new mathematics is claimed.
Historical source API 0.11.0 release. Version 0.11.0 adds elementary facts about erf, erfc and the standard normal distribution function (derivatives, parity, signs, limits, bounds, monotonicity), makes the shifted semigroup identity ∫ p_a(y − m) p_b(x − y) dy = p_{a+b}(x − m) and lheatFlow_sq_eq public, and adds the pointwise-in-time step of the Chen–Dalang estimate and the integrability-free bound ofReal (∫ f) ≤ ∫⁻ ofReal f for nonnegative f. Version 0.10.0 added RoughHeatKernel.Beta, RoughHeatKernel.Scaled and RoughHeatKernel.Erf. The source now has 142 public theorem/lemma declarations across 15 library modules and 51 curated reusable claims; every 0.10.0 statement, hypothesis and definition is unchanged. Scientific source 6a35f44f2d51 passed both verification tiers; receipts for 0.10.0 and earlier remain historical.
What is proved
| Area | Results |
|---|
| Gaussian heat kernel | Positivity, mass one, convolution semigroup, Gaussian-density bridge, exact Lq norms including the supremum norm |
| Rough positive data | Absolute convergence, joint positive-time continuity, Gaussian growth, Gaussian-weighted integrability and local small-time bounds |
| Signed data | Jordan-pair rough measures, domination by total variation, Dirac and genuinely signed examples, finite Mathlib SignedMeasure interoperability |
| Kernel regularity | First spatial and time derivatives, Gaussian moments, spatial and forward-time L1 increments, uniform quarter-Hölder Gaussian envelope |
| Convolution estimates | Chen–Dalang Gaussian quadratic bound, squared-kernel and arcsine identities, heat-flow semigroup, doubled-profile linear and quadratic bounds |
| Diffusion-scale kernel | Squared-kernel and semigroup identities for the kernel p_{νt} of ∂_t u = (ν/2) ∂_x² u |
| Special functions | Real Beta integral on [0, t], error function, standard normal density and distribution function, Φ(x) = (1 + erf(x/√2))/2, Gamma series for e^{z²}(1 + erf z) |
The API guide maps these results to modules. The declaration index lists every public theorem, and claims.yaml describes the curated reusable source claims; registry acceptance is separate.
Scope and assumptions
The kernel has variance t, so its heat equation has diffusion coefficient 1/2. Analytic statements assume positive time; at nonpositive times its definition has the junk value zero. Real-valued heat flows use Bochner integration and require the stated integrability hypotheses. Extended-real lower integrals are defined for arbitrary measures and may be infinite.
Heat-flow continuity is joint in time and space at every strictly positive time, for positive and signed Gaussian-tempered data. The quarter-Hölder kernel envelope has the universal constant 2 * exp(1), before all positive times and spatial points. Continuity at time zero, weak convergence to initial data, higher dimensions, higher derivatives, Fourier estimates and stochastic integration remain outside this release. The finite SignedMeasure bridge goes into RoughMeasure; there is no general converse API yet. No stochastic PDE well-posedness theorem is claimed.
Build and use
Install elan, then use the toolchain pinned in lean-toolchain: currently Lean v4.35.0, with Mathlib 56a005855ea17e0b0958f73ec801ae140b0a1679.
lake exe cache get
lake build
LIBRARY_AUDIT_DIR="$PWD/.lake/native-audit" bash verify.sh "$PWD/.lake/verify.log"
Use import RoughHeatKernel, or a narrower module such as import RoughHeatKernel.Increments. Examples cover finite, signed and infinite-mass data. The getting-started guide and dependency guide explain reproducibility and the public dependency interface.
Verification
Scientific source 6a35f44f2d51 passed the complete fresh local verifier and independent three-kernel comparison for all 51 curated claims. The verifier checked all 142 public propositions, compiled-environment ownership and axiom dependencies for 326 production/positive-test declarations in 33 modules and 297 proved-reference declarations in 16 modules, elaborated types, examples and eleven strict negative fixtures with separately compiled witnesses, with compiled escape controls and exact native module replay. The permitted axioms are Classical.choice, Quot.sound and propext. The trust guide explains each check. Receipts bind the scientific source, dependency pins and retained outputs; proof checking does not validate this prose or remove hypotheses from a theorem.
여기까지가 README 앞부분입니다. 나머지는 원문에서 읽을 수 있습니다. README 전문 보기 ↗
