English
If f is differentiable inside a convex set s and has a well-defined second derivative at a point x ∈ interior s, then f'' v w = f'' w v for any vectors v,w pointing inside s.
Русский
Если f дифференцируема внутри выпуклого множествa s и в точке x ∈ interior s существует вторая производная, то f'' v w = f'' w v для любых векторов v, w, входящих внутрь s.
LaTeX
$$$$ f''(v,w) = f''(w,v). $$$$
Lean4
/-- Assume that `f` is differentiable inside a convex set `s`, and that its derivative `f'` is
differentiable at a point `x`. Then, given two vectors `v` and `w` pointing inside `s`, one
has `f'' v w = f'' w v`. Superseded by `Convex.second_derivative_within_at_symmetric`, which
removes the assumption that `v` and `w` point inside `s`. -/
theorem second_derivative_within_at_symmetric_of_mem_interior {v w : E} (h4v : x + (4 : ℝ) • v ∈ interior s)
(h4w : x + (4 : ℝ) • w ∈ interior s) : f'' w v = f'' v w :=
by
have A : (fun h : ℝ => h ^ 2 • (f'' w v - f'' v w)) =o[𝓝[>] 0] fun h => h ^ 2 :=
by
convert
(s_conv.isLittleO_alternate_sum_square hf xs hx h4v h4w).sub
(s_conv.isLittleO_alternate_sum_square hf xs hx h4w h4v) using
1
ext h
simp only [add_comm, smul_add, smul_sub]
abel
have B : (fun _ : ℝ => f'' w v - f'' v w) =o[𝓝[>] 0] fun _ => (1 : ℝ) :=
by
have : (fun h : ℝ => 1 / h ^ 2) =O[𝓝[>] 0] fun h => 1 / h ^ 2 := isBigO_refl _ _
have C := this.smul_isLittleO A
apply C.congr' _ _
· filter_upwards [self_mem_nhdsWithin]
intro h (hpos : 0 < h)
match_scalars <;> field_simp
· filter_upwards [self_mem_nhdsWithin] with h (hpos : 0 < h)
simp [field]
simpa only [sub_eq_zero] using isLittleO_const_const_iff.1 B
