Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicable
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.

Directional derivatives and partial derivatives of a map U⊆Rm→Rn

Definition

Let U⊆Rm, a∈U, v∈Rm, and f:U→Rn. If the line map t↦f(a+tv) is defined near 0, its derivative at 0 is the directional derivative

Dvf(a):=lim⁡t→0f(a+tv)−f(a)t.

For a standard basis vector ej (The standard list e:n→Fn with ei(i)=1F and ei(j)=0F for j≠i is an ordered basis of Fn; hence dim⁡FFn=n, and F0 is the zero space with basis ∅ and dimension 0), Dejf(a) is the jth partial derivative, written ∂jf(a). For n≥1, these are ordinary vector-valued one-variable derivatives in the sense of The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral.

For n=0, use the zero-space case directly, without invoking that supplier's positive-codomain standing hypothesis. The space R0 has only its zero vector and carries the zero Euclidean norm and its induced metric (The standard list e:n→Fn with ei(i)=1F and ei(j)=0F for j≠i is an ordered basis of Fn; hence dim⁡FFn=n, and F0 is the zero space with basis ∅ and dimension 0 clause 5, The Euclidean inner product ⟨x,y⟩=∑k<nxkyk on Rn, A norm on a real vector space, the induced metric, and the dictionary with the metric axioms). Whenever the line map is defined near 0, every difference quotient for real t≠0 is this zero vector; define Dvf(a)=0. This is the unique possible derivative value, and its normwise difference-quotient error is exactly zero for all such t, so the real parameter still approaches an actual limit point. Every existing coordinate direction therefore has ∂jf(a)=0; these zero-valued partial maps are continuous in the induced norm metrics. If the source dimension is zero, there are no partial indices and the sole direction is v=0; its constant line map is defined near 0.

Depends on

Dependency tree · 2 levels

Sources