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.exists_halfBall_cover_by_eighth_balls
Plain-language statement
A specialized quantitative cover tailored to the half-ball / eighth-ball geometry used in the crossover argument.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.exists_smooth_compactSupport_W1p_approx_univ
Plain-language statement
Global smooth compactly supported approximation of a compactly supported W^{1,p} function on ℝ^d, in the finite-p regime.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.exists_smooth_W12_approx_on_unitBall
Project documentation
L² specialization of the unit-ball smooth approximation theorem.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.exists_smooth_W1p_approx_on_unitBall
Plain-language statement
Sequence form of full W^{1,p} smooth approximation on the unit ball.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.exists_unitBall_cutoff
Plain-language statement
Smooth cutoff: φ = 1 on closedBall 0 1, tsupport ⊆ ball 0 (7/6), range ⊆ [0,1]. Used for the log gradient bound on rescaled cover balls.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.harnack
Plain-language statement
Positive weak solutions satisfy Harnack on the unit ball.
Source project: DeGiorgi
Person-level attribution pending.