dslope_of_ne
theorem dslope_of_ne :
โ {๐ : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField ๐] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] {a b : ๐} (f : ๐ โ E), b โ a โ dslope f a b = slope f a b
The theorem `dslope_of_ne` states that for any nontrivially normed field `๐`, normed add commutative group `E`, and normed space over `๐` and `E`, given two elements `a` and `b` of `๐` and a function `f` from `๐` to `E`, if `b` is not equal to `a`, then the directional slope `dslope` of the function `f` at points `a` and `b` is equal to the slope of `f` on the interval `[a, b]`. In other words, when `a` and `b` are distinct, the directional slope and the slope coincide.
More concisely: For any nontrivially normed field `๐`, normed add commutative group `E`, and normed space over `๐` and `E`, if `f` is a function from `๐` to `E`, `a` and `b` are distinct elements of `๐`, then `dslope(f, a, b) = slope(f, [a, b])`.
|
DifferentiableWithinAt.of_dslope
theorem DifferentiableWithinAt.of_dslope :
โ {๐ : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField ๐] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] {f : ๐ โ E} {a b : ๐} {s : Set ๐},
DifferentiableWithinAt ๐ (dslope f a) s b โ DifferentiableWithinAt ๐ f s b
This theorem states that for any non-trivially normed field `๐`, any normed additive commutative group `E`, any function `f` from `๐` to `E`, any points `a` and `b` in `๐`, and any set `s` of `๐`, if the function `dslope f a` is differentiable at point `b` within set `s`, then the original function `f` is also differentiable at point `b` within the same set `s`. In other words, differentiability of the derivative slope function at a certain point within a certain set implies the differentiability of the original function at the same point within the same set.
More concisely: If the derivative slope function of a continuous function from a normed field to a normed additive commutative group is differentiable at a point within a set, then the original function is also differentiable at that point within the same set.
|
dslope_same
theorem dslope_same :
โ {๐ : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField ๐] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] (f : ๐ โ E) (a : ๐), dslope f a a = deriv f a
The theorem `dslope_same` states that for any function `f` from a nontrivially normed field `๐` to a normed add commutative group `E` over `๐`, the `dslope` of `f` at any point `a` in `๐` when both slope points are the same (i.e., `dslope f a a`) is equal to the derivative of `f` at that point `a` (`deriv f a`). In other words, the `dslope` function coincides with derivative where the two input points are the same.
More concisely: For any function from a nontrivially normed field to a normed add commutative group, the `dslope` is equal to the derivative at a point when both slope points are the same.
|
eqOn_dslope_slope
theorem eqOn_dslope_slope :
โ {๐ : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField ๐] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] (f : ๐ โ E) (a : ๐), Set.EqOn (dslope f a) (slope f a) {a}แถ
The theorem `eqOn_dslope_slope` states that for any non-trivial normed field `๐`, a normed add commutative group `E`, a normed space over `๐` and `E`, and a function `f` mapping from `๐` to `E`, the functions `dslope` and `slope` of `f` at a point `a` are equal on the complement of the set `{a}`. In other words, except at the point `a`, the slope of the function `f` on the interval `[a, b]` equals to the derivative of `f` at `a` when `a = b`, and equals to `(b - a)โปยน โข (f b - f a)` when `a โ b`.
More concisely: For any non-trivial normed field `๐`, normed add commutative group `E`, and function `f` from `๐` to `E`, the functions `dslope` and `slope` of `f` agree on the complement of the singleton set containing any point `a` in `๐`, where `dslope` is the difference quotient and `slope` is the derivative.
|