English
For a bilinear map B, the derivative within a set s of the map y ↦ B(u(y), v(y)) equals the sum of the appropriate bilinear actions of derivatives of u and v, respecting the Within structure.
Русский
Для билинейной карты B производная внутри множества s функции y ↦ B(u(y), v(y)) равна сумме соответствующих билинейных вкладов производных u и v.
LaTeX
$$$\text{If } u,v\text{ are differentiable within } s, \\ \ derivWithin( f(y)=B(u(y),v(y)) , s, x) = B(u(x), derivWithin(v,s,x)) + B(derivWithin(u,s,x), v(x)).$$$
Lean4
theorem derivWithin_of_bilinear (hu : DifferentiableWithinAt 𝕜 u s x) (hv : DifferentiableWithinAt 𝕜 v s x) :
derivWithin (fun y => B (u y) (v y)) s x = B (u x) (derivWithin v s x) + B (derivWithin u s x) (v x) :=
by
by_cases hsx : UniqueDiffWithinAt 𝕜 s x
· exact (B.hasDerivWithinAt_of_bilinear hu.hasDerivWithinAt hv.hasDerivWithinAt).derivWithin hsx
· simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]
