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.deGiorgi_energy_estimate_on_concentricBalls_of_ballPosPart
Plain-language statement
Localized De Giorgi energy estimate on concentric balls. This packages the weighted Caccioppoli inequality together with the localization step.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.deGiorgi_energy_estimate_on_concentricBalls_of_posPartApprox
Plain-language 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
Plain-language 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
Plain-language 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
Plain-language statement
Packaged pre-iteration step after Sobolev, energy, and Chebyshev inputs.
Source project: DeGiorgi
Person-level attribution pending.