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 146 research declarations. Search 10,000 more complete Mathlib declarations.

All topics

146 results

Clear filters
Project-declaredLean 4.29.0-rc6

Campanato implies holder

DeGiorgi.campanato_implies_holder

Plain-language statement

A Campanato bound determines a Hölder representative up to a.e. equality.

partial differential equationsregularity theoryanalysis

Source project: DeGiorgi

Person-level attribution pending.

View proof record
Project-declaredLean 4.29.0-rc6

Countable isolated

DeGiorgi.countable_isolated

Plain-language statement

In ℝ, the set of isolated points of any subset S is countable. Proof: cover by ⋃_{p,q ∈ ℚ} {unique element of S in (p,q)}. Each fiber has at most one element (uniqueness), and ℚ × ℚ is countable.

partial differential equationsregularity theoryanalysis

Source project: DeGiorgi

Person-level attribution pending.

View proof record
Project-declaredLean 4.29.0-rc6

Crossover estimate

DeGiorgi.crossover_estimate

Plain-language statement

Crossover estimate bridging positive and negative powers of a positive supersolution.

partial differential equationsregularity theoryanalysis

Source project: DeGiorgi

Person-level attribution pending.

View proof record
Project-declaredLean 4.29.0-rc6

Crossover estimate unaveraged

DeGiorgi.crossover_estimate_unaveraged

Plain-language statement

Un-averaged half-ball version of crossover_estimate. This is the form needed by downstream weak-Harnack bookkeeping: multiply the average-product estimate by |B_{1/2}|^2.

partial differential equationsregularity theoryanalysis

Source project: DeGiorgi

Person-level attribution pending.

View proof record
Project-declaredLean 4.29.0-rc6

De Giorgi cutoff Sobolev on concentric Balls of ball Pos Part

DeGiorgi.deGiorgi_cutoffSobolev_on_concentricBalls_of_ballPosPart

Plain-language statement

Sobolev/Hölder step for De Giorgi pre-iteration on concentric balls. The argument passes through a zero-trace cutoff witness for η² (u - θ)₊. The originally intended statement with only the bare θ-truncation gradient on the right-hand side is false, e.g. for constant superlevel functions. The proof here records the actual Chapter 05 mechanism: 1. buil...

partial differential equationsregularity theoryanalysis

Source project: DeGiorgi

Person-level attribution pending.

View proof record