Skip to main content

Source-pinned research

Research proof index

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.

All topics

Showing 745 to 750 of 2,569 results.

Project-declaredLean 4.29.0-rc6

De Giorgi preiter on concentric Balls of pos Part Approx

DeGiorgi.deGiorgi_preiter_on_concentricBalls_of_posPartApprox

Project documentation

Approximation-based version of the PDE-facing De Giorgi pre-iteration theorem. This is the approximation-driven counterpart of deGiorgi_preiter_on_concentricBalls_of_ballPosPart: instead of taking a pre-built witness for (u - θ)_+ or a generic positive-part closure axiom, it uses the outer-ball smooth approximation package for u - θ. The analytic pr...

partial differential equationsregularity theoryanalysis

Source project: DeGiorgi

Person-level attribution pending.

View proof record
Project-declaredLean 4.29.0-rc6

De Giorgi preiter to recurrence

DeGiorgi.deGiorgi_preiter_to_recurrence

Mathematical statement

Rewrite the one-step estimate on canonical radii and levels into the standard nonlinear recurrence.

partial differential equationsregularity theoryanalysis

Source project: DeGiorgi

Person-level attribution pending.

View proof record
Project-declaredLean 4.29.0-rc6

De Giorgi preiter vanishing

DeGiorgi.deGiorgi_preiter_vanishing

Mathematical statement

The canonical De Giorgi recurrence tends to zero under the standard smallness threshold. This is the non-PDE closeout for the De Giorgi iteration.

partial differential equationsregularity theoryanalysis

Source project: DeGiorgi

Person-level attribution pending.

View proof record
Project-declaredLean 4.29.0-rc6

De Giorgi Cutoff Test mem W01p of pos Part

DeGiorgi.deGiorgiCutoffTest_memW01p_of_posPart

Project documentation

General cutoff admissibility theorem, parameterized by a positive-part witness theorem. This packages the reusable cutoff argument while keeping the localization argument in memW01p_of_memW1p_of_tsupport_subset.

partial differential equationsregularity theoryanalysis

Source project: DeGiorgi

Person-level attribution pending.

View proof record
Project-declaredLean 4.29.0-rc6

De Giorgi Cutoff Test mem W01p of pos Part Approx

DeGiorgi.deGiorgiCutoffTest_memW01p_of_posPartApprox

Project documentation

Concrete cutoff admissibility theorem using the Chapter 02 positive-part witness constructor and an explicit smooth-approximation package for u - k.

partial differential equationsregularity theoryanalysis

Source project: DeGiorgi

Person-level attribution pending.

View proof record
Project-declaredLean 4.29.0-rc6

De Giorgi Cutoff Test mem W01p on ball of ball Pos Part

DeGiorgi.deGiorgiCutoffTest_memW01p_on_ball_of_ballPosPart

Mathematical statement

Ball version of generalized cutoff admissibility. This avoids any dependence on the legacy Cutoff structure.

partial differential equationsregularity theoryanalysis

Source project: DeGiorgi

Person-level attribution pending.

View proof record