second_derivative_symmetric
theorem second_derivative_symmetric :
∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {x : E} {f : E → F} {f' : E → E →L[ℝ] F}
{f'' : E →L[ℝ] E →L[ℝ] F},
(∀ (y : E), HasFDerivAt f (f' y) y) → HasFDerivAt f' f'' x → ∀ (v w : E), (f'' v) w = (f'' w) v
This theorem states that for a function that is differentiable, if it has two derivatives at a point `x`, then the second derivative is symmetric. Specifically, given a function `f` from a normed additive commutative group `E` to another one `F`, both over the real numbers, and given two continuous linear maps `f'` and `f''`, if for every point `y` in `E` the function `f` has `f' y` as its derivative at `y`, and if `f'` has `f''` as its derivative at `x`, then for every pair of points `v` and `w` in `E`, the value of `f''` at `v` applied to `w` is the same as the value of `f''` at `w` applied to `v`. In mathematical terms, if $f: E \rightarrow F$ is differentiable, and if $f'(y)$ and $f''(x)$ are its first and second derivatives respectively, then the second derivative is symmetric, i.e. $f''(v)(w) = f''(w)(v)$ for all $v, w \in E$.
More concisely: If a differentiable function $f: E \rightarrow F$ over the real numbers has symmetric second derivatives $f''$, then $f''(v)(w) = f''(w)(v)$ for all $v, w \in E$.
|
second_derivative_symmetric_of_eventually
theorem second_derivative_symmetric_of_eventually :
∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {x : E} {f : E → F} {f' : E → E →L[ℝ] F}
{f'' : E →L[ℝ] E →L[ℝ] F},
(∀ᶠ (y : E) in nhds x, HasFDerivAt f (f' y) y) → HasFDerivAt f' f'' x → ∀ (v w : E), (f'' v) w = (f'' w) v
The theorem `second_derivative_symmetric_of_eventually` states that given a function `f` mapping from a normed additive commutative group `E` to another normed additive commutative group `F`, both over the real numbers ℝ, and provided that `f` is differentiable around a particular point `x` in `E`, and has two derivatives at `x` denoted by `f'` and `f''`, then the second derivative `f''` is symmetric. That is, for all pairs of elements `(v, w)` in `E`, the second derivative of the function at `v` and then at `w` is the same as the second derivative of the function at `w` and then at `v`. The differentiability of `f` around `x` is expressed as the condition that for all `y` in a neighborhood of `x` (expressed as `∀ᶠ (y : E) in nhds x`), `f` has derivative `f' y` at `y`. The second derivative `f''` of `f` at `x` is determined by `HasFDerivAt f' f'' x`.
More concisely: Given a real-valued, differentiable function `f` on a normed additive commutative group with two derivatives at a point `x`, the second derivatives `f''(x)(v)` and `f''(x)(w)` are equal for all `v, w` in the group.
|