isLittleO_alternate_sum_square — Mathlib

English

Let f be differentiable inside a convex set s with second derivative f''. The alternating sum of f at the vertices of a small square with sides along v and w, scaled by h, yields a term that, after subtracting h^2 f''(v,w), is o(h^2) as h → 0^+.

Русский

Пусть f дифференцируема внутри выпуклого s и имеет вторую производную f''. Степенная сумма по вершинам квадрата малых сторон hv и hw, взятая с чередованием, после вычитания h^2 f''(v,w) дает остаток o(h^2) при h → 0^+.

LaTeX

$$$$ f(x+ h(2v+2w)) + f(x+ h(v+w)) - f(x+ h(2v+w)) - f(x+ h(v+2w)) - h^2 f''(v,w) = o(h^2) $$$$

Lean4

/-- One can get `f'' v w` as the limit of `h ^ (-2)` times the alternate sum of the values of `f`
along the vertices of a quadrilateral with sides `h v` and `h w` based at `x`.
In a setting where `f` is not guaranteed to be continuous at `f`, we can still
get this if we use a quadrilateral based at `h v + h w`. -/
theorem isLittleO_alternate_sum_square {v w : E} (h4v : x + (4 : ℝ) • v ∈ interior s)
    (h4w : x + (4 : ℝ) • w ∈ interior s) :
    (fun h : ℝ =>
        f (x + h • (2 • v + 2 • w)) + f (x + h • (v + w)) - f (x + h • (2 • v + w)) - f (x + h • (v + 2 • w)) -
          h ^ 2 • f'' v w) =o[𝓝[>] 0]
      fun h => h ^ 2 :=
  by
  have A : (1 : ℝ) / 2 ∈ Ioc (0 : ℝ) 1 := ⟨by simp, by norm_num⟩
  have B : (1 : ℝ) / 2 ∈ Icc (0 : ℝ) 1 := ⟨by simp, by norm_num⟩
  have h2v2w : x + (2 : ℝ) • v + (2 : ℝ) • w ∈ interior s :=
    by
    convert s_conv.interior.add_smul_sub_mem h4v h4w B using 1
    module
  have h2vww : x + (2 • v + w) + w ∈ interior s :=
    by
    convert h2v2w using 1
    module
  have h2v : x + (2 : ℝ) • v ∈ interior s :=
    by
    convert s_conv.add_smul_sub_mem_interior xs h4v A using 1
    module
  have h2w : x + (2 : ℝ) • w ∈ interior s :=
    by
    convert s_conv.add_smul_sub_mem_interior xs h4w A using 1
    module
  have hvw : x + (v + w) ∈ interior s :=
    by
    convert s_conv.add_smul_sub_mem_interior xs h2v2w A using 1
    module
  have h2vw : x + (2 • v + w) ∈ interior s :=
    by
    convert s_conv.interior.add_smul_sub_mem h2v h2v2w B using 1
    module
  have hvww : x + (v + w) + w ∈ interior s :=
    by
    convert s_conv.interior.add_smul_sub_mem h2w h2v2w B using 1
    module
  have TA1 := s_conv.taylor_approx_two_segment hf xs hx h2vw h2vww
  have TA2 := s_conv.taylor_approx_two_segment hf xs hx hvw hvww
  convert TA1.sub TA2 using 1
  ext h
  simp only [two_smul, smul_add, ← add_assoc, ContinuousLinearMap.map_add, ContinuousLinearMap.add_apply]
  abel

Похожие утверждения