Alphabeta MathHow 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 polynomial map and its Jacobian
Example
Let . Then is totally differentiable everywhere and
Facts & Assumptions
Given: The polynomial map .
The function is differentiable everywhere with derivative for positive natural (For a natural the function is differentiable everywhere with derivative ; for it is the constant , with derivative ; for a natural the function is differentiable at every with derivative ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term).
Continuous partial derivatives imply total differentiability with Jacobian derivative (If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative).
Verification
The four partial derivatives are , , , and , by [L1] and derivative algebra.
These polynomial partial derivatives are continuous everywhere, so [L2] gives total differentiability and identifies the derivative with the displayed Jacobian.
Directly, the increment remainder is , whose norm divided by tends to zero, agreeing with step 2.1.
Depends on
- If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative
- The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case
- For a natural $n \ge 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $\iota(n)\,x^{\,n-1}$; for $n = 0$ it is the constant $1$, with derivative $0$; for a natural $n \ge 1$ the function $x \mapsto x^{-n}$ is differentiable at every $x \ne 0$ with derivative $-\iota(n)\,x^{-n-1}$; consequently every polynomial function is differentiable at every real, with the derivative computed term by term
- Sums, scalar multiples, products and quotients: $(f+g)'(c) = f'(c) + g'(c)$, $(\alpha f)'(c) = \alpha f'(c)$, $(fg)'(c) = f'(c)g(c) + f(c)g'(c)$, and $(f/g)'(c) = \bigl(f'(c)g(c) - f(c)g'(c)\bigr)/g(c)^{2}$ when $g(c) \ne 0$
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 99 results over 23 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.4 (standard reference, not scraped)