DifferentiableWithinAt.sub_const
theorem DifferentiableWithinAt.sub_const :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{x : E} {s : Set E},
DifferentiableWithinAt π f s x β β (c : F), DifferentiableWithinAt π (fun y => f y - c) s x
The theorem `DifferentiableWithinAt.sub_const` states that for any non-trivially normed field `π`, normed additive commutative group `E`, normed space `π E`, normed additive commutative group `F`, normed space `π F`, function `f` from `E` to `F`, point `x` in `E`, and subset `s` of `E`, if the function `f` is differentiable at the point `x` within the set `s`, then for any element `c` in `F`, the function `f(y) - c` is also differentiable at the point `x` within the set `s`. In simple terms, the theorem states that the difference between a differentiable function and a constant is also differentiable.
More concisely: If a function is differentiable at a point in a normed space with respect to a subset, then the difference of the function and a constant is also differentiable at that point with respect to the same subset.
|
DifferentiableAt.add
theorem DifferentiableAt.add :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f g : E β F}
{x : E}, DifferentiableAt π f x β DifferentiableAt π g x β DifferentiableAt π (fun y => f y + g y) x
The theorem `DifferentiableAt.add` states that if we have two functions `f` and `g` from `E` to `F` that are both differentiable at a point `x`, then the function that is the pointwise sum of `f` and `g` is also differentiable at `x`. Here, `E` and `F` are normed additively commutative groups over a nontrivially normed field `π`. The pointwise sum of `f` and `g` is the function that at any `y` in `E` returns the sum of `f y` and `g y` in `F`.
More concisely: If functions `f` and `g` are differentiable at point `x` in the normed additively commutative groups `E` and `F` over a nontrivially normed field `π`, then their pointwise sum `f + g` is differentiable at `x`.
|
HasFDerivAtFilter.neg
theorem HasFDerivAtFilter.neg :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{f' : E βL[π] F} {x : E} {L : Filter E},
HasFDerivAtFilter f f' x L β HasFDerivAtFilter (fun x => -f x) (-f') x L
This theorem states that for any nontrivially normed field `π`, normed additive commutative groups `E` and `F`, which are also normed spaces over the field `π`, and any function `f : E β F` with a continuous linear derivative `f'` at a point `x` under a filter `L`, the function obtained by negating `f` also has a continuous linear derivative, which is the negation of `f'`, at the same point `x` under the same filter `L`. In other words, the derivative of the negation of a function is the negation of the derivative of the original function.
More concisely: If `f : E β F` is a continuously differentiable function between normed spaces over a nontrivially normed field, then `(βf)' = β(f)'` at a point `x` under filter `L`.
|
DifferentiableWithinAt.sub
theorem DifferentiableWithinAt.sub :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f g : E β F}
{x : E} {s : Set E},
DifferentiableWithinAt π f s x β
DifferentiableWithinAt π g s x β DifferentiableWithinAt π (fun y => f y - g y) s x
The theorem `DifferentiableWithinAt.sub` states that, for all types `π`, `E`, and `F` where `π` is a nontrivially normed field, `E` is a normed additive commutative group, and `F` is a normed additive commutative group with `E` and `F` being normed spaces over `π`, if you have two functions `f` and `g` from `E` to `F`, a point `x` in `E`, and a set `s` of `E`, then if `f` and `g` are differentiable at the point `x` within the set `s`, then the function that subtracts the outputs of `g` from `f` (i.e., `f y - g y` for all `y` in `E`) is also differentiable at the point `x` within the set `s`.
More concisely: If `f` and `g` are differentiable at `x` within the set `s` in the normed spaces `E` and `F` over a nontrivially normed field `π`, then the function `f - g` is differentiable at `x` within `s`.
|
DifferentiableAt.add_const
theorem DifferentiableAt.add_const :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{x : E}, DifferentiableAt π f x β β (c : F), DifferentiableAt π (fun y => f y + c) x
The theorem `DifferentiableAt.add_const` states that given any nontrivial normed field `π`, normed additive commutative groups `E` and `F` that are also normed spaces over `π`, a function `f` from `E` to `F`, a point `x` in `E`, and a constant `c` in `F`, if `f` is differentiable at `x`, then the function obtained by adding the constant `c` to `f` at every point (i.e., `(fun y => f y + c)`) is also differentiable at `x`. This theorem is a formalisation of the fact that the derivative of a constant-added function is the same as the derivative of the original function.
More concisely: If `f` is differentiable at `x` in the normed space `E` over the field `π`, then the function `(y => f y + c)` is differentiable at `x` in `E` for any constant `c` in the normed space `F`.
|
HasFDerivWithinAt.neg
theorem HasFDerivWithinAt.neg :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{f' : E βL[π] F} {x : E} {s : Set E}, HasFDerivWithinAt f f' s x β HasFDerivWithinAt (fun x => -f x) (-f') s x
This theorem states that for any nontrivially normed field `π`, normed additive commutative groups `E` and `F`, and normed spaces `E` over `π` and `F` over `π`, if a function `f : E β F` has a Frechet derivative `f'` at a point `x` within a set `s` of `E`, then the negation function `(fun x => -f x)` also has a Frechet derivative which is the negation of `f'` within the same set `s` at the same point `x`. In the language of calculus, if a function has a derivative at a point within a set, then the derivative of the negative of the function at that point is the negative of the original derivative.
More concisely: If `f : E β F` has a Frechet derivative `f'` at `x` in `s` in a nontrivially normed field `π`, then `-f` has a Frechet derivative `-f'` at `x` in `s`.
|
HasStrictFDerivAt.add
theorem HasStrictFDerivAt.add :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f g : E β F}
{f' g' : E βL[π] F} {x : E},
HasStrictFDerivAt f f' x β HasStrictFDerivAt g g' x β HasStrictFDerivAt (fun y => f y + g y) (f' + g') x
The theorem `HasStrictFDerivAt.add` states that if we have two functions `f` and `g` from a normed add commutative group `E` to another normed add commutative group `F`, over a nontrivially normed field `π`, and if both `f` and `g` have strict Frechet derivatives (`f'` and `g'` respectively) at a point `x` in `E`, then the sum of the functions `f` and `g` also has a strict Frechet derivative at `x`, and its derivative is the sum of `f'` and `g'`.
More concisely: If functions `f` and `g` from a normed add commutative group `E` to another normed add commutative group `F` over a nontrivially normed field have strict Frechet derivatives `f'` and `g'` at a point `x` in `E`, then the function `f + g` has a strict Frechet derivative `f' + g'` at `x`.
|
fderivWithin_add_const
theorem fderivWithin_add_const :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{x : E} {s : Set E},
UniqueDiffWithinAt π s x β β (c : F), fderivWithin π (fun y => f y + c) s x = fderivWithin π f s x
The theorem `fderivWithin_add_const` states that for a nontrivially normed field `π`, a function `f` mapping from a normed additive commutative group `E` to another normed additive commutative group `F` (both `E` and `F` being normed spaces over `π`), a set `s` of elements of type `E`, and an element `x` of type `E`, if `x` is uniquely differentiable within `s`, then the derivative within `s` at `x` of the function `f` added to a constant `c` is the same as the derivative within `s` at `x` of the function `f` itself. This essentially means that adding a constant to a function does not affect its derivative within a set at a point, if the point is uniquely differentiable within the set.
More concisely: If `f : E β F` is a function between normed additive commutative groups over a nontrivially normed field, `x β E` is uniquely differentiable within a set `s β E`, then `(DF at x : E β F) (x + c) = DF at x` for all `c β π`.
|
fderiv_add_const
theorem fderiv_add_const :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{x : E} (c : F), fderiv π (fun y => f y + c) x = fderiv π f x
The theorem `fderiv_add_const` states that for any non-trivially normed field `π`, any normed additive commutative groups `E` and `F` which are also normed spaces over `π`, any function `f` from `E` to `F`, any element `x` of `E`, and any constant `c` of `F`, the FrΓ©chet derivative at `x` of the function `y` mapping to `f(y) + c` is equal to the FrΓ©chet derivative at `x` of the function `f`. In simpler terms, adding a constant to a function does not change its derivative.
More concisely: The FrΓ©chet derivative of the constant function `c => f(x) + c` is equal to the FrΓ©chet derivative of `f` at `x`, for any normed field `π`, normed additive commutative groups `E` and `F` over `π`, function `f` from `E` to `F`, and element `x` of `E`.
|
HasFDerivAtFilter.const_add
theorem HasFDerivAtFilter.const_add :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{f' : E βL[π] F} {x : E} {L : Filter E},
HasFDerivAtFilter f f' x L β β (c : F), HasFDerivAtFilter (fun y => c + f y) f' x L
The theorem `HasFDerivAtFilter.const_add` states that for any nontrivially normed field `π`, normed additive commutative groups `E` and `F`, and normed spaces over `π` for both `E` and `F`, if the function `f` from `E` to `F` has a Frechet derivative `f'` at a point `x` with respect to a filter `L`, then for any constant `c` in `F`, the function that adds `c` to `f(y)` for every `y` in `E` also has the same derivative `f'` at `x` with respect to the filter `L`.
In simpler terms, it states that the derivative of a function `f` is unaffected by adding a constant to the function, similar to the well-known property in calculus that the derivative of a function plus a constant is simply the derivative of the original function.
More concisely: If a function `f` from a normed space `E` to another normed space `F` over a nontrivially normed field `π` has a Frechet derivative `f'` at `x` with respect to a filter `L`, then the function `g(y) = f(y) + c` (for any constant `c` in `F`) also has derivative `f'` at `x` with respect to `L`.
|
DifferentiableWithinAt.neg
theorem DifferentiableWithinAt.neg :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{x : E} {s : Set E}, DifferentiableWithinAt π f s x β DifferentiableWithinAt π (fun y => -f y) s x
This theorem, `DifferentiableWithinAt.neg`, states that for every function `f` which is differentiable at a point `x` within a set `s` in a normed field `π`, the negated function `-f` is also differentiable at the same point `x` within the same set `s`. Specifically, the normed field `π`, the normed space `E` for the domain of `f`, and the normed space `F` for the codomain of `f` need to be nontrivial with a normed additive commutative group structure. In mathematical terms, if `f` is differentiable at a point `x` in a set `s`, then `-f` is also differentiable at `x` in `s`.
More concisely: If `f` is differentiable at a point `x` in a normed set `s` of a normed field `π`, then the negated function `-f` is also differentiable at `x` in `s`.
|
DifferentiableAt.sub_const
theorem DifferentiableAt.sub_const :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{x : E}, DifferentiableAt π f x β β (c : F), DifferentiableAt π (fun y => f y - c) x
The theorem `DifferentiableAt.sub_const` says that for all types π, E, and F, where π is a non-trivially normed field, E is a normed add commutative group over π, and F is also a normed add commutative group over π, if a function f from E to F is differentiable at a point x in E, then the function obtained by subtracting a constant c from f is also differentiable at the same point x. This theorem establishes that the differentiability property is preserved under subtraction of a constant.
More concisely: If a function f : ββ€x, β is differentiable at x, then the function g(x) = f(x) - c is differentiable at x for any constant c.
|
HasFDerivAtFilter.add
theorem HasFDerivAtFilter.add :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f g : E β F}
{f' g' : E βL[π] F} {x : E} {L : Filter E},
HasFDerivAtFilter f f' x L β HasFDerivAtFilter g g' x L β HasFDerivAtFilter (fun y => f y + g y) (f' + g') x L
This theorem states that if we have two functions `f` and `g` from a normed additivity commutative group `E` to another such group `F` (both over a non-trivially normed field `π`), and if `f` has a derivative `f'` at a point `x` with respect to a filter `L` and `g` has a derivative `g'` at the same point with respect to the same filter, then the function defined by the sum of `f` and `g` has a derivative at `x` with respect to `L`, which is the sum of the derivatives `f'` and `g'`. This encapsulates the rule of differentiation that the derivative of the sum of two functions is the sum of their derivatives.
More concisely: If `f` and `g` are differentiable functions from a normed additive commutative group `E` to another such group `F` over a non-trivially normed field `π`, then the sum `f + g` is differentiable at a point `x` with respect to a filter `L` if and only if both `f` and `g` are, and the derivative of their sum is the sum of their derivatives: `(f + g)'(x) = f'(x) + g'(x)`.
|
HasFDerivAt.const_smul
theorem HasFDerivAt.const_smul :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{f' : E βL[π] F} {x : E} {R : Type u_6} [inst_5 : Semiring R] [inst_6 : Module R F] [inst_7 : SMulCommClass π R F]
[inst_8 : ContinuousConstSMul R F], HasFDerivAt f f' x β β (c : R), HasFDerivAt (fun x => c β’ f x) (c β’ f') x
The theorem `HasFDerivAt.const_smul` establishes that the derivative of a function scaled by a constant is just the derivative of the original function scaled by the same constant. More formally, given a function `f` that has a derivative `f'` at a point `x` in a normed field `π` and a semiring `R` such that `F` is an `R`-module and scalar multiplication by `π` commutes with scalar multiplication by `R`, the derivative at `x` of the function `c β’ f`, where `c` is a constant from `R`, is `c β’ f'`. Here `β’` denotes scalar multiplication. This is a generalization of the familiar rule from single-variable calculus that the derivative of a constant times a function is the constant times the derivative of the function.
More concisely: Given a function `f` with derivative `f'` at `x` in a normed field `π`, and an `R`-module `F` over a semiring `R` with commuting scalar multiplications, the derivative at `x` of the constant `c` times the function `f` is `c` times the derivative `f'`.
|
DifferentiableOn.neg
theorem DifferentiableOn.neg :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{s : Set E}, DifferentiableOn π f s β DifferentiableOn π (fun y => -f y) s
This theorem states that if a function `f` is differentiable on a set `s`, then the negation of the function, i.e., the function that maps each point in `s` to the negation of the corresponding value of `f`, is also differentiable on `s`. Here, `f` is a function from a normed space `E` to another normed space `F`, both over a nontrivial normed field `π`. The concept of differentiability used here is 'differentiability within a set at a point', which means roughly that the function behaves near each point of the set as a linear map plus a small error term.
More concisely: If `f : E β F` is differentiable on a set `s β E`, then the negation of `f`, i.e., `-f`, is also differentiable on `s`.
|
DifferentiableWithinAt.add_const
theorem DifferentiableWithinAt.add_const :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{x : E} {s : Set E},
DifferentiableWithinAt π f s x β β (c : F), DifferentiableWithinAt π (fun y => f y + c) s x
The theorem `DifferentiableWithinAt.add_const` states that for all types `π` with an instance of a non-trivially normed field, all types `E` and `F` with instances of a normed additive commutative group and a normed space over `π`, any function `f` from `E` to `F`, any point `x` of type `E`, and any set `s` of elements of type `E`, if the function `f` is differentiable at the point `x` within the set `s`, then for any constant `c` of type `F`, the function `(fun y => f y + c)`, which adds the constant `c` to the value of `f` at any point `y`, is also differentiable at the point `x` within the set `s`. In short, this theorem guarantees that adding a constant to a differentiable function does not affect its differentiability.
More concisely: If a function is differentiable at a point within a set, then the constant-added version of the function is also differentiable at that point within the same set.
|
DifferentiableAt.sub
theorem DifferentiableAt.sub :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f g : E β F}
{x : E}, DifferentiableAt π f x β DifferentiableAt π g x β DifferentiableAt π (fun y => f y - g y) x
The theorem `DifferentiableAt.sub` states that for any nontrivially normed field `π`, as well as any normed additive commutative groups `E` and `F` that are also normed spaces over `π`, if a function `f` from `E` to `F` is differentiable at a point `x` in `E` and another function `g` from `E` to `F` is also differentiable at the same point `x`, then the function that maps any point `y` in `E` to the difference of `f(y)` and `g(y)` is also differentiable at `x`. In other words, the difference of two differentiable functions is itself differentiable at the same point.
More concisely: If two differentiable functions from a nontrivially normed additive commutative group into another normed space over the same field are given, then their difference is also differentiable at any common point.
|
HasFDerivAtFilter.add_const
theorem HasFDerivAtFilter.add_const :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{f' : E βL[π] F} {x : E} {L : Filter E},
HasFDerivAtFilter f f' x L β β (c : F), HasFDerivAtFilter (fun y => f y + c) f' x L
The theorem `HasFDerivAtFilter.add_const` states that for a given function `f` from a normed additive commutative group `E` to another normed additive commutative group `F` over a non-trivial normed field `π`, if the function `f` has a FrΓ©chet derivative `f'` at a point `x` with respect to a filter `L`, then for any constant `c` from `F`, the function `g` defined as `g(y) = f(y) + c` also has the same FrΓ©chet derivative `f'` at the same point `x` with respect to the same filter `L`. This theorem essentially says that adding a constant to a function does not change its derivative.
More concisely: If a function `f : E β F` from a normed additive commutative group `E` to another normed additive commutative group `F` over a non-trivial normed field `π` has a FrΓ©chet derivative `f'` at `x β E` with respect to filter `L`, then the function `g(y) = f(y) + c` also has the same FrΓ©chet derivative `f'` at `x` with respect to `L`, for any constant `c β F`.
|