English
Product rule for Lie brackets: [V, f·W] = (df V)·W + f·[V, W].
Русский
Правило произведения для скобки Ли: [V, f·W] = (df V)·W + f·[V, W].
LaTeX
$$$\mathrm{lieBracketWithin}(V, (y \mapsto f(y)\,W(y))) = (fderivWithin\mathbb{K} f\, s\, x)(Vx)\cdot Wx + f(x)\cdot \mathrm{lieBracketWithin}(V, W, s, x)$$$
Lean4
/-- Product rule for Lie Brackets: given two vector fields `V W : E → E` and a function `f : E → 𝕜`,
we have `[V, f • W] = (df V) • W + f • [V, W]`
-/
theorem lieBracketWithin_smul_right {f : E → 𝕜} (hf : DifferentiableWithinAt 𝕜 f s x)
(hW : DifferentiableWithinAt 𝕜 W s x) (hs : UniqueDiffWithinAt 𝕜 s x) :
lieBracketWithin 𝕜 V (fun y ↦ f y • W y) s x =
(fderivWithin 𝕜 f s x) (V x) • (W x) + (f x) • lieBracketWithin 𝕜 V W s x :=
by simp [lieBracketWithin, fderivWithin_fun_smul hs hf hW, map_smul, add_comm, smul_sub, add_sub_assoc]
