English
The derivative of a bilinear composition has a formula given by the composition of hasFDerivAt with the bilinear map and its flipped version; concretely, the derivative of y ↦ (c y).comp (d y) is the sum of two composed derivatives.
Русский
Производная по переменной y композиции с билинейной связью задаётся суммой двух композиций производных, соответствующих c и d.
LaTeX
$$$\\text{HasFDerivAt } c c' x \\;\\&\\; \\text{HasFDerivAt } d d' x \\Rightarrow \\text{HasFDerivAt } (y \\mapsto (c y).comp (d y)) (\\text{...}) x$$$
Lean4
theorem hasFDerivAtFilter_iff_tendsto :
HasFDerivAtFilter f f' x L ↔ Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) L (𝓝 0) :=
by
have h : ∀ x', ‖x' - x‖ = 0 → ‖f x' - f x - f' (x' - x)‖ = 0 := fun x' hx' =>
by
rw [sub_eq_zero.1 (norm_eq_zero.1 hx')]
simp
rw [hasFDerivAtFilter_iff_isLittleO, ← isLittleO_norm_left, ← isLittleO_norm_right, isLittleO_iff_tendsto h]
exact tendsto_congr fun _ => div_eq_inv_mul _ _
