Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 41 research declarations. Search 10,000 more complete Mathlib declarations.
41 results
Clear filtersHeat.hasDerivAt_heatKernel_x_x
Project documentation
Auxiliary lemma: derivative of the first spatial derivative's formula.
Source project: PDE
Person-level attribution pending.
Heat.hasDerivAt_heatKernel_xx
Plain-language statement
The second spatial derivative of the heat kernel ∂²/∂x² heatKernel(α, x, t).
Source project: PDE
Person-level attribution pending.
Heat.heatKernel_mass_one_x_sub_y_even
Plain-language statement
Translation Invariance: The heat kernel integrates to 1 regardless of translation. -
Source project: PDE
Person-level attribution pending.
Heat.heatTail_changeOfVariables
Plain-language statement
Change of variables formula for heat kernel tail integrals. Transforms the integral ∫_{|y-x| ≥ δ} Φ(x-y,t) dy into a standard Gaussian tail integral via the substitution z = (x-y)/√(4αt).
Source project: PDE
Person-level attribution pending.
Heat.integral_heatKernel_one_gaussian
Plain-language statement
Property 2: The heat kernel integrates to one over all of ℝ. This shows that the heat kernel is properly normalized and can be interpreted as a probability density function (specifically, a Gaussian distribution).
Source project: PDE
Person-level attribution pending.
Heat.integral_indicator_tail_even
Plain-language statement
For even functions, the two-sided tail integral equals twice the one-sided integral.
Source project: PDE
Person-level attribution pending.