English
Under the same hypotheses as the previous results, the alternate-sum expressions over quadrilaterals yield symmetry constraints on f''; concretely, certain linear combinations vanish in the limit as the step h tends to 0.
Русский
При тех же предположениях итоговые выражения по чередованию вершин квадрилатерала дают условия симметрии для f''; в частности, линейные комбинации сходятся к нулю при стремлении h к нулю.
LaTeX
$$$$ \\text{alternate sums} = o(h^2). $$$$
Lean4
/-- If a function is differentiable around `x`, and has two derivatives at `x`, then the second
derivative is symmetric. Version over `ℝ`. See `second_derivative_symmetric_of_eventually` for a
version over `ℝ` or `ℂ`. -/
theorem second_derivative_symmetric_of_eventually_of_real {f : E → F} {f' : E → E →L[ℝ] F} {f'' : E →L[ℝ] E →L[ℝ] F}
(hf : ∀ᶠ y in 𝓝 x, HasFDerivAt f (f' y) y) (hx : HasFDerivAt f' f'' x) (v w : E) : f'' v w = f'' w v :=
by
rcases Metric.mem_nhds_iff.1 hf with ⟨ε, εpos, hε⟩
have A : (interior (Metric.ball x ε)).Nonempty := by rwa [Metric.isOpen_ball.interior_eq, Metric.nonempty_ball]
exact
Convex.second_derivative_within_at_symmetric (convex_ball x ε) A (fun y hy => hε (interior_subset hy))
(Metric.mem_ball_self εpos) hx.hasFDerivWithinAt v w
