deriv_inv
theorem deriv_inv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜}, deriv (fun x => x⁻¹) x = -(x ^ 2)⁻¹ := by
sorry
This theorem states that for any non-trivially normed field `𝕜` and any value `x` in this field, the derivative of the function `f(x) = x⁻¹` (the reciprocal of `x`) at the point `x` is equal to `-(x ^ 2)⁻¹` (the negative reciprocal of the square of `x`). In mathematical terms, if `f(x) = 1/x`, then `f'(x) = -1/x²`. This is a basic result in calculus.
More concisely: The derivative of the reciprocal function `f(x) = 1/x` is `-1/x²`.
|
DifferentiableAt.inv
theorem DifferentiableAt.inv :
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type w} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {h : E → 𝕜} {z : E},
DifferentiableAt 𝕜 h z → h z ≠ 0 → DifferentiableAt 𝕜 (fun x => (h x)⁻¹) z
The theorem `DifferentiableAt.inv` states that for any non-trivially normed field `𝕜` and normed additive commutative group `E` that is a normed space over `𝕜`, if we have a function `h : E → 𝕜` that is differentiable at a point `z` and the value of `h` at `z` is not zero, then the function that maps any `x` to the multiplicative inverse of `h(x)` (i.e., `(h x)⁻¹`) is also differentiable at `z`.
More concisely: If `h : E → 𝕜` is differentiable at `z ∈ E` in the normed space `(E, 𝕜)` and `h(z) ≠ 0`, then the function `x ↦ h(x)⁻¹` is differentiable at `z`.
|
hasDerivAt_inv
theorem hasDerivAt_inv :
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜}, x ≠ 0 → HasDerivAt (fun y => y⁻¹) (-(x ^ 2)⁻¹) x := by
sorry
This theorem states that for any non-zero point `x` from a non-trivially normed field `𝕜`, the function given by the reciprocal of `y` has a derivative at `x`, where the derivative is the negative reciprocal of the square of `x`. In mathematical terms, if `y = y⁻¹` then the derivative of `y` at `x` is `-(x ^ 2)⁻¹`, provided `x ≠ 0`.
More concisely: For any non-zero element `x` in a non-trivially normed field, the reciprocal function has a derivative equal to the negative reciprocal of the square of `x` at `x`.
|
differentiableAt_inv
theorem differentiableAt_inv :
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜}, DifferentiableAt 𝕜 (fun x => x⁻¹) x ↔ x ≠ 0
The theorem `differentiableAt_inv` states that for any point `x` in a non-trivially normed field `𝕜`, the function `f(x) = x⁻¹` (the reciprocal function) is differentiable at `x` if and only if `x` is not zero. This means that the reciprocal function has a derivative at any point `x` that is not zero, and it does not have a derivative at `x = 0`.
More concisely: The reciprocal function is differentiable at a point in a non-trivially normed field if and only if that point is non-zero.
|
DifferentiableWithinAt.inv
theorem DifferentiableWithinAt.inv :
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type w} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {h : E → 𝕜} {z : E} {S : Set E},
DifferentiableWithinAt 𝕜 h S z → h z ≠ 0 → DifferentiableWithinAt 𝕜 (fun x => (h x)⁻¹) S z
The theorem `DifferentiableWithinAt.inv` states that for any non-trivial normed field `𝕜` and any normed add commutative group `E` over `𝕜`, if a function `h : E → 𝕜` is differentiable at a point `z` within a set `S`, and the value of the function `h` at `z` is non-zero, then the function `x ↦ (h x)⁻¹` is also differentiable at the same point `z` within the same set `S`. This captures the intuitive concept that the reciprocal of a differentiable function, under certain conditions, is also differentiable.
More concisely: If `h : E → ℝ` is differentiable at `z` in the normed add commutative group `E` over a non-trivial normed field `ℝ`, and `h(z) ≠ 0`, then the function `x ↦ h(x)⁻¹` is differentiable at `z`.
|
HasDerivWithinAt.div
theorem HasDerivWithinAt.div :
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_1}
[inst_1 : NontriviallyNormedField 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜'] {c d : 𝕜 → 𝕜'} {c' d' : 𝕜'},
HasDerivWithinAt c c' s x →
HasDerivWithinAt d d' s x →
d x ≠ 0 → HasDerivWithinAt (fun y => c y / d y) ((c' * d x - c x * d') / d x ^ 2) s x
This theorem states that for any two functions `c` and `d` of some type `𝕜` to `𝕜'`, where `𝕜` and `𝕜'` are nontrivially normed fields, `c` and `d` both have derivatives `c'` and `d'` at a point `x` within a subset `s` of `𝕜`, and the value of `d` at `x` is not zero, then the quotient function `(c y) / (d y)` has a derivative at `x` within the subset `s`. The derivative of the quotient function at `x` is given by the quotient rule for derivatives, `(c' * d x - c x * d') / (d x) ^ 2`.
More concisely: If `c` and `d` are differentiable functions from a nontrivially normed field `𝕜` to another such field `𝕜'`, `d(x) ≠ 0` for some `x` in a subset `s` of `𝕜`, then the quotient function `c / d` is differentiable at `x` in `s` and its derivative is `(c' * d x - c x * d') / (d x) ^ 2`.
|