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 146 research declarations. Search 10,000 more complete Mathlib declarations.
146 results
Clear filtersDeGiorgi.dirichletProblem_unique_of_divergenceData
Plain-language statement
Inhomogeneous Dirichlet solutions are unique up to a.e. equality.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.divergenceRHSOfField_add
Plain-language statement
The divergence-form RHS is additive in the test slot.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.divergenceRHSOfField_bound
Plain-language statement
The divergence-form RHS is bounded with respect to the L² gradient seminorm.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.du_bois_reymond
Project documentation
Du Bois-Reymond lemma: if g ∈ L^1(a,b) and ∫ g · φ' = 0 for all smooth compactly supported φ in (a,b), then g is constant a.e. Proof (Evans, Appendix C): fix ψ₀ ∈ C_c^∞(a,b) with ∫ψ₀ = 1, set c = ∫g·ψ₀. For any test η, decompose η = [η - (∫η)·ψ₀] + (∫η)·ψ₀. The first part has zero integral, hence is φ' for some test φ (antideri...
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.EllipticCoeff.mixed_bound
Plain-language statement
Mixed bilinear bound needed by the variational branch.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.EllipticCoeff.mulVec_sq_le
Plain-language statement
Mixed quadratic bound derived from inverse coercivity.
Source project: DeGiorgi
Person-level attribution pending.