HasDerivAt.mul
theorem HasDerivAt.mul :
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝔸 : Type u_3} [inst_1 : NormedRing 𝔸]
[inst_2 : NormedAlgebra 𝕜 𝔸] {c d : 𝕜 → 𝔸} {c' d' : 𝔸},
HasDerivAt c c' x → HasDerivAt d d' x → HasDerivAt (fun y => c y * d y) (c' * d x + c x * d') x
This theorem, `HasDerivAt.mul`, states that for any type `𝕜` which is a non-trivially normed field and any type `𝔸` which is a normed ring and also a normed algebra over `𝕜`, given two functions `c, d` from `𝕜` to `𝔸` and their respective derivatives `c'` and `d'` at a point `x` in `𝕜`, if `c` has derivative `c'` at `x` and `d` has derivative `d'` at `x`, then the derivative at `x` of the function that maps `y` to the product of `c y` and `d y`, is `(c' * d x) + (c x * d')`.
In mathematical terms, if we have two functions `c` and `d` differentiable at point `x`, then the derivative of the function `f(y) = c(y) * d(y)` at point `x` is given by the Leibniz product rule: `f'(x) = c'(x) * d(x) + c(x) * d'(x)`.
More concisely: Given two differentiable functions $c$ and $d$ from a normed field $ℝ$ to a normed ring and algebra $𝔸$ over $ℝ$, the derivative of their product function $f(y) = c(y) \cdot d(y)$ at a point $x$ is given by the Leibniz product rule: $f'(x) = c'(x) \cdot d(x) + c(x) \cdot d'(x)$.
|
HasDerivAt.div_const
theorem HasDerivAt.div_const :
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_2} [inst_1 : NontriviallyNormedField 𝕜']
[inst_2 : NormedAlgebra 𝕜 𝕜'] {c : 𝕜 → 𝕜'} {c' : 𝕜'},
HasDerivAt c c' x → ∀ (d : 𝕜'), HasDerivAt (fun x => c x / d) (c' / d) x
The theorem `HasDerivAt.div_const` states that for any nontrivially normed fields `𝕜` and `𝕜'` where `𝕜'` is a normed algebra over `𝕜`, given a function `c` from `𝕜` to `𝕜'`, and a point `x` in `𝕜`, if `c` has a derivative `c'` at the point `x`, then for any constant `d` in `𝕜'`, the function defined by `c x / d` has the derivative `c' / d` at the point `x`.
In other words, this theorem is stating the rule that the derivative of a function divided by a constant is the derivative of the original function divided by that constant.
More concisely: If a function from a nontrivially normed field to a normed algebra over that field has a derivative at a point, then the derivative of the function evaluated at that point divided by a constant is equal to the quotient of the derivative and the constant.
|
HasDerivAt.mul_const
theorem HasDerivAt.mul_const :
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝔸 : Type u_3} [inst_1 : NormedRing 𝔸]
[inst_2 : NormedAlgebra 𝕜 𝔸] {c : 𝕜 → 𝔸} {c' : 𝔸},
HasDerivAt c c' x → ∀ (d : 𝔸), HasDerivAt (fun y => c y * d) (c' * d) x
This theorem states that if a function `c` has a derivative `c'` at a point `x` in a nontrivially normed field `𝕜`, then for any element `d` of a normed ring `𝔸`, which is also a normed algebra over `𝕜`, the function that maps `y` to `c y * d` has a derivative of `c' * d` at that point `x`. In other words, it is the rule for differentiation of a function multiplied by a constant, generalised to normed fields and normed algebras.
More concisely: If `c` is differentiable at `x` in a nontrivially normed field `𝕜`, then the function `y ↦ c(y) * d` is differentiable at `x` in the normed algebra `𝔸` over `𝕜`, with derivative `c'(x) * d`.
|
HasDerivWithinAt.mul_const
theorem HasDerivWithinAt.mul_const :
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝔸 : Type u_3} [inst_1 : NormedRing 𝔸]
[inst_2 : NormedAlgebra 𝕜 𝔸] {c : 𝕜 → 𝔸} {c' : 𝔸},
HasDerivWithinAt c c' s x → ∀ (d : 𝔸), HasDerivWithinAt (fun y => c y * d) (c' * d) s x
The theorem `HasDerivWithinAt.mul_const` states that for any type `𝕜` which forms a nontrivial normed field, a point `x` of type `𝕜`, a set `s` of elements of type `𝕜`, another type `𝔸` which forms a normed ring, and a normed algebra over `𝕜`, a function `c` from `𝕜` to `𝔸`, its derivative `c'` at the point `x` within the subset `s`, and an element `d` of type `𝔸` — if `c` has the derivative `c'` at the point `x` within the subset `s`, then the function obtained by multiplying `c` by the constant `d` has the derivative `c' * d` at the point `x` within the subset `s`. In mathematical terms, it tells us that the derivative of the function `c(y) * d` (where `d` is a constant) with respect to `y` at the point `x` within `s` equals `c'(x) * d`.
More concisely: If `c:` 𝕜 → 𝔸 is differentiable at `x` ∈ 𝕜 with respect to a subset `s` of 𝕜, then the function `d => c(x) * d:` 𝔸 → 𝔸 is differentiable at `x` with respect to `s` and has derivative `c'(x) * d`.
|
deriv_mul_const_field
theorem deriv_mul_const_field :
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_2} [inst_1 : NormedField 𝕜']
[inst_2 : NormedAlgebra 𝕜 𝕜'] {u : 𝕜 → 𝕜'} (v : 𝕜'), deriv (fun y => u y * v) x = deriv u x * v
The theorem `deriv_mul_const_field` states that for any point `x` in a non-trivially normed field `𝕜`, and a function `u` from `𝕜` to another normed field `𝕜'` with a normed algebra structure over `𝕜`, the derivative at `x` of the function which multiplies `u` by a constant from `𝕜'` is equal to the product of the derivative of `u` at `x` and the constant. In mathematical terms, if we denote the derivative operation as `deriv`, the theorem states that: `deriv (λy . u(y) * v) x = deriv u(x) * v`.
More concisely: The derivative of the multiplication of a function and a constant, both defined over a non-trivially normed field, is equal to the product of the function's derivative and the constant.
|
HasDerivAt.const_mul
theorem HasDerivAt.const_mul :
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝔸 : Type u_3} [inst_1 : NormedRing 𝔸]
[inst_2 : NormedAlgebra 𝕜 𝔸] {d : 𝕜 → 𝔸} {d' : 𝔸} (c : 𝔸),
HasDerivAt d d' x → HasDerivAt (fun y => c * d y) (c * d') x
The theorem `HasDerivAt.const_mul` states that for any non-trivially normed field `𝕜`, any point `x` in `𝕜`, a normed ring `𝔸`, a normed algebra `𝕜 𝔸`, a function `d : 𝕜 → 𝔸`, its derivative `d' : 𝔸` at `x`, and a constant `c : 𝔸`, if `d` has the derivative `d'` at the point `x`, then the function `fun y => c * d y`, which is the multiplication of the function `d` by the constant `c`, has the derivative `c * d'` at the point `x`. This theorem essentially captures the rule of constants in differentiation, which states that the derivative of a constant times a function is equal to the constant times the derivative of the function.
More concisely: If `d : ℝ→ℝ^n` is differentiable at `x ∈ ℝ` and `c ∈ ℝ`, then the function `f : ℝ→ℝ^n` defined by `f(y) := c * d(y)` is differentiable at `x` and has derivative `f'(x) = c * d'(x)`.
|
deriv_mul
theorem deriv_mul :
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝔸 : Type u_3} [inst_1 : NormedRing 𝔸]
[inst_2 : NormedAlgebra 𝕜 𝔸] {c d : 𝕜 → 𝔸},
DifferentiableAt 𝕜 c x →
DifferentiableAt 𝕜 d x → deriv (fun y => c y * d y) x = deriv c x * d x + c x * deriv d x
The `deriv_mul` theorem states that for any non-trivial normed field `𝕜`, any point `x` in `𝕜`, any normed ring `𝔸` over `𝕜`, and any two functions `c` and `d` from `𝕜` to `𝔸`, if `c` and `d` are both differentiable at `x`, then the derivative at `x` of the function defined by multiplying `c` and `d` is equal to the product of the derivative of `c` at `x` and the value of `d` at `x`, plus the product of the value of `c` at `x` and the derivative of `d` at `x`. Essentially, this theorem is a formalization of the product rule from calculus in the context of differentiable functions on normed algebra.
More concisely: For any non-trivial normed field `𝕜`, any point `x` in `𝕜`, and normed rings `𝔸` over `𝕜`, if functions `c` and `d` from `𝕜` to `𝔸` are differentiable at `x`, then `(dc/dx)(x) * d(x) = c(x) * (dd/dx)(x)`.
|
HasDerivWithinAt.smul
theorem HasDerivWithinAt.smul :
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_2}
[inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜'] [inst_5 : NormedSpace 𝕜' F]
[inst_6 : IsScalarTower 𝕜 𝕜' F] {c : 𝕜 → 𝕜'} {c' : 𝕜'},
HasDerivWithinAt c c' s x →
HasDerivWithinAt f f' s x → HasDerivWithinAt (fun y => c y • f y) (c x • f' + c' • f x) s x
This theorem states that the derivative of a function, that is the product of two functions, within a given subset can be calculated if the derivatives of the individual functions within the same subset are known. More specifically, if `c` is a function from `𝕜` to `𝕜'` with derivative `c'` at a point `x` within a set `s`, and `f` is a function from `𝕜` to `F` with derivative `f'` at the same point `x` within the same set `s`, then the derivative of the function `(c y) * (f y)` at the point `x` within the set `s` is `(c x) * f' + c' * (f x)`. Here, `𝕜`, `𝕜'` and `F` are types over which certain algebraic structures like normed fields, normed add comm groups and normed spaces are defined, and `IsScalarTower 𝕜 𝕜' F` means that the scalar multiplication operations in these structures are compatible with each other.
More concisely: If `c` and `f` are functions with derivatives `c'` and `f'` in the set `s` of a normed field `𝕜`, `𝕜'`, and `F` with compatible scalars, then the derivative of the product `(c ∘ y) * (f ∘ y)` at `x` in `s` is `(c x) * f' + c' * (f x)`.
|