English
In a boundaryless manifold, a C1 vector field with a C1 tangent component admits a local integral curve at any interior initial point.
Русский
На безграничной (без границы) многообразии векторное поле, удовлетворяющее условиям непрерывности и дифференцируемости, имеет локальную интегральную кривую в начальной interior точки.
LaTeX
$$$\exists \gamma:\mathbb{R}\to M,\; \gamma(t_0)=x_0 \land \mathrm{IsMIntegralCurveAt}(\gamma,v,t_0).$$$
Lean4
/-- Existence of local integral curves for a $C^1$ vector field at interior points of a `C^1`
manifold. -/
theorem exists_isMIntegralCurveAt_of_contMDiffAt [CompleteSpace E]
(hv : ContMDiffAt I I.tangent 1 (fun x ↦ (⟨x, v x⟩ : TangentBundle I M)) x₀) (hx : I.IsInteriorPoint x₀) :
∃ γ : ℝ → M, γ t₀ = x₀ ∧ IsMIntegralCurveAt γ v t₀ := by
-- express the differentiability of the vector field `v` in the local chart
rw [contMDiffAt_iff] at hv
obtain ⟨_, hv⟩ := hv
obtain ⟨f, hf1, hf2⟩ :=
hv.contDiffAt
(range_mem_nhds_isInteriorPoint hx) |>.snd.exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt₀
t₀
simp_rw [← Real.ball_eq_Ioo, ← Metric.eventually_nhds_iff_ball] at hf2
have ⟨a, ha, hf2'⟩ := Metric.eventually_nhds_iff_ball.mp hf2
have hcont := (hf2' t₀ (Metric.mem_ball_self ha)).continuousAt
rw [continuousAt_def, hf1] at hcont
have hnhds : f ⁻¹' (interior (extChartAt I x₀).target) ∈ 𝓝 t₀ :=
hcont _ (isOpen_interior.mem_nhds ((I.isInteriorPoint_iff).mp hx))
rw [← eventually_mem_nhds_iff] at hnhds
obtain ⟨s, hs, haux⟩ := (hf2.and hnhds).exists_mem
refine
⟨(extChartAt I x₀).symm ∘ f,
Eq.symm (by rw [Function.comp_apply, hf1, PartialEquiv.left_inv _ (mem_extChartAt_source ..)]),
isMIntegralCurveAt_iff.mpr ⟨s, hs, ?_⟩⟩
intro t ht
let xₜ : M :=
(extChartAt I x₀).symm
(f t) -- `xₜ := γ t`
have h :
HasDerivAt f (x := t) <|
fderivWithin ℝ (extChartAt I x₀ ∘ (extChartAt I xₜ).symm) (range I) (extChartAt I xₜ xₜ) (v xₜ) :=
(haux t ht).1
rw [← tangentCoordChange_def] at h
have hf3 := mem_preimage.mp <| mem_of_mem_nhds (haux t ht).2
have hf3' := mem_of_mem_of_subset hf3 interior_subset
have hft1 := mem_preimage.mp <| mem_of_mem_of_subset hf3' (extChartAt I x₀).target_subset_preimage_source
have hft2 := mem_extChartAt_source (I := I) xₜ
apply HasMFDerivAt.hasMFDerivWithinAt
refine ⟨(continuousAt_extChartAt_symm'' hf3').comp h.continuousAt, HasDerivWithinAt.hasFDerivWithinAt ?_⟩
simp only [mfld_simps, hasDerivWithinAt_univ]
change HasDerivAt ((extChartAt I xₜ ∘ (extChartAt I x₀).symm) ∘ f) (v xₜ) t
rw [← tangentCoordChange_self (I := I) (x := xₜ) (z := xₜ) (v := v xₜ) hft2, ←
tangentCoordChange_comp (x := x₀) ⟨⟨hft2, hft1⟩, hft2⟩]
apply HasFDerivAt.comp_hasDerivAt _ _ h
apply
HasFDerivWithinAt.hasFDerivAt (s := range I) _ <|
mem_nhds_iff.mpr
⟨interior (extChartAt I x₀).target, subset_trans interior_subset (extChartAt_target_subset_range ..),
isOpen_interior, hf3⟩
rw [← (extChartAt I x₀).right_inv hf3']
exact hasFDerivWithinAt_tangentCoordChange ⟨hft1, hft2⟩
