HasDerivAt.comp_const_add
theorem HasDerivAt.comp_const_add :
โ {๐ : Type u_1} [inst : NontriviallyNormedField ๐] (a x : ๐) {๐' : Type u_2} [inst_1 : NormedAddCommGroup ๐']
[inst_2 : NormedSpace ๐ ๐'] {h : ๐ โ ๐'} {h' : ๐'},
HasDerivAt h h' (a + x) โ HasDerivAt (fun x => h (a + x)) h' x
This theorem states that adding a constant to the argument of a function does not change the derivative of the function. Concretely, given a function `h : ๐ โ ๐'` with derivative `h'` at the point `a + x`, where `a` and `x` are scalars in a nontrivial normed field `๐`, and `๐'` is a normed additive commutative group with a normed space structure over `๐`, the derivative of the translated function `(fun x => h (a + x))` at the point `x` is also `h'`. In mathematical terms, if `h` has a derivative `h'` at `a + x`, then the derivative of `h(a + x)` with respect to `x` is `h'`.
More concisely: The derivative of the function `h` at `a + x` is equal to the derivative of the translated function `x โฆ h(a + x)` at `x`.
|
HasDerivAt.comp_add_const
theorem HasDerivAt.comp_add_const :
โ {๐ : Type u_1} [inst : NontriviallyNormedField ๐] (x a : ๐) {๐' : Type u_2} [inst_1 : NormedAddCommGroup ๐']
[inst_2 : NormedSpace ๐ ๐'] {h : ๐ โ ๐'} {h' : ๐'},
HasDerivAt h h' (x + a) โ HasDerivAt (fun x => h (x + a)) h' x
The theorem `HasDerivAt.comp_add_const` states that for any non-trivially normed field `๐`, any elements `x` and `a` of `๐`, any normed add commutative group `๐'` over `๐`, any function `h` from `๐` to `๐'`, and any element `h'` of `๐'`, if `h` has derivative `h'` at the point `x + a`, then the function `h` composed with the addition of `a` also has the derivative `h'` at the point `x`. In other words, translating the input of a function by a constant does not change its derivative.
More concisely: If `h` is a differentiable function from a normed field `๐` to a normed add commutative group `๐'` over `๐`, then `h โ (x โฆ x + a)` is also differentiable at `x`, with derivative `h'` for any `x โ ๐` and `a โ ๐`.
|