ODEs.ODE_properties

Existence and continuous-dependence theorems used throughout the stability track.

The integral formulation IsIntegralSolution and its dictionary with Mathlib's IsIntegralCurveOn are general facts about ODE solutions with no control content; they live in Analysis/IntegralCurves.lean, which this file imports.

Main declarations

• ContDiffAt.exists_isIntegralCurveOn_Icc — local existence from a C¹ field.
• continuous_dependence_ODE (Khalil, Theorem 3.4) — quantitative bound on ‖y(t) − z(t)‖ when y solves ẏ = f and z solves the perturbed system ż = f + g.
• continuous_dependence_parameters (Khalil, Theorem 3.5) — uniform ε-bound when both the initial perturbation ‖z₀ − y₀‖ and the forcing ‖g‖ are bounded by α.

Reference: Khalil, Nonlinear Systems (3rd ed.), Chapter 3.

theorem ContDiffAt.exists_isIntegralCurveOn_Icc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {g : E → E} {x₀ : E} (hg : ContDiffAt ℝ 1 g x₀) : ∃ (T : ℝ) (φ : ℝ → E), 0 < T ∧ φ 0 = x₀ ∧ IsIntegralCurveOn φ (fun (x : ℝ) (y : E) => g y) (Set.Icc 0 T)

A C¹ vector field admits a nontrivial solution segment from every point at which it is C¹. The anchor 0 is a construction choice, not a restriction: by time invariance a segment from any anchor follows.

Reference: the Picard--Lindelöf local existence theorem.

theorem continuous_dependence_ODE {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {t₀ t₁ : ℝ} {f g : ℝ → E → E} {y z : ℝ → E} {y₀ z₀ : E} {L μ : ℝ} (hL : 0 < L) (hy : IsIntegralSolution t₀ t₁ y y₀ f) (hz : IsIntegralSolution t₀ t₁ z z₀ fun (s : ℝ) (x : E) => f s x + g s x) (hy_cont : ContinuousOn y (Set.uIcc t₀ t₁)) (hz_cont : ContinuousOn z (Set.uIcc t₀ t₁)) (hf_cont : Continuous fun (p : ℝ × E) => f p.1 p.2) (hgz : IntervalIntegrable (fun (s : ℝ) => g s (z s)) MeasureTheory.volume t₀ t₁) (hLip : ∀ t ∈ Set.uIcc t₀ t₁, LipschitzWith ⟨L, ⋯⟩ (f t)) (hg : ∀ t ∈ Set.uIcc t₀ t₁, ∀ (x : E), ‖g t x‖ ≤ μ) (t : ℝ) : t ∈ Set.uIcc t₀ t₁ → ‖y t - z t‖ ≤ ‖y₀ - z₀‖ * Real.exp (L * |t - t₀|) + μ / L * (Real.exp (L * |t - t₀|) - 1)

Continuous dependence on initial states and parameters.

If y is an integral solution of ẏ = f(t, y) and z is an integral solution of ż = f(t, z) + g(t, z), with f Lipschitz in the state with constant L and g uniformly bounded by μ, then for t on either side of t₀:

‖y(t) − z(t)‖ ≤ ‖y₀ − z₀‖ · exp(L|t−t₀|) + (μ/L) · (exp(L|t−t₀|) − 1).

We work globally on the segment between t₀ and t₁ (rather than on a local domain W ⊂ ℝⁿ) to avoid local-extension boilerplate.

Proof: the Gronwall bootstrap itself (integrability setup, base inequality, shift into Gronwall form, apply gronwall_const) is inherently forward-marching — it is proved once, as the general private lemma continuous_dependence_forward, and reused twice: directly for t₀ ≤ t₁, and via the time-reflection σ ↦ t₀ + t₁ - σ (applied to y, z, f, g) for t₁ ≤ t₀, which turns the backward instance into a forward one on [t₁, t₀].

Reference: Khalil, Nonlinear Systems (3rd ed.), Theorem 3.4.

theorem continuous_dependence_parameters {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {t₀ t₁ : ℝ} {f g : ℝ → E → E} {y z : ℝ → E} {y₀ z₀ : E} {L α ε : ℝ} (ht : t₀ ≤ t₁) (hL : 0 < L) (hα : 0 < α) (hαε : α * (1 + 1 / L) * Real.exp (L * (t₁ - t₀)) ≤ ε) (hy : IsIntegralSolution t₀ t₁ y y₀ f) (hz : IsIntegralSolution t₀ t₁ z z₀ fun (s : ℝ) (x : E) => f s x + g s x) (hy_cont : ContinuousOn y (Set.Icc t₀ t₁)) (hz_cont : ContinuousOn z (Set.Icc t₀ t₁)) (hf_cont : Continuous fun (p : ℝ × E) => f p.1 p.2) (hg_cont : Continuous fun (p : ℝ × E) => g p.1 p.2) (hLip : ∀ t ∈ Set.Icc t₀ t₁, LipschitzWith ⟨L, ⋯⟩ (f t)) (hg : ∀ t ∈ Set.Icc t₀ t₁, ∀ (x : E), ‖g t x‖ ≤ α) (hz₀ : ‖z₀ - y₀‖ ≤ α) (t : ℝ) : t ∈ Set.Icc t₀ t₁ → ‖y t - z t‖ ≤ ε

Continuous dependence on parameters.

A uniform ε-bound: if ‖z₀ − y₀‖ ≤ α and ‖g(t, x)‖ ≤ α for all t, x, and α · (1 + 1/L) · exp(L(t₁−t₀)) ≤ ε, then ‖y(t) − z(t)‖ ≤ ε for all t ∈ [t₀, t₁].

λ-dependence is modeled via the perturbation term g (i.e., g t x = f_λ t x − f t x). The α-condition plays the role of δ from the classical statement.

Reference: Khalil, Nonlinear Systems (3rd ed.), Theorem 3.5.