English
Let I be a model with corners and M a manifold. Given a smoothly varying tangent field V along M defined on a subset s, if V is smoothly varying within s, and s has a unique-differentiability property, then the pullback of V along extChartAt(x) via mpullbackWithin to the model space remains smoothly varying of order m in a neighborhood of x contained in s.
Русский
Пусть I — модуль с углами, M — многообразие. Пусть вдоль M на подмножестве s задано гладко зависящее векторное поле V. Если V гладко зависит по внутренности s и s удовлетворяет свойству уникальной дифференцируемости, то его отклонение через отображение pullback внутри extChartAt(x) остаётся гладким порядка m в окрестности точки x, лежащей в s.
LaTeX
$$$\forall x \in s,\; [\text{ContMDiffWithinAt}(I,\;I.{\text{tangent}},\;m)(x)\;\wedge\; \text{UniqueMDiffOn}(I,s) ] \Rightarrow \\ \exists \mathcal{N} \subset s:\; x \in \mathcal{N} \wedge \\ \forall y \in \mathcal{N}, \; \text{ContMDiffWithinAt}_{\mathcal{I}(\mathbb{K},E)\;\mathcal{I}(\mathbb{K},E).tangent}(m)\; (z \mapsto \mathrm{mpullbackWithin}_{\mathcal{I}}(\mathrm{extChartAt}\; I \; x)^{\,-1} V(y))(z). $$$
Lean4
theorem eventually_contMDiffWithinAt_mpullbackWithin_extChartAt_symm {V : Π (x : M), TangentSpace I x}
(hV : ContMDiffWithinAt I I.tangent m (fun x ↦ (V x : TangentBundle I M)) s x) (hs : UniqueMDiffOn I s) (hx : x ∈ s)
(hmn : m + 1 ≤ n) (hm : m ≠ ∞) :
∀ᶠ y in 𝓝[s] x,
ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent m
(fun z ↦ (mpullbackWithin 𝓘(𝕜, E) I (extChartAt I x).symm V (range I) z : TangentBundle 𝓘(𝕜, E) E))
((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' s) (extChartAt I x y) :=
by
have T :=
nhdsWithin_mono _ (subset_insert _ _)
((contMDiffWithinAt_iff_contMDiffWithinAt_nhdsWithin hm).1
(contMDiffWithinAt_mpullbackWithin_extChartAt_symm hV hs hx hmn))
have A := (continuousAt_extChartAt (I := I) x).continuousWithinAt.preimage_mem_nhdsWithin'' T rfl
apply (nhdsWithin_le_iff.2 _) A
filter_upwards [self_mem_nhdsWithin, nhdsWithin_le_nhds (extChartAt_source_mem_nhds (I := I) x)] with y hy h'y
simp only [mfld_simps] at hy h'y
simp [hy, h'y]
