English
If two integral curves γ and γ′ share the same initial value at t0 and satisfy the same differential equation in a neighborhood, they are equal on a neighborhood of t0.
Русский
Если два интегральных кривых γ и γ′ имеют одно и то же начальное значение в t0 и удовлетворяют одному и тому же дифференциальному уравнению в окрестности, то они совпадают в окрестности t0.
LaTeX
$$$IIsMIntegralCurveAt(\gamma,v,t_0) \land IIsMIntegralCurveAt(\gamma',v,t_0) \land \gamma(t_0)=\gamma'(t_0) \Rightarrow γ=^{𝓝 t_0} γ'.$$$
Lean4
/-- Local integral curves are unique.
If a $C^1$ vector field `v` admits two local integral curves `γ γ' : ℝ → M` at `t₀` with
`γ t₀ = γ' t₀`, then `γ` and `γ'` agree on some open interval containing `t₀`. -/
theorem isMIntegralCurveAt_eventuallyEq_of_contMDiffAt (hγt₀ : I.IsInteriorPoint (γ t₀))
(hv : ContMDiffAt I I.tangent 1 (fun x ↦ (⟨x, v x⟩ : TangentBundle I M)) (γ t₀)) (hγ : IsMIntegralCurveAt γ v t₀)
(hγ' : IsMIntegralCurveAt γ' v t₀) (h : γ t₀ = γ' t₀) : γ =ᶠ[𝓝 t₀] γ' := by
-- first define `v'` as the vector field expressed in the local chart around `γ t₀`
-- this is basically what the function looks like when `hv` is unfolded
set v' : E → E := fun x ↦
tangentCoordChange I ((extChartAt I (γ t₀)).symm x) (γ t₀) ((extChartAt I (γ t₀)).symm x)
(v ((extChartAt I (γ t₀)).symm x)) with
hv'
rw [contMDiffAt_iff] at hv
obtain ⟨_, hv⟩ := hv
obtain ⟨K, s, hs, hlip⟩ : ∃ K, ∃ s ∈ 𝓝 _, LipschitzOnWith K v' s :=
(hv.contDiffAt (range_mem_nhds_isInteriorPoint hγt₀)).snd.exists_lipschitzOnWith
have hlip (t : ℝ) : LipschitzOnWith K ((fun _ ↦ v') t) ((fun _ ↦ s) t) := hlip
have hsrc {g} (hg : IsMIntegralCurveAt g v t₀) : ∀ᶠ t in 𝓝 t₀, g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t :=
eventually_mem_nhds_iff.mpr <| continuousAt_def.mp hg.continuousAt _ <| extChartAt_source_mem_nhds (g t₀)
have hmem {g : ℝ → M} {t} (ht : g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t) : g t ∈ (extChartAt I (g t₀)).source :=
mem_preimage.mp <| mem_of_mem_nhds ht
have hdrv {g} (hg : IsMIntegralCurveAt g v t₀) (h' : γ t₀ = g t₀) :
∀ᶠ t in 𝓝 t₀,
HasDerivAt ((extChartAt I (g t₀)) ∘ g) ((fun _ ↦ v') t (((extChartAt I (g t₀)) ∘ g) t)) t ∧
((extChartAt I (g t₀)) ∘ g) t ∈ (fun _ ↦ s) t :=
by
apply Filter.Eventually.and
· apply (hsrc hg |>.and hg.eventually_hasDerivAt).mono
rintro t ⟨ht1, ht2⟩
rw [hv', h']
apply ht2.congr_deriv
congr <;> rw [Function.comp_apply, PartialEquiv.left_inv _ (hmem ht1)]
· apply ((continuousAt_extChartAt (g t₀)).comp hg.continuousAt).preimage_mem_nhds
rw [Function.comp_apply, ← h']
exact hs
have heq {g} (hg : IsMIntegralCurveAt g v t₀) : g =ᶠ[𝓝 t₀] (extChartAt I (g t₀)).symm ∘ ↑(extChartAt I (g t₀)) ∘ g :=
by
apply (hsrc hg).mono
intro t ht
rw [Function.comp_apply, Function.comp_apply, PartialEquiv.left_inv _ (hmem ht)]
-- main proof
suffices (extChartAt I (γ t₀)) ∘ γ =ᶠ[𝓝 t₀] (extChartAt I (γ' t₀)) ∘ γ' from
(heq hγ).trans <| (this.fun_comp (extChartAt I (γ t₀)).symm).trans (h ▸ (heq hγ').symm)
exact
ODE_solution_unique_of_eventually (.of_forall hlip) (hdrv hγ rfl) (hdrv hγ' h)
(by rw [Function.comp_apply, Function.comp_apply, h])
