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 187 research declarations. Search 10,000 more complete Mathlib declarations.
187 results
Clear filtersDeGiorgi.EllipticCoeff.quadratic_upper
Plain-language statement
Pointwise quadratic upper bound derived from the mixed bound.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.eLpNorm_const_average_le
Plain-language statement
Jensen's inequality for eLpNorm: the L^p norm of a constant equal to the average is at most the L^p norm of the function. For 1 ≤ p < ⊤, an integrable f, and a finite measure μ: eLpNorm (fun _ => ⨍ x, f x ∂μ) p μ ≤ eLpNorm f p μ This is a consequence of Jensen's inequality for the convex function t ↦ |t|^p, proved here via Hölder's ine...
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.essSup_halfBall_le_of_ae_bound
Plain-language statement
An a.e. upper bound on the half ball upgrades to an essential-supremum bound on the half ball.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.exists_finite_inner_ball_cover
Plain-language statement
A compact inner ball can be covered by finitely many smaller balls whose dilated closed balls still lie inside the ambient ball.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.exists_finite_inner_ball_cover_with_card
Plain-language statement
A quantitative version of exists_finite_inner_ball_cover with a coarse explicit cardinality bound depending only on r / ρ and d.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.exists_global_smooth_W1p_approx_of_localizedWitness
Plain-language statement
Global smooth compactly supported approximation for a local witness whose support is already compactly contained in the source open set.
Source project: DeGiorgi
Person-level attribution pending.