English
If γ is an integral curve on s, then under a chart, γ has a derivative within s given by the tangent change along v.
Русский
Если γ интегральная кривая на s, то в локальной системе координат производная γ внутри s равна соответствующему касательному изменению вдоль v.
LaTeX
$$$\text{HasDerivWithinAt}( (\text{extChartAt } I (\gamma(t_0))) \circ \gamma,\; \text{tangentCoordChange}(I,\gamma(t),(\gamma(t_0)))(v(\gamma(t))),\; s,\; t_0).$$$
Lean4
/-- If `γ` is an integral curve of a vector field `v`, then `γ t` is tangent to `v (γ t)` when
expressed in the local chart around the initial point `γ t₀`. -/
theorem hasDerivWithinAt (hγ : IsMIntegralCurveOn γ v s) {t : ℝ} (ht : t ∈ s)
(hsrc : γ t ∈ (extChartAt I (γ t₀)).source) :
HasDerivWithinAt ((extChartAt I (γ t₀)) ∘ γ) (tangentCoordChange I (γ t) (γ t₀) (γ t) (v (γ t))) s t := by
-- turn `HasDerivWithinAt` into comp of `HasMFDerivWithinAt`
replace hsrc := extChartAt_source I (γ t₀) ▸ hsrc
rw [hasDerivWithinAt_iff_hasFDerivWithinAt, ← hasMFDerivWithinAt_iff_hasFDerivWithinAt]
apply
(HasMFDerivWithinAt.comp t (hasMFDerivWithinAt_extChartAt (I := I) hsrc) (hγ _ ht)
(Set.subset_preimage_image _ _)).congr_mfderiv
rw [ContinuousLinearMap.ext_iff]
intro a
rw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.smulRight_apply, map_smul, ←
ContinuousLinearMap.one_apply (R₁ := ℝ) a, ← ContinuousLinearMap.smulRight_apply,
mfderiv_chartAt_eq_tangentCoordChange hsrc]
rfl
