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.sobolev_poincare_smooth_unitBall
Plain-language statement
Sobolev-Poincare for smooth functions on the unit ball.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.sobolev_poincare_unitBall
Plain-language statement
Sobolev-Poincare inequality on the unit ball.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.sobolev_poincare_unitBall'
Plain-language statement
Sobolev-Poincare inequality for MemW1p in existential form.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.sobolev_prepare_on_ball
Plain-language statement
Generic local Sobolev preparation on a ball: zero-extend a W₀^{1,2} ball witness to the whole space, apply Sobolev, then restrict back. This is the Chapter 06 analogue of the private Chapter 05 helper for cutoff functions.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.sobolev_smooth
Plain-language statement
Sobolev inequality for smooth compactly supported functions at general p. Direct wrapper around Mathlib's eLpNorm_le_eLpNorm_fderiv_of_eq.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.stampacchia_1d
Plain-language statement
1D Stampacchia for W^{1,1}: the weak derivative g vanishes a.e. on {u = 0}. Proof: replace u by its AC representative F (from w11_ae_eq_ac_representative). Then F' = g a.e. by the FTC. Apply deriv_eq_zero_ae_on_zeroSet to F.
Source project: DeGiorgi
Person-level attribution pending.