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 4 research declarations. Search 10,000 more complete Mathlib declarations.
4 results
Clear filtersFderivCcinfty
Plain-language statement
The Fréchet derivative x ↦ (∂ˢψ(x))(unitSeq s) of a test function ψ ∈ Cc^∞(U) again lies in Cc^∞(U). This is used to compose the weak derivative definition with itself.
Source project: PDE
Person-level attribution pending.
IsOpen.ae_eq_of_integral_contDiff_smul_eq
Project documentation
If ∫ ψ · f = ∫ ψ · g for all ψ ∈ Cc^∞(U), then f =ᵃᵉ g on U. This is the du Bois-Reymond lemma, the key uniqueness engine for weak derivatives.
Source project: PDE
Person-level attribution pending.
WeakDerivUniqU
Project documentation
Uniqueness of weak multi-derivatives on U: any two candidates must agree almost everywhere on U. The proof reduces to the du Bois-Reymond lemma via the defining identity.
Source project: PDE
Person-level attribution pending.
zeroWeakmultiDerivU
Project documentation
Any weak multi-derivative Df on U agrees a.e. with the canonical choice. -/ theorem WeakmultiderivU_unique {d : ℕ+} {n : ℕ} {U : Set (Fin d → ℝ)} (hU : IsOpen U) (s : Fin n → Fin d) (f : Lp_locU d 1 U) (h : HasWeakMultiDerivU U f s) (Df : Lp_locU d 1 U) (hDf : IsWeakMultiDerivU U s f Df) : (WeakmultiderivU U f s h : (Fin d → ℝ) →ₘ[μU d U] ℝ) =ᵐ[volume...
Source project: PDE
Person-level attribution pending.