Homotopy Type Theory partial derivative > history (Rev #2, changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

Contents

Definition

Given a calculus field?sequentially Cauchy complete Archimedean ordered field F F \mathbb{R} of scalars and a type of indices II, one could define a calculus vector space?real vector space V F I V \coloneqq F^I \mathbb{R}^I with a basis vector function e:IVe:I \hookrightarrow V. Let f:V F f:V \to F \mathbb{R} be a differentiable scalar function, and given an index i:Ii:I, the partial derivative i\partial_{i} is pointwise defined as

i(f)(v)lim (x,y)(x,x)f(v+xe i)f(v+ye i)xy\partial_{i}(f)(v) \coloneqq \lim_{(x, y) \to (x, x)} \frac{f(v + x e_i) - f(v + y e_i)}{x - y}

See also

Revision on June 10, 2022 at 14:31:27 by Anonymous?. See the history of this page for a list of all contributions to it.