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 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 739 to 744 of 2,569 results.
DeGiorgi.deGiorgi_energy_estimate_on_concentricBalls_of_posPartApprox
Mathematical statement
Localized De Giorgi energy estimate using the concrete Chapter 02 positive-part witness constructor on the outer ball.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.deGiorgi_preiter_abstract
Mathematical statement
Abstract real-variable combination step for De Giorgi pre-iteration.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.deGiorgi_preiter_of_ballSobolev_on_concentricBalls_of_ballPosPart
Project documentation
PDE-facing De Giorgi pre-iteration wrapper on concentric balls. This theorem packages the bookkeeping step that combines: - a localized De Giorgi energy estimate at level θ, - a Sobolev/Hölder interpolation input for level λ, - and the Chebyshev bound already proved in this chapter. The local Sobolev/Hölder interpolation theorem is kept as an explicit...
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.deGiorgi_preiter_of_ballSobolev_on_concentricBalls_of_posPartApprox
Mathematical statement
De Giorgi pre-iteration on concentric balls using the concrete positive-part witness constructor on the outer ball.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.deGiorgi_preiter_of_energy
Mathematical statement
Packaged pre-iteration step after Sobolev, energy, and Chebyshev inputs.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.deGiorgi_preiter_on_concentricBalls_of_ballPosPart
Project documentation
PDE-facing De Giorgi pre-iteration theorem on concentric balls. This now factors through the explicit cutoff-Sobolev bridge deGiorgi_cutoffSobolev_on_concentricBalls_of_ballPosPart instead of keeping the local Sobolev argument bundled into one monolithic proof.
Source project: DeGiorgi
Person-level attribution pending.