English
If two vector fields are ContMDiffAt with sufficient smoothness, their Lie bracket is ContMDiffAt of lower order.
Русский
Если два векторных поля обладают достаточной гладкостью, их скобка Ли гладкая меньшего порядка.
LaTeX
$$$\mathrm{ContMDiffAt}(I, I.tangent, m, \lambda x. (\mathrm{mlieBracket}(I, U, V) x))$$$
Lean4
/-- If two vector fields are `C^n` with `n ≥ m + 1`, then their Lie bracket is `C^m`. -/
theorem _root_.ContDiff.mlieBracket_vectorField {m n : ℕ∞} [IsManifold I (n + 1) M] {U V : Π (x : M), TangentSpace I x}
(hU : ContMDiff I I.tangent n (fun x ↦ (U x : TangentBundle I M)))
(hV : ContMDiff I I.tangent n (fun x ↦ (V x : TangentBundle I M))) (hmn : minSmoothness 𝕜 (m + 1) ≤ n) :
ContMDiff I I.tangent m (fun x ↦ (mlieBracket I U V x : TangentBundle I M)) :=
by
simp only [← contMDiffOn_univ] at hU hV ⊢
exact hU.mlieBracketWithin_vectorField hV uniqueMDiffOn_univ hmn
