Project-declaredLean 4.30.0
Wkp U ibp tendsto
WkpU.ibp_tendsto
Plain-language statement
The IBP identity passes to the limit.
partial differential equationsSobolev spacesanalysis
Source project: PDE
Person-level attribution pending.
Source-pinned research
Research proof index
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 filtersView proof record
Project-declaredLean 4.30.0
Wkp U limit mem
WkpU.limit_mem
Plain-language statement
Given an Lp limit g and derivative limits g_ns, package them into a WkpU element.
partial differential equationsSobolev spacesanalysis
Source project: PDE
Person-level attribution pending.
Project-declaredLean 4.30.0
Wkp U limit of cauchy Seq
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.
partial differential equationsSobolev spacesanalysis
Source project: PDE
Person-level attribution pending.
Project-declaredLean 4.30.0
Wkp U norm derivto Lp le
WkpU.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.
partial differential equationsSobolev spacesanalysis
Source project: PDE
Person-level attribution pending.
Project-declaredLean 4.30.0
Wkp U tendsto iff all deriv ELp Norm
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.
partial differential equationsSobolev spacesanalysis
Source project: PDE
Person-level attribution pending.
Project-declaredLean 4.30.0
Wkp UNorm eq zero iff
WkpUNorm_eq_zero_iff
Plain-language statement
The W^{k,p}(U) norm vanishes iff the function is zero a.e..
partial differential equationsSobolev spacesanalysis
Source project: PDE
Person-level attribution pending.