English
Pullback version with stricter hypotheses: mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀ = mlieBracketWithin I (mpullbackWithin I I' f V s) (mpullbackWithin I I' f W s) s x₀.
Русский
Подстановка в виде mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀ = mlieBracketWithin I (mpullbackWithin I I' f V s) (mpullbackWithin I I' f W s) s x₀.
LaTeX
$$$\mathrm{mpullbackWithin}(I, I', f, \mathrm{mlieBracketWithin}(I', V, W, t), s, x_0) = \mathrm{mlieBracketWithin}(I, \mathrm{mpullbackWithin}(I, I', f, V, s), \mathrm{mpullbackWithin}(I, I', f, W, s), s, x_0)$$$
Lean4
/-- The pullback commutes with the Lie bracket of vector fields on manifolds. -/
theorem mpullback_mlieBracketWithin {f : M → M'} {V W : Π (x : M'), TangentSpace I' x} {x₀ : M} {s : Set M} {t : Set M'}
(hV : MDifferentiableWithinAt I' I'.tangent (fun x ↦ (V x : TangentBundle I' M')) t (f x₀))
(hW : MDifferentiableWithinAt I' I'.tangent (fun x ↦ (W x : TangentBundle I' M')) t (f x₀)) (hu : UniqueMDiffOn I s)
(hf : ContMDiffAt I I' n f x₀) (hx₀ : x₀ ∈ s) (hn : minSmoothness 𝕜 2 ≤ n) (hst : f ⁻¹' t ∈ 𝓝[s] x₀) :
mpullback I I' f (mlieBracketWithin I' V W t) x₀ =
mlieBracketWithin I (mpullback I I' f V) (mpullback I I' f W) s x₀ :=
by
have : mpullback I I' f (mlieBracketWithin I' V W t) x₀ = mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀ :=
by
simp only [mpullback, mpullbackWithin]
congr
apply (mfderivWithin_eq_mfderiv (hu _ hx₀) _).symm
exact hf.mdifferentiableAt (one_le_two.trans (le_minSmoothness.trans hn))
rw [this,
mpullbackWithin_mlieBracketWithin' hV hW hu uniqueMDiffOn_univ hf.contMDiffWithinAt hx₀ hn hst (by simp)
(subset_univ _)]
apply Filter.EventuallyEq.mlieBracketWithin_vectorField_of_insert
· rw [insert_eq_of_mem hx₀]
filter_upwards [nhdsWithin_le_nhds
((contMDiffAt_iff_contMDiffAt_nhds (by simp)).1 (hf.of_le (le_minSmoothness.trans hn))),
self_mem_nhdsWithin] with y hy h'y
simp only [mpullback, mpullbackWithin]
congr
apply mfderivWithin_eq_mfderiv (hu _ h'y)
exact hy.mdifferentiableAt one_le_two
· rw [insert_eq_of_mem hx₀]
filter_upwards [nhdsWithin_le_nhds
((contMDiffAt_iff_contMDiffAt_nhds (by simp)).1 (hf.of_le (le_minSmoothness.trans hn))),
self_mem_nhdsWithin] with y hy h'y
simp only [mpullback, mpullbackWithin]
congr
apply mfderivWithin_eq_mfderiv (hu _ h'y)
exact hy.mdifferentiableAt one_le_two
