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 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 733 to 738 of 2,569 results.
DeGiorgi.countable_isolated
Mathematical 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.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.crossover_estimate
Mathematical statement
Crossover estimate bridging positive and negative powers of a positive supersolution.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.crossover_estimate_unaveraged
Mathematical 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.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.deGiorgi_cutoffSobolev_on_concentricBalls_of_ballPosPart
Mathematical 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...
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.deGiorgi_cutoffSobolev_on_concentricBalls_of_posPartApprox
Mathematical statement
Sobolev/Hölder step for De Giorgi pre-iteration on concentric balls, using the concrete positive-part approximation input.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.deGiorgi_energy_estimate_on_concentricBalls_of_ballPosPart
Mathematical 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.