English
If two vector fields are ContMDiffAt order n at a point, their bracket is ContMDiffAt order m at that point.
Русский
Если два векторных поля — ContMDiffAt порядка n в точке, их скобка — ContMDiffAt порядка m в той же точке.
LaTeX
$$$\mathrm{ContMDiffAt}(I, I', n, \mathrm{mlieBracketWithin}(I, U, V, \cdot)) x \Rightarrow \mathrm{ContMDiffAt}(I, I', m, \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`. -/
protected theorem _root_.ContMDiffWithinAt.mlieBracketWithin_vectorField [IsManifold I (n + 1) M] {m : WithTop ℕ∞}
{U V : Π (x : M), TangentSpace I x} {s : Set M} {x : M}
(hU : ContMDiffWithinAt I I.tangent n (fun x ↦ (U x : TangentBundle I M)) s x)
(hV : ContMDiffWithinAt I I.tangent n (fun x ↦ (V x : TangentBundle I M)) s x) (hs : UniqueMDiffOn I s) (hx : x ∈ s)
(hmn : minSmoothness 𝕜 (m + 1) ≤ n) :
ContMDiffWithinAt I I.tangent m (fun x ↦ (mlieBracketWithin I U V s x : TangentBundle I M)) s x := by
/- The statement is not obvious, since at different points the Lie bracket is defined using
different charts. However, since we know that the Lie bracket is invariant under diffeos, we can
use a single chart to prove the statement. Let `U'` and `V'` denote the pullbacks of `U` and `V`
in the chart around `x`. Then the Lie bracket there is smooth (as it coincides with the vector
space Lie bracket, given by an explicit formula). Pulling back this Lie bracket in `M` gives
locally a smooth function, which coincides with the initial Lie bracket by invariance
under diffeos. -/
have min2 : minSmoothness 𝕜 2 ≤ n + 1 :=
by
apply le_trans _ (add_le_add_right hmn 1)
rw [← minSmoothness_add, add_assoc]
exact minSmoothness_monotone le_add_self
apply contMDiffWithinAt_iff_le_ne_infty.2 (fun m' hm' h'm' ↦ ?_)
have hn : 1 ≤ m' + 1 := le_add_self
have hm'n : m' + 1 ≤ n := le_trans (add_le_add_right hm' 1) (le_minSmoothness.trans hmn)
have pre_mem : (extChartAt I x) ⁻¹' ((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' s) ∈ 𝓝[s] x :=
by
filter_upwards [self_mem_nhdsWithin, nhdsWithin_le_nhds (extChartAt_source_mem_nhds (I := I) x)] with y hy h'y
exact ⟨(extChartAt I x).map_source h'y, by simpa only [mem_preimage, (extChartAt I x).left_inv h'y] using hy⟩
let U' := mpullbackWithin 𝓘(𝕜, E) I (extChartAt I x).symm U (range I)
let V' := mpullbackWithin 𝓘(𝕜, E) I (extChartAt I x).symm V (range I)
have A :
ContDiffWithinAt 𝕜 m' (lieBracketWithin 𝕜 U' V' ((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' s))
((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' s) (extChartAt I x x) :=
ContDiffWithinAt.lieBracketWithin_vectorField
(contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt.1
(contMDiffWithinAt_mpullbackWithin_extChartAt_symm hU hs hx le_rfl))
(contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt.1
(contMDiffWithinAt_mpullbackWithin_extChartAt_symm hV hs hx le_rfl))
(hs.uniqueDiffOn_target_inter x) hm'n (by simp [hx])
have B :
ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent m'
(fun y ↦
(mlieBracketWithin 𝓘(𝕜, E) U' V' ((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' s) y :
TangentBundle 𝓘(𝕜, E) E))
((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' s) (extChartAt I x x) :=
by
rw [← mlieBracketWithin_eq_lieBracketWithin] at A
exact contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt.2 A
have C :
ContMDiffWithinAt I I.tangent m'
(fun y ↦
(mpullback I 𝓘(𝕜, E) (extChartAt I x)
((mlieBracketWithin 𝓘(𝕜, E) U' V' ((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' s))) y :
TangentBundle I M))
s x :=
ContMDiffWithinAt.mpullback_vectorField_of_mem_nhdsWithin_of_eq B (n := m' + 1) contMDiffAt_extChartAt
(isInvertible_mfderiv_extChartAt (mem_extChartAt_source x)) le_rfl pre_mem rfl
apply C.congr_of_eventuallyEq_of_mem _ hx
filter_upwards [eventually_eventually_nhdsWithin.2 pre_mem,
eventually_eventually_nhdsWithin.2 (eventuallyEq_mpullback_mpullbackWithin_extChartAt U),
eventually_eventually_nhdsWithin.2 (eventuallyEq_mpullback_mpullbackWithin_extChartAt V),
eventually_contMDiffWithinAt_mpullbackWithin_extChartAt_symm (hU.of_le hm'n) hs hx (add_le_add_right hm'n 1)
(by simp [h'm']),
eventually_contMDiffWithinAt_mpullbackWithin_extChartAt_symm (hV.of_le hm'n) hs hx (add_le_add_right hm'n 1)
(by simp [h'm']),
nhdsWithin_le_nhds (chart_source_mem_nhds H x), self_mem_nhdsWithin] with y hy hyU hyV h'yU h'yV hy_chart hys
simp only [Bundle.TotalSpace.mk_inj]
rw [mpullback_mlieBracketWithin (h'yU.mdifferentiableWithinAt hn) (h'yV.mdifferentiableWithinAt hn) hs
(contMDiffAt_extChartAt' hy_chart) hys min2 hy]
exact Filter.EventuallyEq.mlieBracketWithin_vectorField_eq_of_mem hyU hyV hys
