English
If h is a bounded bilinear map, then it has a strict Fréchet derivative at every p with derivative given by h.deriv p.
Русский
Если gранична билинейная карта h, то у нее есть строгая Фредхеп-производная в любой точке p, производная равна h.deriv p.
LaTeX
$$$\text{HasStrictFDerivAt}(b, h.deriv p, p)$ for $h$ bounded bilinear$$
Lean4
@[fun_prop]
theorem hasStrictFDerivAt (h : IsBoundedBilinearMap 𝕜 b) (p : E × F) : HasStrictFDerivAt b (h.deriv p) p :=
by
simp only [hasStrictFDerivAt_iff_isLittleO]
simp only [← map_add_left_nhds_zero (p, p), isLittleO_map]
set T := (E × F) × E × F
calc
_ = fun x ↦ h.deriv (x.1 - x.2) (x.2.1, x.1.2) :=
by
ext ⟨⟨x₁, y₁⟩, ⟨x₂, y₂⟩⟩
rcases p with ⟨x, y⟩
simp only [map_sub, deriv_apply, Function.comp_apply, Prod.mk_add_mk, h.add_right, h.add_left, Prod.mk_sub_mk,
h.map_sub_left, h.map_sub_right, sub_add_sub_cancel]
abel
-- _ =O[𝓝 (0 : T)] fun x ↦ ‖x.1 - x.2‖ * ‖(x.2.1, x.1.2)‖ :=
-- h.toContinuousLinearMap.deriv₂.isBoundedBilinearMap.isBigO_comp
-- _ = o[𝓝 0] fun x ↦ ‖x.1 - x.2‖ * 1 := _
_ =o[𝓝 (0 : T)] fun x ↦ x.1 - x.2 := by
-- TODO : add 2 `calc` steps instead of the next 3 lines
refine h.toContinuousLinearMap.deriv₂.isBoundedBilinearMap.isBigO_comp.trans_isLittleO ?_
suffices (fun x : T ↦ ‖x.1 - x.2‖ * ‖(x.2.1, x.1.2)‖) =o[𝓝 0] fun x ↦ ‖x.1 - x.2‖ * 1 by
simpa only [mul_one, isLittleO_norm_right] using this
refine
(isBigO_refl _ _).mul_isLittleO
((isLittleO_one_iff _).2 ?_)
-- TODO: `continuity` fails
exact (continuous_snd.fst.prodMk continuous_fst.snd).norm.tendsto' _ _ (by simp)
_ = _ := by simp [T, Function.comp_def]
