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.
The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case
Definition
If every partial derivative of exists, the Jacobian matrix is . For scalar-valued , its gradient is
with coordinates understood in the standard basis (The standard list with and for is an ordered basis of ; hence , and is the zero space with basis and dimension ). The partial derivatives are those of Directional derivatives and partial derivatives of a map .
Depends on
- Directional derivatives and partial derivatives of a map $U\subseteq\mathbb{R}^m\to\mathbb{R}^n$
- The Euclidean inner product $\langle x,y\rangle = \sum_{k<n} x_k y_k$ on $\mathbb{R}^n$
- The standard list $e : n \to F^{n}$ with $e_i(i) = 1_F$ and $e_i(j) = 0_F$ for $j \ne i$ is an ordered basis of $F^{n}$; hence $\dim_F F^{n} = n$, and $F^{0}$ is the zero space with basis $\varnothing$ and dimension $0$
Used by
- Lagrange multipliers for a regular graph constraint y=ψ(x) Corollary
- The degenerate constraint x²+y²=0 defeats the multiplier conclusion Counterexample
- Continuously differentiable maps, local inverses, and local diffeomorphisms Definition
- The Hessian matrix and critical points of a scalar field Definition
- The Jacobian determinant of a square-dimensional C¹ map is the determinant of its Jacobian matrix Definition
- The polynomial map (x,y)↦(1+x+2y+x², 2x+3y+xy) and its Jacobian Example
- A total derivative computes every directional derivative, and its matrix is the Jacobian Theorem
- Fermat's theorem: an interior differentiable local extremum has zero gradient Theorem
- For a differentiable scalar field, Dᵥf(a)=⟨∇ f(a),v⟩ and the unit direction of steepest ascent is the normalized gradient Theorem
- If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 121 results over 29 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- J. Lebl, Basic Analysis I, §8.3 (standard reference, not scraped)