How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
maps and multi-index derivative notation in Euclidean space
Definition
Let , let be open, and let . A multi-index is . Put
Here and use the natural-number sum and product of Finite sums and finite products of natural numbers, and in , and is the factorial of The factorial and the falling factorial , defined by recursion in . By contrast, is the finite product in of Finite sums and finite products, by recursion, with the natural exponents interpreted by Integer powers . For the zero multi-index , set . For nonzero , write
for this displayed, canonical order whenever it exists. Coordinate partial derivatives have the meaning fixed in Directional derivatives and partial derivatives of a map .
For , is of class on when, for every word of coordinate indices with , the iterated derivative exists and is continuous on ; the word of length denotes . Thus this definition does not presuppose that differently ordered derivatives are equal. Equality of their values is a later theorem under these regularity hypotheses.
Depends on
- Directional derivatives and partial derivatives of a map $U\subseteq\mathbb{R}^m\to\mathbb{R}^n$
- The factorial $n!$ and the falling factorial $n^{\underline{k}}$, defined by recursion in $\mathbb{N}$
- Finite sums and finite products of natural numbers, $\sum_{k<n} a_k$ and $\prod_{k<n} a_k$ in $\mathbb{N}$
- Finite sums and finite products, by recursion
- Integer powers $a^m$
Used by
- Adjoint hypergradient with a measured linear-solve residual Algorithm
- Every closed subset of a manifold is the zero set of a smooth nonnegative function Corollary
- Green's first identity on a glued elementary solid region Corollary
- Green's second identity on a glued elementary solid region Corollary
- Holomorphic functions are real analytic and smooth in their two real coordinates Corollary
- Holomorphic functions of several variables are smooth and their complex derivatives are holomorphic Corollary
- Multivariable Taylor formula with o(‖h‖ᵏ) remainder Corollary
- The classical Euler-Lagrange equation under regularity Corollary
- The coefficients of a convergent multi-indexed power series are its derivative coefficients, hence unique Corollary
- The curl of a curl is the gradient of the divergence minus the Laplacian Corollary
- The finite-basis projector energy model supplies a C1 Hermitian response map Corollary
- The flux of a curl through the boundary of a glued elementary solid vanishes Corollary
- Unique continuation for harmonic functions Corollary
- A non-Dini continuous Poisson source can destroy the continuity of the second derivatives Counterexample
- A reflected sphere embedding is regularly homotopic but not isotopic to the standard one Counterexample
- An isolated boundary point obstructs pointwise-zero Green data Counterexample
- Bounded measurable coefficients do not give Schauder estimates Counterexample
- Extension by zero without support away from the boundary is not smooth Counterexample
- Neumann Poisson data require a flux compatibility equation Counterexample
- Peano's function has unequal mixed partials at the origin Counterexample
- Point evaluation is unbounded below the Sobolev continuity threshold Counterexample
- The fundamental Hessian is not absolutely locally integrable Counterexample
- Bounded Cᵏ domains and boundary charts Definition
- Cᵏ Euclidean maps and diffeomorphisms Definition
- Complex Lp classes and Euclidean test-function conventions Definition
- Cʳ and smooth maps between smooth manifolds Definition
- Forward and central finite-difference Jacobian-vector and Hessian-vector products Definition
- Grand maximal test class of order N and the grand maximal function Definition
- Hölder spaces C^k,α, closure and interior scaled norms, and C^k,α domains Definition
- Hᵖ atoms with a prescribed moment order Definition
- Local Hölder and scaled C-two-alpha norms on balls Definition
- Mihlin smoothness convention above half the dimension Definition
- Multi-indexed power series in ℂᵐ and their absolute convergence Definition
- Parabolic cylinder and parabolic boundary Definition
- Periodic correctors and effective tensor Definition
- Real-analytic maps between open subsets of the coordinate plane Definition
- Regular minimum-energy paths on a declared collision-free tube Definition
- Scalar conservation laws, fluxes and Cauchy data Definition
- Schwartz space and its seminorms Definition
- Shin's parabolic operator, data, and initial-lateral boundary Definition
…and 138 more results.
Dependency tree · two levels
41 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- MAT237 notes: Taylor's theorem in several variables (standard reference, not scraped)