English
There exists a neighborhood of t0 in which γ has a derivative in charts with tangent coordinate change along v.
Русский
Существуют окрестности t0, в которых γ имеет производную в координатах через касательное изменение вдоль v.
LaTeX
$$$\forall \text{neighborhood } U \ni t_0, \ HasDerivAt ( (\mathrm{extChartAt} I (\gamma(t_0)) \circ \gamma) )( \text{tangentCoordChange}(I,\gamma(t),(\gamma(t_0)))\big( v(\gamma(t)) \big), t).$$$
Lean4
theorem eventually_hasDerivAt (hγ : IsMIntegralCurveAt γ v t₀) :
∀ᶠ t in 𝓝 t₀, HasDerivAt ((extChartAt I (γ t₀)) ∘ γ) (tangentCoordChange I (γ t) (γ t₀) (γ t) (v (γ t))) t :=
by
apply
eventually_mem_nhds_iff.mpr (hγ.continuousAt.preimage_mem_nhds (extChartAt_source_mem_nhds (I := I) _)) |>.and
hγ |>.mono
rintro t ⟨ht1, ht2⟩
have hsrc := mem_of_mem_nhds ht1
rw [mem_preimage, extChartAt_source I (γ t₀)] at hsrc
rw [hasDerivAt_iff_hasFDerivAt, ← hasMFDerivAt_iff_hasFDerivAt]
apply (HasMFDerivAt.comp t (hasMFDerivAt_extChartAt (I := I) hsrc) ht2).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
