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 757 to 762 of 2,569 results.
DeGiorgi.divergenceRHSOfField_add
Mathematical statement
The divergence-form RHS is additive in the test slot.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.divergenceRHSOfField_bound
Mathematical 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
Mathematical statement
Mixed bilinear bound needed by the variational branch.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.EllipticCoeff.mulVec_sq_le
Mathematical statement
Mixed quadratic bound derived from inverse coercivity.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.EllipticCoeff.quadratic_upper
Mathematical statement
Pointwise quadratic upper bound derived from the mixed bound.
Source project: DeGiorgi
Person-level attribution pending.