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.norm_derivtoLp_le
Plain-language statement
The Lp norm of the n-th weak derivative of f is bounded by the W^{k,p} norm.
Source project: PDE
Person-level attribution pending.
WkpU.tendsto_iff_all_derivELpNorm
Plain-language statement
Convergence in W^{k,p}(U) is equivalent to convergence of each weak-derivative eLpNorm component to zero: fₙ → f in W^{k,p} if and only if ‖D^s(fₙ - f)‖_{Lp} → 0 for all multi-indices s with |s| ≤ k.
Source project: PDE
Person-level attribution pending.
WkpUNorm_eq_zero_iff
Plain-language statement
The W^{k,p}(U) norm vanishes iff the function is zero a.e..
Source project: PDE
Person-level attribution pending.