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.abs_sub_const_bmo_le_two
Plain-language statement
The absolute value function |u - c| has BMO seminorm at most 2M whenever u has BMO seminorm at most M. Uses the reverse triangle inequality ||a| - |b|| ≤ |a - b|.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.abs_subballAverage_sub_ballAverage_le
Plain-language 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
Plain-language 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
Plain-language statement
A zero-trace Sobolev function with vanishing L² gradient class vanishes almost everywhere.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.aestronglyMeasurable_bilinFormIntegrandOfCoeff
Plain-language statement
The bilinear-form integrand is a.e. strongly measurable on Ω.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.aestronglyMeasurable_divergenceRHSIntegrandOfField
Plain-language statement
The divergence-form RHS integrand is a.e. strongly measurable on Ω.
Source project: DeGiorgi
Person-level attribution pending.