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 793 to 798 of 2,569 results.

Project-declaredLean 4.29.0-rc6

Linfty subsolution De Giorgi

DeGiorgi.linfty_subsolution_DeGiorgi

Mathematical statement

De Giorgi L∞ bound for subsolutions on the unit ball. The positive part is bounded almost everywhere on the half-ball by an explicit coefficient-dependent constant times the size of u₊ on B₁. The result is stated as an a.e. bound rather than a pointwise supremum bound, since the representative/continuity upgrade comes later in the theory.

partial differential equationsregularity theoryanalysis

Source project: DeGiorgi

Person-level attribution pending.

View proof record
Project-declaredLean 4.29.0-rc6

Linfty subsolution De Giorgi ae of unit Ball height bound

DeGiorgi.linfty_subsolution_DeGiorgi_ae_of_unitBall_height_bound

Mathematical statement

Height-threshold version of the De Giorgi endpoint. Once the PDE-facing one-step estimate is supplied, a lower bound for lamStar of the form C(d,K) * sqrt(∫_{B₁} (u₊)^2) yields the a.e. half-ball L∞ bound.

partial differential equationsregularity theoryanalysis

Source project: DeGiorgi

Person-level attribution pending.

View proof record
Project-declaredLean 4.29.0-rc6

Linfty subsolution De Giorgi ae of unit Ball initial energy smallness

DeGiorgi.linfty_subsolution_DeGiorgi_ae_of_unitBall_initial_energy_smallness

Project documentation

Unit-ball smallness packaging for the De Giorgi endpoint. This is the direct successor to the raw hsmall-based theorem: instead of assuming a bound on the abstract initial De Giorgi energy A₀, it is enough to assume the same recurrence threshold for the concrete unit-ball quantity ∫_{B₁} (u₊)^2. The radius/level bookkeeping then supplies the A₀ bo...

partial differential equationsregularity theoryanalysis

Source project: DeGiorgi

Person-level attribution pending.

View proof record
Project-declaredLean 4.29.0-rc6

Linfty subsolution De Giorgi ae zero of smallness

DeGiorgi.linfty_subsolution_DeGiorgi_ae_zero_of_smallness

Mathematical statement

Small-data De Giorgi endpoint: if the canonical De Giorgi energy sequence tends to zero, then the final truncation vanishes almost everywhere on the half-ball. This is the formally correct endpoint available from the current Chapter 05 infrastructure before any representative/continuity upgrade.

partial differential equationsregularity theoryanalysis

Source project: DeGiorgi

Person-level attribution pending.

View proof record
Project-declaredLean 4.29.0-rc6

Linfty subsolution De Giorgi normalized

DeGiorgi.linfty_subsolution_DeGiorgi_normalized

Mathematical statement

Normalized-coefficient De Giorgi L∞ bound with the explicit scaling C(d) * Λ^(d/4) on the unit ball.

partial differential equationsregularity theoryanalysis

Source project: DeGiorgi

Person-level attribution pending.

View proof record