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 805 to 810 of 2,569 results.
DeGiorgi.memW01p_of_contDiff_hasCompactSupport_subset
Mathematical statement
A smooth compactly supported function whose support is contained in an open set belongs to W₀^{1,p} on that set.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.memW01p_of_memW1p_of_tsupport_subset
Mathematical statement
Localization by compact support: a finite-p Sobolev function whose support is compactly contained in an open set belongs to W₀^{1,p}.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.MemW01p.add
Mathematical statement
H₀¹(Ω) is closed under addition.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.MemW01p.smul
Mathematical statement
H₀¹(Ω) is closed under scalar multiplication.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.MemW1pWitness.ae_eq
Mathematical statement
Two W^{1,2} witnesses on an open set have a.e.-equal gradients.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.MemW1pWitness.ae_eq_p
Mathematical statement
Weak gradients of the same W^{1,p} function agree a.e. on the source open set.
Source project: DeGiorgi
Person-level attribution pending.