English
Product rule with scalar field: [V, f·W] = (Df f)(V)·W + f·[V, W].
Русский
Производное правило с умножением на скаляр: [V, f·W] = (Df f)(V)·W + f·[V, W].
LaTeX
$$$\mathrm{lieBracket}(V, (x \mapsto f(x)W(x))) = (fderiv\mathbb{K} f)(Vx) \cdot Wx + f(x) \cdot \mathrm{lieBracket}(V, W)(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 lieBracket_smul_right {f : E → 𝕜} (hf : DifferentiableAt 𝕜 f x) (hW : DifferentiableAt 𝕜 W x) :
lieBracket 𝕜 V (fun y ↦ f y • W y) x = (fderiv 𝕜 f x) (V x) • (W x) + (f x) • lieBracket 𝕜 V W x :=
by
simp_rw [← differentiableWithinAt_univ, ← lieBracketWithin_univ, fderiv] at hW hf ⊢
exact lieBracketWithin_smul_right hf hW uniqueDiffWithinAt_univ
