English
Let E and F be normed spaces. Suppose f: E → F is differentiable inside a convex set s, and its first and second derivatives f' and f'' exist along the segment connecting x with x + hv and x + hw. Then a second-order Taylor expansion along the segment {x + h v, x + h (v + w)} holds with an o(h^2) remainder; equivalently, the difference between f along the two-parameter path and its second-order Taylor polynomial is little-o of h^2 as h → 0^+.
Русский
Пусть E, F – нормированные пространства. Пусть f: E → F дифференцируема внутри выпуклого множества s, и существуют первые и вторые производные f', f'' вдоль сегмента, соединяющего x и x + h v, x + h (v + w). Тогда поужинаемое по Тейлору во втором порядке вдоль сегмента {x + h v, x + h (v + w)} имеет остаток o(h^2); то есть выражение, отличающееся от его второго порядка аппроксимации, является малы по отношению к h^2 при h → 0^+.
LaTeX
$$$$\\displaystyle \\Big(f(x+hv+hw) - f(xhv) - h\\,f'(x)w - h^2\\,f''(v,w) - \\frac{h^2}{2}\\,f''(w,w)\\Big) = o(h^2) \\quad \\text{as } h \\to 0^+.$$$$
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 can
Taylor-expand to order two the function `f` on the segment `[x + h v, x + h (v + w)]`, giving a
bilinear estimate for `f (x + hv + hw) - f (x + hv)` in terms of `f' w` and of `f'' ⬝ w`, up to
`o(h^2)`.
This is a technical statement used to show that the second derivative is symmetric. -/
theorem taylor_approx_two_segment {v w : E} (hv : x + v ∈ interior s) (hw : x + v + w ∈ interior s) :
(fun h : ℝ =>
f (x + h • v + h • w) - f (x + h • v) - h • f' x w - h ^ 2 • f'' v w - (h ^ 2 / 2) • f'' w w) =o[𝓝[>] 0]
fun h => h ^ 2 :=
by
-- it suffices to check that the expression is bounded by `ε * ((‖v‖ + ‖w‖) * ‖w‖) * h^2` for
-- small enough `h`, for any positive `ε`.
refine
IsLittleO.trans_isBigO (isLittleO_iff.2 fun ε εpos => ?_)
(isBigO_const_mul_self ((‖v‖ + ‖w‖) * ‖w‖) _ _)
-- consider a ball of radius `δ` around `x` in which the Taylor approximation for `f''` is
-- good up to `δ`.
rw [HasFDerivWithinAt, hasFDerivAtFilter_iff_isLittleO, isLittleO_iff] at hx
rcases Metric.mem_nhdsWithin_iff.1 (hx εpos) with ⟨δ, δpos, sδ⟩
have E1 : ∀ᶠ h in 𝓝[>] (0 : ℝ), h * (‖v‖ + ‖w‖) < δ :=
by
have : Filter.Tendsto (fun h => h * (‖v‖ + ‖w‖)) (𝓝[>] (0 : ℝ)) (𝓝 (0 * (‖v‖ + ‖w‖))) :=
(continuous_id.mul continuous_const).continuousWithinAt
apply (tendsto_order.1 this).2 δ
simpa only [zero_mul] using δpos
have E2 : ∀ᶠ h in 𝓝[>] (0 : ℝ), (h : ℝ) < 1 := mem_nhdsWithin_of_mem_nhds <| Iio_mem_nhds zero_lt_one
filter_upwards [E1, E2, self_mem_nhdsWithin] with h hδ h_lt_1 hpos
replace hpos : 0 < h := hpos
have xt_mem : ∀ t ∈ Icc (0 : ℝ) 1, x + h • v + (t * h) • w ∈ interior s :=
by
intro t ht
have : x + h • v ∈ interior s := s_conv.add_smul_mem_interior xs hv ⟨hpos, h_lt_1.le⟩
rw [← smul_smul]
apply s_conv.interior.add_smul_mem this _ ht
rw [add_assoc] at hw
convert s_conv.add_smul_mem_interior xs hw ⟨hpos, h_lt_1.le⟩ using 1
module
-- define a function `g` on `[0,1]` (identified with `[v, v + w]`) such that `g 1 - g 0` is the
-- quantity to be estimated. We will check that its derivative is given by an explicit
-- expression `g'`, that we can bound. Then the desired bound for `g 1 - g 0` follows from the
-- mean value inequality.
let g t := f (x + h • v + (t * h) • w) - (t * h) • f' x w - (t * h ^ 2) • f'' v w - ((t * h) ^ 2 / 2) • f'' w w
set g' := fun t => f' (x + h • v + (t * h) • w) (h • w) - h • f' x w - h ^ 2 • f'' v w - (t * h ^ 2) • f'' w w with
hg'
have g_deriv : ∀ t ∈ Icc (0 : ℝ) 1, HasDerivWithinAt g (g' t) (Icc 0 1) t :=
by
intro t ht
apply_rules [HasDerivWithinAt.sub, HasDerivWithinAt.add]
· refine (hf _ ?_).comp_hasDerivWithinAt _ ?_
· exact xt_mem t ht
apply_rules [HasDerivAt.hasDerivWithinAt, HasDerivAt.const_add, HasDerivAt.smul_const, hasDerivAt_mul_const]
· apply_rules [HasDerivAt.hasDerivWithinAt, HasDerivAt.smul_const, hasDerivAt_mul_const]
· apply_rules [HasDerivAt.hasDerivWithinAt, HasDerivAt.smul_const, hasDerivAt_mul_const]
· suffices H :
HasDerivWithinAt (fun u => ((u * h) ^ 2 / 2) • f'' w w)
((((2 : ℕ) : ℝ) * (t * h) ^ (2 - 1) * (1 * h) / 2) • f'' w w) (Icc 0 1) t
by
convert H using 2
ring
apply_rules [HasDerivAt.hasDerivWithinAt, HasDerivAt.smul_const, hasDerivAt_id', HasDerivAt.pow,
HasDerivAt.mul_const]
-- check that `g'` is uniformly bounded, with a suitable bound `ε * ((‖v‖ + ‖w‖) * ‖w‖) * h^2`.
have g'_bound : ∀ t ∈ Ico (0 : ℝ) 1, ‖g' t‖ ≤ ε * ((‖v‖ + ‖w‖) * ‖w‖) * h ^ 2 :=
by
intro t ht
have I : ‖h • v + (t * h) • w‖ ≤ h * (‖v‖ + ‖w‖) :=
calc
‖h • v + (t * h) • w‖ ≤ ‖h • v‖ + ‖(t * h) • w‖ := norm_add_le _ _
_ = h * ‖v‖ + t * (h * ‖w‖) := by
simp only [norm_smul, Real.norm_eq_abs, hpos.le, abs_of_nonneg, abs_mul, ht.left, mul_assoc]
_ ≤ h * ‖v‖ + 1 * (h * ‖w‖) := by gcongr; exact ht.2.le
_ = h * (‖v‖ + ‖w‖) := by ring
calc
‖g' t‖ = ‖(f' (x + h • v + (t * h) • w) - f' x - f'' (h • v + (t * h) • w)) (h • w)‖ :=
by
rw [hg']
congrm ‖?_‖
simp only [ContinuousLinearMap.sub_apply, ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply,
map_add, map_smul]
module
_ ≤ ‖f' (x + h • v + (t * h) • w) - f' x - f'' (h • v + (t * h) • w)‖ * ‖h • w‖ :=
(ContinuousLinearMap.le_opNorm _ _)
_ ≤ ε * ‖h • v + (t * h) • w‖ * ‖h • w‖ := by
gcongr
have H : x + h • v + (t * h) • w ∈ Metric.ball x δ ∩ interior s :=
by
refine ⟨?_, xt_mem t ⟨ht.1, ht.2.le⟩⟩
rw [add_assoc, add_mem_ball_iff_norm]
exact I.trans_lt hδ
simpa only [mem_setOf_eq, add_assoc x, add_sub_cancel_left] using sδ H
_ ≤ ε * (‖h • v‖ + ‖h • w‖) * ‖h • w‖ := by
gcongr
apply (norm_add_le _ _).trans
gcongr
simp only [norm_smul, Real.norm_eq_abs, abs_mul, abs_of_nonneg, ht.1, hpos.le, mul_assoc]
exact mul_le_of_le_one_left (by positivity) ht.2.le
_ = ε * ((‖v‖ + ‖w‖) * ‖w‖) * h ^ 2 := by simp only [norm_smul, Real.norm_eq_abs, abs_of_nonneg, hpos.le];
ring
-- conclude using the mean value inequality
have I : ‖g 1 - g 0‖ ≤ ε * ((‖v‖ + ‖w‖) * ‖w‖) * h ^ 2 := by
simpa only [mul_one, sub_zero] using
norm_image_sub_le_of_norm_deriv_le_segment' g_deriv g'_bound 1 (right_mem_Icc.2 zero_le_one)
convert I using 1
· congr 1
simp only [g, add_zero, one_mul, zero_div, zero_mul, sub_zero, zero_smul, Ne, not_false_iff, zero_pow, reduceCtorEq]
abel
· simp (discharger := positivity) only [Real.norm_eq_abs, abs_of_nonneg]
ring
