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 10 research declarations. Search 10,000 more complete Mathlib declarations.
10 results
Clear filterscLpNorm_dft_indicator_one_pow
Plain-language statement
The -th Fourier moment of the indicator of a finite set equals its order- additive energy: . This is the standard bridge between Fourier norms and additive tuple counts.
Source project: Arithmetic Progressions Almost Periodicity
Person-level attribution pending.
DeGiorgi.caccioppoli_localize_on_subset
Plain-language statement
Localization step for weighted Caccioppoli on nested sets.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.caccioppoli_weighted_on_ball_of_ballPosPart
Project documentation
Ball-specialized weighted Caccioppoli inequality, using the generalized cutoff admissibility theorem from the previous section.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.caccioppoli_weighted_on_ball_of_posPartApprox
Plain-language statement
Ball-specialized weighted Caccioppoli inequality with the truncation witness constructed from the concrete Chapter 02 positive-part API.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.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.