DifferentiableWithinAt.pow
theorem DifferentiableWithinAt.pow :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {𝔸 : Type u_6} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸]
{a : E → 𝔸}, DifferentiableWithinAt 𝕜 a s x → ∀ (n : ℕ), DifferentiableWithinAt 𝕜 (fun x => a x ^ n) s x
The theorem `DifferentiableWithinAt.pow` states that for any nontrivially normed field `𝕜`, normed addative commutative group `E`, normed ring `𝔸`, normed algebra of `𝕜` and `𝔸`, and set `s` of `E`, if a function `a` from `E` to `𝔸` is differentiable at a point `x` within `s`, then the function obtained by raising `a(x)` to the power `n` (for any natural number `n`), is also differentiable at `x` within `s`. The theorem represents the property that the power function preserves differentiability under certain conditions.
More concisely: If `a: E -> 𝔸` is differentiable at `x` in the normed additive commutative group `E`, then the function `b(y) = a(y)^n` is differentiable at `x` in `E` for any natural number `n`.
|
DifferentiableWithinAt.smul
theorem DifferentiableWithinAt.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}
{x : E} {s : Set E} {𝕜' : Type u_6} [inst_5 : NontriviallyNormedField 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜']
[inst_7 : NormedSpace 𝕜' F] [inst_8 : IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'},
DifferentiableWithinAt 𝕜 c s x →
DifferentiableWithinAt 𝕜 f s x → DifferentiableWithinAt 𝕜 (fun y => c y • f y) s x
The theorem `DifferentiableWithinAt.smul` states that for every non-trivially normed field `𝕜`, every normed additively commutative group `E` and `F` (which are also normed spaces over `𝕜`), every function `f` from `E` to `F`, every point `x` in `E`, and every set `s` of `E`, if `c` is a scalar field over `E`, and both `c` and `f` are differentiable at `x` within `s`, then the function which maps `y` in `E` to the scalar product of `c(y)` and `f(y)` is also differentiable at `x` within `s`. Here, `𝕜'` is a non-trivially normed field that is a normed algebra over `𝕜` and `F` is a normed space over `𝕜'`, with `𝕜` being a scalar tower over `𝕜'` and `F`.
More concisely: Given a non-trivially normed field `𝕜`, a normed additively commutative group `E` and `F` over `𝕜` (with `F` a normed space over a normed algebra `𝕜'` over `𝕜`), if `f: E → F` is differentiable at `x ∈ E` within a set `s ⊆ E`, and `c: E → 𝕜` is a scalar function differentiable at `x` within `s`, then the function `y ∈ s ↦ c(y)⊤f(y) ∈ 𝕜'` is differentiable at `x`.
|
differentiableAt_inv'
theorem differentiableAt_inv' :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {R : Type u_6} [inst_1 : NormedDivisionRing R]
[inst_2 : NormedAlgebra 𝕜 R] [inst_3 : CompleteSpace R] {x : R}, x ≠ 0 → DifferentiableAt 𝕜 Inv.inv x
The theorem `differentiableAt_inv'` states that for any non-zero element `x` in a complete normed division ring `R`, which is also a normed algebra over a non-trivially normed field `𝕜`, the function representing the inverse operation `Inv.inv` is differentiable at `x`. In other words, there exists a derivative of the inverse operation at any non-zero point in the ring.
More concisely: The inverse function in a complete normed division ring that is also a normed algebra over a non-trivially normed field is differentiable at any non-zero element.
|
DifferentiableAt.smul
theorem DifferentiableAt.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}
{x : E} {𝕜' : Type u_6} [inst_5 : NontriviallyNormedField 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜']
[inst_7 : NormedSpace 𝕜' F] [inst_8 : IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'},
DifferentiableAt 𝕜 c x → DifferentiableAt 𝕜 f x → DifferentiableAt 𝕜 (fun y => c y • f y) x
The theorem `DifferentiableAt.smul` states that for any types `𝕜`, `E`, `F`, and `𝕜'` where `𝕜` is a non-trivially normed field, `E` is a normed additive commutative group and is a normed space over `𝕜`, `F` is also a normed additive commutative group and a normed space over `𝕜` and `𝕜'`, and `𝕜'` is a non-trivially normed field with `𝕜` being a normed algebra over `𝕜'` and a scalar tower over `F`, if a function `f` from `E` to `F` is differentiable at a point `x` in `E`, and another function `c` from `E` to `𝕜'` is also differentiable at `x`, then the function defined by pointwise scalar multiplication of `c` and `f` (i.e., `(fun y => c y • f y)`) is also differentiable at `x`.
More concisely: If `f: E → F` is differentiable at `x ∈ E` and `c: E → ℝ'` is differentiable at `x` in the normed spaces `E` over `ℝ` and `F` over `ℝ'`, then the pointwise multiplication `(c ∘ x) • f` is differentiable at `x`.
|
differentiableAt_inverse
theorem differentiableAt_inverse :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {R : Type u_6} [inst_1 : NormedRing R]
[inst_2 : NormedAlgebra 𝕜 R] [inst_3 : CompleteSpace R] {x : R}, IsUnit x → DifferentiableAt 𝕜 Ring.inverse x
This theorem states that for every nontrivially normed field 𝕜 and a complete normed ring R over 𝕜, the function that sends a unit element `x` in R to its multiplicative inverse is differentiable at `x`. In simpler terms, the function that calculates the inverse of a unit in a certain complete normed ring is smooth at that unit point.
More concisely: The function sending a unit in a complete normed ring over a nontrivially normed field to its multiplicative inverse is differentiable.
|