has_deriv_at_interval_right_endpoint_of_tendsto_deriv
theorem has_deriv_at_interval_right_endpoint_of_tendsto_deriv :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set ℝ} {e : E} {a : ℝ} {f : ℝ → E},
DifferentiableOn ℝ f s →
ContinuousWithinAt f s a →
s ∈ nhdsWithin a (Set.Iio a) →
Filter.Tendsto (fun x => deriv f x) (nhdsWithin a (Set.Iio a)) (nhds e) →
HasDerivWithinAt f e (Set.Iic a) a
The theorem `has_deriv_at_interval_right_endpoint_of_tendsto_deriv` states that if a function `f` mapping real numbers to a normed additive commutative group `E` is differentiable on a set `s`, continuous at a real number `a` within `s`, and if `s` belongs to the neighborhood of `a` within the left-open interval ending at `a` and the derivative of `f` converges to `e` in the neighborhood of `a` within the left-open interval ending at `a`, then `f` has a derivative `e` at `a` within the left-closed interval ending at `a`. In mathematical terms, if a function's derivative exists on the left of a point and also tends to a limit at that point, then the function is differentiable at that point from the left.
More concisely: If a real-valued differentiable function on a set is continuous at a point, has a convergent derivative in the left-open interval containing that point, then it is differentiable from the left at that point with the given limit as its derivative.
|
has_fderiv_at_boundary_of_tendsto_fderiv
theorem has_fderiv_at_boundary_of_tendsto_fderiv :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {F : Type u_2}
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {f : E → F} {s : Set E} {x : E} {f' : E →L[ℝ] F},
DifferentiableOn ℝ f s →
Convex ℝ s →
IsOpen s →
(∀ y ∈ closure s, ContinuousWithinAt f s y) →
Filter.Tendsto (fun y => fderiv ℝ f y) (nhdsWithin x s) (nhds f') →
HasFDerivWithinAt f f' (closure s) x
The theorem `has_fderiv_at_boundary_of_tendsto_fderiv` states that if a function `f` from a normed additive commutative group `E` to another such group `F` (both over the real numbers), is differentiable on a convex and open set `s` and continuous on the closure of `s`, and if the derivative of `f` converges to a limit `f'` at a point `x` on the boundary of `s`, then `f` is differentiable at the point `x` with the derivative being `f'`. In other words, under the given conditions, the derivative of `f` at a boundary point of `s` exists and matches the limit of the derivative within the set `s`.
More concisely: If a real-valued function `f` on a convex, open set `s` in a normed additive commutative group is differentiable on `s` and continuously differentiable on the closure of `s`, then `f` has a derivative at every boundary point of `s` equal to the limit of its derivatives on `s`.
|
hasDerivAt_of_hasDerivAt_of_ne
theorem hasDerivAt_of_hasDerivAt_of_ne :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f g : ℝ → E} {x : ℝ},
(∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y) → ContinuousAt f x → ContinuousAt g x → HasDerivAt f (g x) x
This theorem states that if a real-valued function `f` has a derivative `g` at all points except possibly one, and both `f` and `g` are continuous at this excepted point, then `g` is also the derivative of `f` at this point. In mathematical terms, for all real numbers `y` not equal to `x`, if `f` has a derivative `g(y)` at `y`, and if `f` and `g` are both continuous at `x`, then `g(x)` is the derivative of `f` at `x`.
More concisely: If a real-valued function `f` has a continuous derivative `g` everywhere except possibly at `x`, and `f` and `g` are continuous at `x`, then `g(x)` is the derivative of `f` at `x`.
|
hasDerivAt_of_hasDerivAt_of_ne'
theorem hasDerivAt_of_hasDerivAt_of_ne' :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f g : ℝ → E} {x : ℝ},
(∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y) →
ContinuousAt f x → ContinuousAt g x → ∀ (y : ℝ), HasDerivAt f (g y) y
The theorem `hasDerivAt_of_hasDerivAt_of_ne'` states that for a real function `f` and another function `g`, if `f` has a derivative `g` at every point except one point `x`, and if both `f` and `g` are continuous at `x`, then `g` is the derivative of `f` at every point. In other words, even if the function `f` is not differentiable at a particular point, as long as the function `f` and its derivative `g` are continuous at that point, the derivative of the function `f` everywhere is `g`.
More concisely: If real functions `f` and `g` are such that `f` has derivative `g` everywhere except at point `x`, and both `f` and `g` are continuous at `x`, then `g` is the derivative of `f` at every point.
|
has_deriv_at_interval_left_endpoint_of_tendsto_deriv
theorem has_deriv_at_interval_left_endpoint_of_tendsto_deriv :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set ℝ} {e : E} {a : ℝ} {f : ℝ → E},
DifferentiableOn ℝ f s →
ContinuousWithinAt f s a →
s ∈ nhdsWithin a (Set.Ioi a) →
Filter.Tendsto (fun x => deriv f x) (nhdsWithin a (Set.Ioi a)) (nhds e) →
HasDerivWithinAt f e (Set.Ici a) a
The theorem `has_deriv_at_interval_left_endpoint_of_tendsto_deriv` states that if a function `f` from real numbers to a normed additive commutative group `E` is differentiable on a set `s`, and is continuous at a real number `a` within this set `s`, and the set `s` is in the neighborhood of `a` within the interval `(a, ∞)`, and the derivative of `f` converges to an element `e` in `E` when the input approaches `a` from values greater than `a`, then `f` has the derivative `e` at `a` within the interval `[a, ∞)`. In simple words, if a function is differentiable and continuous at a point, and its derivative also converges at the same point from the right, then the function is differentiable at that point from the right.
More concisely: If a differentiable and continuous function at a point in the interval (a, ∞) has a converging derivative at that point from the right, then the function is right-differentiable at that point with the given limit as its derivative.
|