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 21 research declarations. Search 10,000 more complete Mathlib declarations.
21 results
Clear filtersWkpU.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.
WkpU.ibp_tendsto
Plain-language statement
The IBP identity passes to the limit.
Source project: PDE
Person-level attribution pending.
WkpU.limit_mem
Plain-language statement
Given an Lp limit g and derivative limits g_ns, package them into a WkpU element.
Source project: PDE
Person-level attribution pending.
WkpU.limit_of_cauchySeq
Plain-language statement
A Cauchy sequence in W^{k,p}(U) has a limit f_lim in W^{k,p}(U), with the toLp and derivtoLp projections of the sequence converging to those of f_lim.
Source project: PDE
Person-level attribution pending.