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 filtersintegral_smul_aezero_tsupport
Plain-language statement
If f vanishes a.e. on U and g is supported in U, then ∫ f • g ∂μU = 0.
Source project: PDE
Person-level attribution pending.
integral_tendsto_of_Lploc_tendsto
Plain-language statement
If f i converges to g in Lᵖ(U), then for any test function ψ ∈ C_c^∞(U), the integrals ∫ f i * ψ ∂μU converge to ∫ g * ψ ∂μU.
Source project: PDE
Person-level attribution pending.
NNReal.rpow_sum_le_sum
Plain-language statement
A discrete Minkowski inequality: for p ≥ 1 and a finite sequence a : Fin n → ℝ≥0, the ℓᵖ norm of a is bounded above by the sum of its entries.
Source project: PDE
Person-level attribution pending.
WkpU.cauchySeq_derivtoLp
Plain-language statement
A Cauchy sequence in W^{k,p}(U) induces a Cauchy sequence in Lp for each weak derivative component.
Source project: PDE
Person-level attribution pending.
WkpU.derivELpNorm_add_le
Plain-language statement
Triangle inequality for a single weak-derivative eLpNorm.
Source project: PDE
Person-level attribution pending.
WkpU.derivELpNorm_le_eNorm
Plain-language statement
Each weak-derivative eLpNorm is bounded by the Sobolev eNorm.
Source project: PDE
Person-level attribution pending.