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 filtersDeGiorgi.weighted_caccioppoli_absorb
Plain-language statement
Abstract absorption step for weighted Caccioppoli.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.zeroExtend_memW01p_p
Plain-language statement
Zero-extension of a compactly supported local W₀^{1,p} witness to all of ℝ^d.
Source project: DeGiorgi
Person-level attribution pending.
FderivCcinfty
Plain-language statement
The Fréchet derivative x ↦ (∂ˢψ(x))(unitSeq s) of a test function ψ ∈ Cc^∞(U) again lies in Cc^∞(U). This is used to compose the weak derivative definition with itself.
Source project: PDE
Person-level attribution pending.
heat_from_convolution_heatKernel
Project documentation
Swap the second spatial derivative with the integral . -/ lemma swap_xx_heatKernel {α : ℝ} {x t : ℝ} (g : ℝ → ℝ) (ht : 0 < t) (hα : 0 < α) (hg : Integrable g) : HasDerivAt (fun x' => ∫ y, HKx α (x' - y) t * g y ∂volume) (∫ y, HKxx α (x - y) t * g y ∂volume) x := by have mem_nhds : Metric.ball x 1 ∈ 𝓝 x := Metric.ball_mem_nhds x (by...
Source project: PDE
Person-level attribution pending.
Heat.deriv_exp_heatKernel
Plain-language statement
Derivative of the exponential term exp(-(x²)/(4αt)) with respect to x.
Source project: PDE
Person-level attribution pending.
Heat.deriv_sqrt_inv
Plain-language statement
Derivative of 1/√x at a positive point.
Source project: PDE
Person-level attribution pending.