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 filtersWkpU.derivELpNorm_zero_le_eNorm
Plain-language statement
The eLpNorm of f is bounded by the Sobolev eNorm.
Source project: PDE
Person-level attribution pending.
WkpU.derivToLp_sub
Plain-language statement
The projection of the weak derivative of f - g to Lp equals the difference of the projections of the weak derivatives of f and g.
Source project: PDE
Person-level attribution pending.
WkpU.eNorm_add_le
Plain-language statement
Triangle inequality for eLpNorm.
Source project: PDE
Person-level attribution pending.
WkpU.eNorm_eq_zero_of_ae_zero
Plain-language statement
If f : WkpU d k p U hU is almost everywhere zero on U, then its Sobolev eNorm is zero.
Source project: PDE
Person-level attribution pending.
WkpU.eNorm_ne_top
Plain-language statement
The W^{k,p}(U) norm is finite.
Source project: PDE
Person-level attribution pending.
WkpU.eNorm_smul
Plain-language statement
Absolute homogeneity for eNorm .
Source project: PDE
Person-level attribution pending.