deriv.neg'
theorem deriv.neg' :
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F}, (deriv fun y => -f y) = fun x => -deriv f x
This theorem states that for any function `f` from a nontrivially normed field `𝕜` to a normed add commutative group `F` (with `𝕜` as its underlying field), the derivative of the negation function (i.e., `fun y => -f y`) is equal to the negation of the derivative of `f` itself. In mathematical notation, this can be expressed as `(d/dx)(-f) = - (d/dx)f`.
More concisely: For any function `f` from a nontrivially normed field to a normed add commutative group, the derivative of the negation function `fun y => -f y` is equal to the negative of the derivative of `f`. In mathematical notation, `(d/dx)(-f) = -(d/dx)f`.
|
HasDerivAtFilter.add
theorem HasDerivAtFilter.add :
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace 𝕜 F] {f g : 𝕜 → F} {f' g' : F} {x : 𝕜} {L : Filter 𝕜},
HasDerivAtFilter f f' x L → HasDerivAtFilter g g' x L → HasDerivAtFilter (fun y => f y + g y) (f' + g') x L
The theorem `HasDerivAtFilter.add` states that for any non-trivially normed field `𝕜`, normed additive commutative group `F` and normed space over `𝕜` and `F`, given two functions `f` and `g` from `𝕜` to `F`, their derivatives `f'` and `g'` at a point `x` along a filter `L`, if `f` has the derivative `f'` at `x` along `L` and `g` has the derivative `g'` at `x` along `L`, then the function `h` defined as `h(y) = f(y) + g(y)` has the derivative `f' + g'` at the same point `x` along the same filter `L`. In other words, it says that the derivative of the sum of two functions is the sum of their derivatives, under the given conditions.
More concisely: For any non-trivially normed field `𝕜`, normed additive commutative group `F`, and normed space over `𝕜` and `F`, if functions `f` and `g` from `𝕜` to `F` have derivatives `f'` and `g'` at a point `x` along filter `L`, then the function `h(y) = f(y) + g(y)` has derivative `f' + g'` at `x` along `L`.
|
HasDerivAt.const_add
theorem HasDerivAt.const_add :
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} (c : F),
HasDerivAt f f' x → HasDerivAt (fun x => c + f x) f' x
The theorem `HasDerivAt.const_add` asserts that if a function `f` has a derivative `f'` at a point `x` in a nontrivial normed field `𝕜` with values in a normed add commutative group `F`, then the function defined by adding a constant `c` to `f` at each point also has the same derivative `f'` at the point `x`. In other words, the derivative of a function remains unchanged even if a constant is added to the function. This is a formalization of the mathematical principle that the derivative of a constant added to a function is just the derivative of the function itself.
More concisely: If `f` is differentiable at `x` in a normed field `𝕜` with values in a normed additive commutative group `F`, then the function `g(x) = f(x) + c` is also differentiable at `x` with derivative `f'(x)`, where `c` is a constant.
|
deriv_add
theorem deriv_add :
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace 𝕜 F] {f g : 𝕜 → F} {x : 𝕜},
DifferentiableAt 𝕜 f x → DifferentiableAt 𝕜 g x → deriv (fun y => f y + g y) x = deriv f x + deriv g x
The theorem `deriv_add` states that for any point `x` in a specific type `𝕜`, and for any two functions `f` and `g` from `𝕜` to another specific type `F`, if both `f` and `g` are differentiable at the point `x`, the derivative at `x` of the sum of `f` and `g` is equal to the sum of the derivatives of `f` and `g` at `x`. Here, `𝕜` is a nontrivially normed field and `F` is a normed space over `𝕜`. The function `deriv` is used to denote the derivative of a function at a point, and the function `DifferentiableAt` indicates whether a function is differentiable at a particular point.
More concisely: If `f` and `g` are differentiable functions from a normed field `𝕜` to a normed space `F` at a point `x ∈ 𝕜`, then `(f + g).deriv x = f.deriv x + g.deriv x`.
|
HasDerivAtFilter.const_add
theorem HasDerivAtFilter.const_add :
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {L : Filter 𝕜} (c : F),
HasDerivAtFilter f f' x L → HasDerivAtFilter (fun y => c + f y) f' x L
The theorem `HasDerivAtFilter.const_add` states that for a nontrivially normed field `𝕜`, a normed additively commutative group `F`, and a normed space `𝕜 F`, if a function `f` from `𝕜` to `F` has a derivative `f'` at a point `x` along a filter `L`, then the function that adds a constant `c` to each value of `f`, also has the derivative `f'` at the same point `x` along the same filter `L`. Essentially, it demonstrates that adding a constant to a function does not change its derivative.
More concisely: If a function from a nontrivially normed field to a normed additively commutative group has a derivative at a point along a filter, then the derivative is preserved under constant addition at that point along the same filter.
|
HasStrictDerivAt.neg
theorem HasStrictDerivAt.neg :
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜},
HasStrictDerivAt f f' x → HasStrictDerivAt (fun x => -f x) (-f') x
The theorem `HasStrictDerivAt.neg` states that for any non-trivial normed field `𝕜`, any normed additive commutative group `F` and any point `x` in `𝕜`, if a function `f : 𝕜 → F` has a strict derivative `f'` at the point `x`, then the negative function `-f` has a strict derivative `-f'` at the same point `x`. In other words, the derivative of the negation of a function is the negation of the derivative of the function, at any given point, under the condition of strict differentiability.
More concisely: If `f : 𝕜 → F` is a function with strict derivative `f'` at `x` in a non-trivial normed field `𝕜` and normed additive commutative group `F`, then `-f` has strict derivative `-f'` at `x`.
|
HasStrictDerivAt.add
theorem HasStrictDerivAt.add :
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace 𝕜 F] {f g : 𝕜 → F} {f' g' : F} {x : 𝕜},
HasStrictDerivAt f f' x → HasStrictDerivAt g g' x → HasStrictDerivAt (fun y => f y + g y) (f' + g') x
This theorem states that if a function `f` has a strict derivative `f'` at a point `x` and similarly a function `g` has a strict derivative `g'` at the same point `x`, then the function formed by adding `f` and `g` has a strict derivative at `x` that is the sum of `f'` and `g'`. This describes the property of linearity of differentiation in the context of strict differentiability. In other words, the derivative of the sum of two functions at a point is equal to the sum of the derivatives of those functions at that point.
More concisely: If functions `f` and `g` have strict derivatives `f'` and `g'` at a point `x` respectively, then the function `f + g` has a strict derivative `(f + g)' = f' + g'` at `x`.
|
HasDerivAt.neg
theorem HasDerivAt.neg :
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜}, HasDerivAt f f' x → HasDerivAt (fun x => -f x) (-f') x
The theorem `HasDerivAt.neg` states that for any type `𝕜` which forms a nontrivially normed field, a type `F` which forms a normed add commutative group and also a normed space over `𝕜`, a function `f` from `𝕜` to `F`, its derivative `f'` at a point `x` in `𝕜`, if `f` has the derivative `f'` at the point `x` (that is, `f` satisfies the equation `f x' = f x + (x' - x) • f' + o(x' - x)` where `x'` converges to `x`), then the function `-f` (the negation of `f`) has the derivative `-f'` (the negation of `f'`) at the same point `x`.
More concisely: If `𝕜` is a nontrivially normed field, `F` is a normed add commutative group and normed space over `𝕜`, `f : 𝕜 → F` has derivative `f'` at `x ∈ 𝕜`, then `-f` has derivative `-f'` at `x`.
|
HasDerivAt.sub
theorem HasDerivAt.sub :
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace 𝕜 F] {f g : 𝕜 → F} {f' g' : F} {x : 𝕜},
HasDerivAt f f' x → HasDerivAt g g' x → HasDerivAt (fun x => f x - g x) (f' - g') x
The theorem `HasDerivAt.sub` states that for any type `𝕜` which forms a nontrivial normed field and any type `F` which forms a normed additively commutative group and a normed space over `𝕜`, if the function `f` has a derivative `f'` at a point `x` and the function `g` has a derivative `g'` at the same point `x`, then the function that sends `x` to `f x - g x` has a derivative `f' - g'` at the point `x`. In other words, the derivative of the difference of two functions at a point is equal to the difference of their derivatives at that point.
More concisely: If `f` and `g` are differentiable functions at point `x` in a normed additively commutative group and normed space over a nontrivial normed field, then `(f - g)'(x) = f'(x) - g'(x)`.
|
HasDerivWithinAt.sub
theorem HasDerivWithinAt.sub :
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace 𝕜 F] {f g : 𝕜 → F} {f' g' : F} {x : 𝕜} {s : Set 𝕜},
HasDerivWithinAt f f' s x → HasDerivWithinAt g g' s x → HasDerivWithinAt (fun x => f x - g x) (f' - g') s x
This theorem states that if the function `f` has a derivative `f'` at a point `x` within a subset `s`, and the function `g` has a derivative `g'` at the same point `x` within the same subset `s`, then the function `h` defined as `h(x) = f(x) - g(x)` has a derivative `h' = f' - g'` at the point `x` within the subset `s`. The space in which these functions and derivatives are taken is a normed vector space over a normed field. This theorem essentially encapsulates the linearity of differentiation in such normed spaces.
More concisely: If `f` and `g` are differentiable functions at `x` in the subset `s` of a normed vector space, then their difference `h(x) = f(x) - g(x)` is also differentiable at `x` with derivative `h'(x) = f'(x) - g'(x)`.
|
HasDerivAtFilter.neg
theorem HasDerivAtFilter.neg :
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {L : Filter 𝕜},
HasDerivAtFilter f f' x L → HasDerivAtFilter (fun x => -f x) (-f') x L
The theorem `HasDerivAtFilter.neg` asserts that for every non-trivially normed field 𝕜, normed add commutative group F, and normed space over 𝕜 and F, if a function `f` from 𝕜 to F has a derivative `f'` at a point `x` as `x` goes along the filter `L`, then the function that maps `x` to the negation of `f(x)` has the derivative `-f'` at the same point `x` along the same filter `L`. This means that negating a function negates its derivative at any given point.
More concisely: For any non-trivially normed field 𝕜, normed add commutative group F, and normed space over 𝕜 and F, if a function `f` from 𝕜 to F has a derivative `f'` at point `x` along filter `L`, then `-f` has derivative `-f'` at `x` along `L`.
|
deriv_sub
theorem deriv_sub :
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace 𝕜 F] {f g : 𝕜 → F} {x : 𝕜},
DifferentiableAt 𝕜 f x → DifferentiableAt 𝕜 g x → deriv (fun y => f y - g y) x = deriv f x - deriv g x
The theorem `deriv_sub` states that for any two functions `f` and `g` that are differentiable at a point `x`, in a normed space over a nontrivially normed field `𝕜`, the derivative at `x` of the difference of `f` and `g` is equal to the difference of the derivatives at `x` of `f` and `g` respectively. In mathematical terms, this can be written as: if `f` and `g` are differentiable at `x`, then `(f - g)'(x) = f'(x) - g'(x)`.
More concisely: The derivative of the difference of two differentiable functions is equal to the difference of their derivatives.
|
hasDerivAtFilter_neg
theorem hasDerivAtFilter_neg :
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (x : 𝕜) (L : Filter 𝕜), HasDerivAtFilter Neg.neg (-1) x L := by
sorry
The theorem `hasDerivAtFilter_neg` states that for all types `𝕜` that are nontrivially normed fields, for any element `x : 𝕜` and any filter `L` over `𝕜`, the negative function (which computes the negative or opposite of its argument) has a derivative of `-1` at the point `x` along the filter `L`. In mathematical terms, this means that the derivative of the function `f(x) = -x` is `f'(x) = -1` for all `x` in the field.
More concisely: For any nontrivially normed field `𝕜` and element `x` in `𝕜`, the negative function `f(x) = -x` has a derivative of `-1` along any filter over `𝕜`.
|
HasDerivAtFilter.add_const
theorem HasDerivAtFilter.add_const :
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {L : Filter 𝕜},
HasDerivAtFilter f f' x L → ∀ (c : F), HasDerivAtFilter (fun y => f y + c) f' x L
The theorem `HasDerivAtFilter.add_const` states that for any function `f` from a nontrivially normed field `𝕜` to a normed add commutative group `F` (with the associated normed space structure), if `f` has a derivative `f'` at a point `x` with respect to a filter `L`, then addition of a constant `c` from `F` to the function (i.e., the function `g` defined as `g(y) = f(y) + c`) does not change the derivative at that point with respect to the same filter. In other words, the derivative of the sum of a function and a constant is the same as the derivative of the original function with respect to the same point and filter.
More concisely: If a function from a nontrivially normed field to a normed add commutative group has a derivative at a point with respect to a filter, then the derivative of the function at that point with respect to the filter is equal to the derivative of the function's constant addition to it.
|
hasDerivAt_neg
theorem hasDerivAt_neg : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (x : 𝕜), HasDerivAt Neg.neg (-1) x := by
sorry
The theorem `hasDerivAt_neg` states that, for every point `x` in a nontrivially normed field `𝕜`, the function `Neg.neg`, which computes the negative or opposite of a number, has a derivative of `-1` at that point. This means that if we look at the change in the `Neg.neg` function as we infinitesimally move away from `x`, this change is proportional to `-1`, i.e., the function is decreasing at a constant rate.
More concisely: The negative function `Neg.neg` has a derivative of `-1` in the nontrivially normed field `𝕜`.
|