English
Left multiplication by a scalar function in the first argument of the Lie bracket obeys a product rule with a minus sign on the derivative term: [f·V, W] = -(Df f)(W)·V + f·[V, W].
Русский
Левая линейная композиция по функции-скаляру в первой компоненте скобки Ли удовлетворяет правилу произведения с минусом в производной: [f·V, W] = -(Df f)(W)·V + f·[V, W].
LaTeX
$$$\mathrm{lieBracket}(V, f\cdot W) = - (fderiv\mathbb{K} f)(W)\cdot V + f\cdot \mathrm{lieBracket}(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 lieBracket_fmul_left {f : E → 𝕜} (hf : DifferentiableAt 𝕜 f x) (hV : DifferentiableAt 𝕜 V x) :
lieBracket 𝕜 (fun y ↦ f y • V y) W x = -(fderiv 𝕜 f x) (W x) • (V x) + (f x) • lieBracket 𝕜 V W x :=
by
rw [lieBracket_swap, lieBracket_smul_right hf hV, lieBracket_swap, add_comm]
simp
