English
A simplified form of the symmetry statement for the alternate-sum square; under the convex setting, the little-o bounds hold in a simplified index form.
Русский
Упрощенная форма симметрии для квадрата чередующих сумм; при выпуклом множестве небольшие o-погрешности сохраняются в упрощенной форме индексов.
LaTeX
$$$$ (f'' w v - f'' v w) = o(1) \\quad \\text{as } h \\to 0. $$$$
Lean4
/-- If a function is `C^2` at a point, then its second derivative there is symmetric. Over a field
different from `ℝ` or `ℂ`, we should require that the function is analytic. -/
theorem isSymmSndFDerivAt {n : WithTop ℕ∞} (hf : ContDiffAt 𝕜 n f x) (hn : minSmoothness 𝕜 2 ≤ n) :
IsSymmSndFDerivAt 𝕜 f x := by
by_cases h : IsRCLikeNormedField 𝕜
· intro v w
apply second_derivative_symmetric_of_eventually (f := f) (f' := fderiv 𝕜 f) (x := x)
· obtain ⟨u, hu, h'u⟩ : ∃ u ∈ 𝓝 x, ContDiffOn 𝕜 2 f u :=
(hf.of_le hn).contDiffOn (m := 2) le_minSmoothness (by simp)
rcases mem_nhds_iff.1 hu with ⟨v, vu, v_open, xv⟩
filter_upwards [v_open.mem_nhds xv] with y hy
have : DifferentiableAt 𝕜 f y :=
by
have := (h'u.mono vu y hy).contDiffAt (v_open.mem_nhds hy)
exact this.differentiableAt one_le_two
exact DifferentiableAt.hasFDerivAt this
· have : DifferentiableAt 𝕜 (fderiv 𝕜 f) x :=
by
apply ContDiffAt.differentiableAt _ le_rfl
exact hf.fderiv_right (le_minSmoothness.trans hn)
exact DifferentiableAt.hasFDerivAt this
· simp only [minSmoothness, h, ↓reduceIte, top_le_iff] at hn
apply ContDiffAt.isSymmSndFDerivAt_of_omega
simpa [hn] using hf
