English
Remarks on minimal required smoothness for the bracket identity to hold in manifold contexts.
Русский
Замечания о минимальной гладкости, необходимой для соблюдения тождества скобки на многообразиях.
LaTeX
$$$\text{minSmoothness}(\mathbb{K}, n)$ governs bracket identities$$
Lean4
/-- The Lie bracket of vector fields in manifolds satisfies the Leibniz identity
`[U, [V, W]] = [[U, V], W] + [V, [U, W]]` (also called Jacobi identity). -/
theorem leibniz_identity_mlieBracket_apply {U V W : Π (x : M), TangentSpace I x} {x : M}
(hU : ContMDiffAt I I.tangent (minSmoothness 𝕜 2) (fun x ↦ (U x : TangentBundle I M)) x)
(hV : ContMDiffAt I I.tangent (minSmoothness 𝕜 2) (fun x ↦ (V x : TangentBundle I M)) x)
(hW : ContMDiffAt I I.tangent (minSmoothness 𝕜 2) (fun x ↦ (W x : TangentBundle I M)) x) :
mlieBracket I U (mlieBracket I V W) x =
mlieBracket I (mlieBracket I U V) W x + mlieBracket I V (mlieBracket I U W) x :=
by
simp only [← mlieBracketWithin_univ, ← contMDiffWithinAt_univ] at hU hV hW ⊢
exact leibniz_identity_mlieBracketWithin_apply uniqueMDiffOn_univ (by simp) (mem_univ _) hU hV hW
