RoughHeatKernel.heatKernel_convolution_heatKernel
Semigroup identity p_t * p_s = p_{t+s} for the 1-d heat kernel, as functions via Mathlib's convolution, for s,t > 0.
Reusable declaration index
Analytic estimates state positive-time hypotheses. heatKernel has value zero at nonpositive time. heatFlow is a real Bochner integral; rough-data theorems prove the required integrability. lheatFlow is an extended-real lower integral and may be infinite. Signed data are represented by mutually singular Gaussian-tempered Jordan parts, with no finite-total-mass assumption unless explicitly stated.
Each entry links to the scientific source copied from the explicit generation input. These 37 entries match the source claims ledger; this does not claim every public helper is a separate reusable claim.
RoughHeatKernel.eLpNorm_heatKernel
Exact L^q norm of the heat kernel for every q in [1, infinity]: C_q t^{-(1-1/q)/2} with an explicit constant.
RoughHeatKernel.continuous_heatFlow
For a Gaussian-tempered positive measure (possibly of infinite mass) and t > 0, the heat flow x -> int p_t(x-y) nu(dy) is continuous.
RoughHeatKernel.integrable_exp_mul_heatFlow_rpow
Weighted bound for the heat flow of a Gaussian-tempered measure: e^{-a x^2} (heat flow)^p is integrable for a, t > 0, p >= 1.
RoughHeatKernel.exists_sqrt_mul_heatFlow_le
Local small-time bound: sqrt(s) times the heat flow of a Gaussian-tempered measure is bounded uniformly on s in (0,T], |y| <= R.
RoughHeatKernel.ofReal_heatFlow
For a Gaussian-tempered measure and t > 0, the extended-real heat flow lheatFlow equals ofReal of the real heat flow (and is finite).
RoughHeatKernel.RoughMeasure.abs_heatFlow_le
For a signed measure with Gaussian-tempered total variation (Jordan pair), |heat flow of mu| <= heat flow of |mu|.
RoughHeatKernel.RoughMeasure.abs_heatFlow_le_of_isFiniteMeasure
For a finite signed measure, |heat flow| <= (2 pi t)^{-1/2} |mu|(R) at every point.
RoughHeatKernel.heatKernel_eq_gaussianPDFReal
The heat kernel is Mathlib's centred Gaussian density: heatKernel t = gaussianPDFReal 0 t.toNNReal for every real t.
RoughHeatKernel.integral_gaussianReal_eq_integral_heatKernel
Integration against the normal law gaussianReal x t equals integration against heatKernel t (x - y), for t != 0.
RoughHeatKernel.RoughMeasure.toSignedMeasure_ofSignedMeasure
A Mathlib SignedMeasure on R becomes a RoughMeasure via its Jordan decomposition; positive minus negative part recovers s, and the total variation is s.totalVariation.
RoughHeatKernel.lheatFlow_eq_ofReal_mul_lintegral
For every measure and every real t, the extended-real heat flow equals ofReal((2 pi t)^{-1/2}) times the lower integral of exp(-(x-y)^2/(2t)).
RoughHeatKernel.RoughMeasure.totalVariation_ofTempered
A Jordan pair whose total variation pos + neg is Gaussian-tempered is a RoughMeasure (single-condition form of the class), with that total variation.
RoughHeatKernel.integral_abs_heatKernel_sub_sub_le
Spatial L^1 increment of the 1-d heat kernel: int |p_t(x-y) - p_t(z-y)| dy <= min(2, |x-z|/sqrt t) for t > 0.
RoughHeatKernel.integral_abs_heatKernel_add_sub_le
Time L^1 increment of the 1-d heat kernel: int |p_{t+e}(x-y) - p_t(x-y)| dy <= min(2, e/t) for t > 0, e >= 0.
RoughHeatKernel.hasDerivAt_heatKernel_time
Time derivative of the heat kernel: d/dt p_t(x) = (x^2 - t)/(2 t^2) p_t(x) for t > 0 (the spatial one, -(x/t) p_t(x), is hasDerivAt_heatKernel).
RoughHeatKernel.lintegral_enorm_sub_le_lintegral
L^1 mean-value inequality: if F has derivative F' in theta on [a,b], F' is continuous in theta for each y and jointly measurable, then int |F(b,y)-F(a,y)| dy <= int_a^b int |F'(theta,y)| dy dtheta (lower integrals).
RoughHeatKernel.integral_sq_mul_heatKernel
Gaussian moments of the heat kernel: int x^2 p_t(x) dx = t, and int |x| p_t(x) dx <= sqrt t (integral_abs_mul_heatKernel_le), for t > 0.
RoughHeatKernel.lintegral_sq_lheatFlow_conv_le
Chen-Dalang estimate (Gaussian case): for s-finite nu, t > 0, measurable h >= 0, int_0^t int J(s,y)^2 p_{(t-s)/2}(x-y) h(t-s) dy ds <= 2 sqrt t J(2t,x)^2 int_0^t h(t-s)/sqrt s ds, J = lheatFlow nu (lower integrals).
RoughHeatKernel.heatKernel_mul_heatKernel_eq
Gaussian product identity: p_t(y-z1) p_t(y-z2) = p_{2t}(z1-z2) p_{t/2}(y-(z1+z2)/2) for t > 0.
RoughHeatKernel.heatKernel_le_sqrt_div_mul
Heat-kernel comparison across times: p_a(x) <= sqrt(b/a) p_b(x) for 0 < a <= b.
RoughHeatKernel.IsGaussianTempered.isLocallyFiniteMeasure
A Gaussian-tempered measure on R is locally finite (finite on bounded sets), hence sigma-finite.
RoughHeatKernel.lintegral_sq_lheatFlow_mul_heatKernel_sq_le
White-noise Chen-Dalang bound: for s-finite nu and t > 0, int_0^t int J(s,y)^2 p_{t-s}(x-y)^2 dy ds <= sqrt(pi) sqrt(t) J(2t,x)^2 with J = lheatFlow nu, as lower integrals.
RoughHeatKernel.heatKernel_sq_eq
Squared heat kernel: p_r(z)^2 = p_{r/2}(z) (4 pi r)^{-1/2} for r > 0; hence int p_r^2 = (4 pi r)^{-1/2} (integral_heatKernel_sq).
RoughHeatKernel.lintegral_arcsine
The arcsine integral: int_0^t ds / sqrt(s (t - s)) = pi for t > 0, as a lower Lebesgue integral.
RoughHeatKernel.lintegral_heatKernel_mul_lheatFlow
Heat-flow semigroup: for s-finite nu and 0 < s < t, int p_{t-s}(x-y) J(s,y) dy = J(t,x) with J = lheatFlow nu, as a lower integral.
RoughHeatKernel.lintegral_lintegral_heatKernel_mul_lheatFlow
Time-integrated heat-flow semigroup: for s-finite nu, int_0^t int p_{t-s}(x-y) J(s,y) dy ds = t J(t,x) with J = lheatFlow nu, as lower integrals.
RoughHeatKernel.heatKernel_add_le_sqrt_two_mul
For t > 0 and 0 <= s <= t, p_(t+s)(x) <= sqrt(2) p_(2t)(x).
RoughHeatKernel.lheatFlow_add_le_sqrt_two_mul
For every positive measure nu, t > 0 and 0 <= s <= t, J(t+s,x) <= sqrt(2) J(2t,x), with J = lheatFlow nu.
RoughHeatKernel.lintegral_heatKernel_mul_lheatFlow_two_mul
For every s-finite nu and 0 < s < t, the lower integral of p_(t-s)(x-y) J(2s,y) equals J(t+s,x).
RoughHeatKernel.lintegral_heatKernel_mul_lheatFlow_two_mul_le
For every s-finite nu and 0 < s < t, the lower integral of p_(t-s)(x-y) J(2s,y) is at most sqrt(2) J(2t,x).
RoughHeatKernel.lintegral_heatKernel_two_mul_mul_le
For 0 < s < t, the lower integral of p_(2s)(y-z1) p_(2s)(y-z2) p_((t-s)/2)(x-y) is at most sqrt(2t/s) p_(2t)(x-z1) p_(2t)(x-z2).
RoughHeatKernel.lintegral_heatKernel_sq_mul_lheatFlow_two_mul_sq_le
For every s-finite nu and 0 < s < t, the lower integral of p_(t-s)(x-y)^2 J(2s,y)^2 is at most sqrt(t)/(sqrt(2*pi)*sqrt(s*(t-s))) J(2t,x)^2.
RoughHeatKernel.heatKernel_sq_le_local
Local Gaussian-square domination on a positive-time neighborhood with bounded output displacement; an explicit integrable envelope for continuity arguments.
RoughHeatKernel.continuousAt_heatFlow_joint
Joint time-space continuity of the heat flow at every positive time for any Gaussian-tempered positive measure, including infinite mass.
RoughHeatKernel.RoughMeasure.continuousAt_heatFlow_joint
Joint time-space continuity at every positive time for signed Jordan data with Gaussian-tempered total variation; no finite-total-variation assumption.
RoughHeatKernel.SpatialEnvelope.quarter_increment
Uniform quarter-Hölder Gaussian envelope: for every r>0 and u,v, |p_r(u)-p_r(v)| is bounded by 2 exp(1) |u-v|^(1/4) r^(-1/8) times p_(2r)(u)+p_(2r)(v).
Machine data: claims.yaml · THEOREM_INVENTORY.txt.