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 187 research declarations. Search 10,000 more complete Mathlib declarations.
187 results
Clear filtersHeat.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.
Heat.integral_mul_exp_neg_sq_Ici_zero
Plain-language statement
Evaluation of ∫₀^∞ z exp(-z²) dz = 1/2.
Source project: PDE
Person-level attribution pending.
Heat.integral_split_near_far
Project documentation
Helper lemma for splitting integrals into near and far regions.
Source project: PDE
Person-level attribution pending.
integral_smul_aezero_tsupport
Plain-language statement
If f vanishes a.e. on U and g is supported in U, then ∫ f • g ∂μU = 0.
Source project: PDE
Person-level attribution pending.
integral_tendsto_of_Lploc_tendsto
Plain-language statement
If f i converges to g in Lᵖ(U), then for any test function ψ ∈ C_c^∞(U), the integrals ∫ f i * ψ ∂μU converge to ∫ g * ψ ∂μU.
Source project: PDE
Person-level attribution pending.