English
Under appropriate differentiability and symmetry hypotheses, the Leibniz identity holds for the Lie bracket within a set: [U, [V, W]] = [[U, V], W] + [V, [U, W]] within s at x.
Русский
При заданных условиях дифференцируемости и симметричности двойной производной скобка Ли внутри множества удовлетворяет тождеству Лейбница: [U,[V,W]] = [[U,V],W] + [V,[U,W]] внутри s в точке x.
LaTeX
$$$ lieBracketWithin 𝕜 U (lieBracketWithin 𝕜 V W s) s x = lieBracketWithin 𝕜 (lieBracketWithin 𝕜 U V s) W s x + lieBracketWithin 𝕜 V (lieBracketWithin 𝕜 U W s) s x $$$
Lean4
/-- The Lie bracket of vector fields in vector spaces satisfies the Leibniz identity
`[U, [V, W]] = [[U, V], W] + [V, [U, W]]`. -/
theorem leibniz_identity_lieBracketWithin (hn : minSmoothness 𝕜 2 ≤ n) {U V W : E → E} {s : Set E} {x : E}
(hs : UniqueDiffOn 𝕜 s) (h'x : x ∈ closure (interior s)) (hx : x ∈ s) (hU : ContDiffWithinAt 𝕜 n U s x)
(hV : ContDiffWithinAt 𝕜 n V s x) (hW : ContDiffWithinAt 𝕜 n W s x) :
lieBracketWithin 𝕜 U (lieBracketWithin 𝕜 V W s) s x =
lieBracketWithin 𝕜 (lieBracketWithin 𝕜 U V s) W s x + lieBracketWithin 𝕜 V (lieBracketWithin 𝕜 U W s) s x :=
by
apply
leibniz_identity_lieBracketWithin_of_isSymmSndFDerivWithinAt hs hx (hU.of_le (le_minSmoothness.trans hn))
(hV.of_le (le_minSmoothness.trans hn)) (hW.of_le (le_minSmoothness.trans hn))
· exact hU.isSymmSndFDerivWithinAt hn hs h'x hx
· exact hV.isSymmSndFDerivWithinAt hn hs h'x hx
· exact hW.isSymmSndFDerivWithinAt hn hs h'x hx
