English
Product rule with left scalar: [f·V, W] = - (df W)·V + f·[V, W].
Русский
Производное правило слева по скалярному множителю: [f·V, W] = - (Df f)(W)·V + f·[V, W].
LaTeX
$$$\mathrm{lieBracketWithin}(f\cdot V, W) = - (fderivWithin\mathbb{K} f)(W x)\cdot V x + f(x)\cdot \mathrm{lieBracketWithin}(V, W).$$$
Lean4
/-- Product rule for Lie Brackets: given two vector fields `V W : E → E` and a function `f : E → 𝕜`,
we have `[f • V, W] = - (df W) • V + f • [V, W]`
-/
theorem lieBracketWithin_smul_left {f : E → 𝕜} (hf : DifferentiableWithinAt 𝕜 f s x)
(hV : DifferentiableWithinAt 𝕜 V s x) (hs : UniqueDiffWithinAt 𝕜 s x) :
lieBracketWithin 𝕜 (fun y ↦ f y • V y) W s x =
-(fderivWithin 𝕜 f s x) (W x) • (V x) + (f x) • lieBracketWithin 𝕜 V W s x :=
by
rw [lieBracketWithin_swap, Pi.neg_apply, lieBracketWithin_smul_right hf hV hs, lieBracketWithin_swap, add_comm]
simp
