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.
A linear map in Euclidean coordinates
Definition
Let . A map is linear when
for all and all . Both spaces carry their Euclidean vector-space operations and Euclidean norms from The Euclidean inner product on .
Remarks
This is the concrete Euclidean notion required for total differentiation. It makes no assertion about linear maps between arbitrary vector spaces.
Depends on
Used by
- x²y/(x²+y²) has every directional derivative at the origin but is not totally differentiable there Counterexample
- Holomorphic functions on an open subset of ℂᵐ Definition
- Holomorphic maps ℂᵐ → ℂⁿ and the complex Jacobian matrix Definition
- Invertible Euclidean linear maps Definition
- The total (Fréchet) derivative Df(a) as the linear first-order approximation with o(‖h‖₂) remainder Definition
- A real-linear functional on ℂᵐ is complex linear exactly when its antiholomorphic part vanishes Lemma
- Every Euclidean linear map has a unique matrix and satisfies ‖Lh‖₂≤ K‖h‖₂ for some K≥0 Lemma
- Nonnegative combinations, affine precomposition, and finite pointwise maxima preserve convexity Proposition
- Dimension, openness, norm, Jacobian, and the native Euclidean linear-map agreement seam Remark
- Complex differentiability is equivalent to real total differentiability together with a complex-linear derivative, with ∂_z̄f=0, or with the Cauchy–Riemann equations Theorem
- Sums and scalar multiples of totally differentiable maps are totally differentiable with the expected derivatives Theorem
- The chain rule for total derivatives: D(g∘ f)(a)=Dg(f(a))∘ Df(a) Theorem
- The composite of holomorphic maps is holomorphic and its complex Jacobian is the product Theorem
Dependency tree · two levels
14 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
- J. Lebl, Basic Analysis I, §8.3 (standard reference, not scraped)