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 715 to 720 of 2,569 results.
DeGiorgi.abs_subballAverage_sub_ballAverage_le
Mathematical statement
The average on a sub-ball differs from the average on a larger ball by at most the volume ratio times the mean oscillation on the larger ball.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.ae_eq_dyadicBallAverageLimit_on_halfBall
Mathematical statement
On the inner ball, the dyadic Campanato average limit agrees a.e. with the original function.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.ae_eq_zero_of_memH01_of_gradLpOfWitness_eq_zero
Mathematical statement
A zero-trace Sobolev function with vanishing L² gradient class vanishes almost everywhere.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.aestronglyMeasurable_bilinFormIntegrandOfCoeff
Mathematical statement
The bilinear-form integrand is a.e. strongly measurable on Ω.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.aestronglyMeasurable_divergenceRHSIntegrandOfField
Mathematical statement
The divergence-form RHS integrand is a.e. strongly measurable on Ω.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.aestronglyMeasurable_unitBallExtension_of_memLp
Mathematical statement
AEStronglyMeasurable for unitBallExtension of rough u. Uses measurable representative + ae_eq transfer.
Source project: DeGiorgi
Person-level attribution pending.