RoughHeatKernel v0.11.0

RoughHeatKernel v0.11.0 adds general-purpose lemmas extracted from a Lean verification of Chen–Dalang (Ann. Probab. 2015), where three independent proof efforts each needed them.

• RoughHeatKernel.Erf: the derivative erf' x = (2/√π) e^{-x²} (and erfc' = -erf'), continuity, erf 0 = 0, erfc 0 = 1, oddness, signs, and the limits erf → ±1 at ±∞ and erfc → 0 at +∞; the standard normal density is nonnegative with total mass one; normalCDF takes values in [0, 1], is monotone, and is at least 1/2 on [0, ∞).
• RoughHeatKernel.ChenDalang: the shifted semigroup identity ∫ p_a(y − m) p_b(x − y) dy = p_{a+b}(x − m) and its integrability, and lheatFlow_sq_eq, all previously module-private and now public; the pointwise-in-time step of the Chen–Dalang estimate, ∫ J(r,y)² p_{(R−r)/2}(x − y) dy ≤ 2√(R/r) J(2R,x)² for 0 < r < R (J = lheatFlow ν); and ENNReal.ofReal (∫ f dμ) ≤ ∫⁻ ENNReal.ofReal f dμ for nonnegative f, with no integrability hypothesis.

Every v0.10.0 statement, hypothesis and definition is unchanged: the raw types of all 172 v0.10.0 public constants are byte-identical, and 24 constants are new (22 theorems, three of them previously module-private, and the generated equation lemmas erf.eq_1, erfc.eq_1).

Scientific source 6a35f44f2d51 passed the complete fresh verifier: the 142-proposition inventory, all-owned declaration/axiom audits (326 production/positive-test declarations in 33 modules, 297 reference declarations in 16 modules), eleven strict negative/witness pairs, compiled escape controls and exact native module replay. The Lean toolchain comparator (lake comparator, con-ron kernel replay) accepted all 51 curated claims. Permitted axioms are Classical.choice, Quot.sound and propext.

Pinned Lean: leanprover/lean4:v4.35.0. Mathlib: 56a005855ea17e0b0958f73ec801ae140b0a1679. License: Apache-2.0.

No new research result or Palomar submission readiness is claimed; these are standard facts.

Documentation · Source and verification record