feat(Analysis/ODE/GlobalExistence): prove uniqueness and semigroup properties

[AdoHaha]

Couple of proofs around existence theory

[mcdoll]

Thanks. Some comments below.

Can you also split the input-output changes into a separate PR?

[mcdoll]

Suggested change

	unfold γ₁ γ₂
	simp [hΦ.initial]
	simp [γ₁, γ₂, hΦ.initial]

Untested, but if this does not work, use set .. with hγ₁

[mcdoll]

does rw work?

[mcdoll]

same as above

[mcdoll]

Suggested change

	have : γ₂ s = γ₁ s := hs.symm
	rw [this]
	exact hU
	rwa [hs.symm]

?

[mcdoll]

grind should be able to prove this after you established huniv

[mcdoll]

You probably can use ext : 2 and then you don't need congrFun (which should not be used anyway, rw is probably better in this case)

[mcdoll]

Suggested change

	(hf : UniformlyLocallyLipschitz f) (_hf' : Continuous f) :
	(hf : UniformlyLocallyLipschitz f) :

[AdoHaha]

Thanks for the review — all comments addressed, and the input/output change is now split out as #71.

New commit address_globalexistence_comments:

• add_apply / add_apply: ht₀ is now simp [γ₁, γ₂, …]; the closing congrFun is replaced by rw.
• eq_of_uniformlyLocallyLipschitz: hU' is now rwa [hs.symm]; the closing is grind.
  (Note: grind cannot consume the set equality {s | γ₁ s = γ₂ s} = Set.univ in the pinned Mathlib — grind [Set.ext_iff] errors — so huniv is stated pointwise and the set equality is converted with simpa [Set.ext_iff]. The clopen argument is otherwise unchanged.)
• unique: closed with ext t₀ x₀ + rw, and the unused Continuous f hypothesis is dropped.
• Also replaced the last congrFun in the file (in the pre-existing add_apply') by rw, for consistency; this is why the diff touches a declaration that predates the PR.

The InputOutput proofs (isGraph_inputOutput, isGraph_inputState) now live in #71.

[mcdoll]

Suggested change

	have hf_curve : IsIntegralCurve γ₁ (fun _ ↦ f) := (hΦ (Φ x t')).1
	have hg_curve : IsIntegralCurve γ₂ (fun _ ↦ f) := (hΦ x).1.comp_add t'
	have hf : IsIntegralCurve γ₁ (fun _ ↦ f) := (hΦ (Φ x t')).1
	have hg : IsIntegralCurve γ₂ (fun _ ↦ f) := (hΦ x).1.comp_add t'

[mcdoll]

Suggested change

	have heq := IsIntegralCurve.eq_of_uniformlyLocallyLipschitz hv.uniformlyLocallyLipschitz
	hf_curve hg_curve ht₀
	have heq := hf.eq_of_uniformlyLocallyLipschitz hv.uniformlyLocallyLipschitz hg ht₀

[mcdoll]

Suggested change

	have hf_curve : IsIntegralCurve γ₁ (fun _ ↦ f) := hΦ.isIntegralCurve 0 (Φ' 0 x t')
	have hg_curve : IsIntegralCurve γ₂ (fun _ ↦ f) := (hΦ.isIntegralCurve 0 x).comp_add t'
	have hf : IsIntegralCurve γ₁ (fun _ ↦ f) := hΦ.isIntegralCurve 0 (Φ' 0 x t')
	have hg : IsIntegralCurve γ₂ (fun _ ↦ f) := (hΦ.isIntegralCurve 0 x).comp_add t'

[mcdoll]

Suggested change

	ext t₀ x₀
	have heq := IsIntegralCurve.eq_of_uniformlyLocallyLipschitz hf
	(hΦ.isIntegralCurve t₀ x₀) (hΦ'.isIntegralCurve t₀ x₀)
	(by rw [hΦ.initial, hΦ'.initial])
	rw [heq]
	ext t₀ x₀ : 2
	apply (hΦ.isIntegralCurve t₀ x₀).eq_of_uniformlyLocallyLipschitz hf (hΦ'.isIntegralCurve t₀ x₀)
	rw [hΦ.initial, hΦ'.initial]

[mcdoll]

Suggested change

	have heq_ev := IsIntegralCurveAt.eventuallyEq hfK
	(h1.isIntegralCurveAt s) hU1
	(h2.isIntegralCurveAt s) hU2
	hs
	exact heq_ev.mono (fun s' hs' ↦ hs')
	have huniv : ∀ s : ℝ, γ₁ s = γ₂ s := by
	have h : {s : ℝ | γ₁ s = γ₂ s} = Set.univ := by
	refine isClopen_iff.mp ⟨hclosed, hopen⟩ |>.resolve_left ?_
	intro hempty
	have : t₀ ∈ ({s : ℝ | γ₁ s = γ₂ s} : Set ℝ) := heq
	rw [hempty] at this
	exact this
	simpa [Set.ext_iff] using h
	have heq_ev := (h1.isIntegralCurveAt s).eventuallyEq hfK hU1 (h2.isIntegralCurveAt s) hU2 hs
	exact heq_ev.mono (fun s' hs' ↦ hs')
	have huniv : ∀ s : ℝ, γ₁ s = γ₂ s := by
	suffices {s : ℝ | γ₁ s = γ₂ s} = Set.univ by simpa [Set.ext_iff]
	refine isClopen_iff.mp ⟨hclosed, hopen⟩ |>.resolve_left ?_
	have : t₀ ∈ ({s : ℝ | γ₁ s = γ₂ s} : Set ℝ) := heq
	grind

[AdoHaha]

Round-2 comments applied — thanks.

• add_apply' / add_apply: hf_curve/hg_curve renamed to hf/hg, and the uniqueness step is now hf.eq_of_uniformlyLocallyLipschitz hv.uniformlyLocallyLipschitz hg ht₀ (generalized dot notation).
• eq_of_uniformlyLocallyLipschitz: the local-equality call now uses (h1.isIntegralCurveAt s).eventuallyEq hfK hU1 (h2.isIntegralCurveAt s) hU2 hs; huniv is shortened to suffices … = Set.univ by simpa [Set.ext_iff] followed by grind.
• unique: body is now ext t₀ x₀ : 2, apply (hΦ.isIntegralCurve t₀ x₀).eq_of_uniformlyLocallyLipschitz hf (hΦ'.isIntegralCurve t₀ x₀), rw [hΦ.initial, hΦ'.initial].

Commit address_globalexistence_comments_2. Build, lint, lake env lean, and the axiom audit are all clean.