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 829 to 834 of 2,569 results.
DeGiorgi.sobolev_poincare_unitBall
Mathematical statement
Sobolev-Poincare inequality on the unit ball.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.sobolev_poincare_unitBall'
Mathematical statement
Sobolev-Poincare inequality for MemW1p in existential form.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.sobolev_prepare_on_ball
Mathematical 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
Mathematical 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
Mathematical 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.
DeGiorgi.super_sq_le_of_le_rpow_half_mul
Mathematical statement
Squaring a bound of the form c ≤ a^(1/2) * b^(1/2) gives c² ≤ a * b.
Source project: DeGiorgi
Person-level attribution pending.