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 10 research declarations. Search 10,000 more complete Mathlib declarations.
10 results
Clear filtersDeGiorgi.ae_eq_zero_of_memH01_of_gradLpOfWitness_eq_zero
Plain-language statement
A zero-trace Sobolev function with vanishing L² gradient class vanishes almost everywhere.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.aHarmonic_replacement_exists
Plain-language statement
A-harmonic replacement: given u ∈ W^{1,2}(B_R), there exists h that is A-harmonic with h - u ∈ W₀^{1,2}(B_R).
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.aHarmonic_replacement_unique
Plain-language statement
A-harmonic replacements are unique up to a.e. equality.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.dirichletProblem_exists_of_divergenceData
Plain-language statement
Existence of weak solutions to the inhomogeneous Dirichlet problem with boundary datum u₀ and divergence-form right-hand side div F.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.dirichletProblem_stability_of_divergenceData
Plain-language statement
Energy estimate for the shifted Dirichlet solution u - u₀.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.dirichletProblem_unique_of_divergenceData
Plain-language statement
Inhomogeneous Dirichlet solutions are unique up to a.e. equality.
Source project: DeGiorgi
Person-level attribution pending.