ODEs.ODE_properties

Core ODE definitions and continuous-dependence theorems used throughout the stability track.

Main declarations

• IsIntegralSolution — integral formulation of an ODE solution on a time interval.
• IntervalIntegrable_of_lipschitz — integrability of s ↦ f(s, z(s)) from joint continuity.
• continuous_dependence_ODE (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 (Theorem 3.5) — uniform ε-bound when both the initial perturbation ‖z₀ − y₀‖ and the forcing ‖g‖ are bounded by α.

def IsIntegralSolution {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (t₀ t₁ : ℝ) (x : ℝ → E) (x₀ : E) (F : ℝ → E → E) : Prop

An integral solution of ẋ = F(t, x) on [t₀, t₁] with initial value x₀: for every t ∈ [t₀, t₁], x(t) = x₀ + ∫_{t₀}^{t} F(s, x(s)) ds.

Equations

• IsIntegralSolution t₀ t₁ x x₀ F = ∀ t ∈ Set.Icc t₀ t₁, x t = x₀ + ∫ (s : ℝ) in t₀..t, F s (x s)

theorem IntervalIntegrable_of_lipschitz {E : Type u_1} [NormedAddCommGroup E] {t₀ t₁ : ℝ} (hle : t₀ ≤ t₁) {f : ℝ → E → E} {z : ℝ → E} (hf_cont : Continuous fun (p : ℝ × E) => f p.1 p.2) (hz : ContinuousOn z (Set.Icc t₀ t₁)) : IntervalIntegrable (fun (s : ℝ) => f s (z s)) MeasureTheory.volume t₀ t₁

s ↦ f(s, z(s)) is interval-integrable on [t₀, t₁] when f is jointly continuous and z is continuous on [t₀, t₁].

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 μ : ℝ} (ht : t₀ ≤ t₁) (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.Icc t₀ t₁)) (hz_cont : ContinuousOn z (Set.Icc 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.Icc t₀ t₁, LipschitzWith ⟨L, ⋯⟩ (f t)) (hg : ∀ t ∈ Set.Icc t₀ t₁, ∀ (x : E), ‖g t x‖ ≤ μ) (t : ℝ) : t ∈ Set.Icc t₀ t₁ → ‖y t - z t‖ ≤ ‖y₀ - z₀‖ * Real.exp (L * (t - t₀)) + μ / L * (Real.exp (L * (t - t₀)) - 1)

Theorem 3.4 (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 all t ∈ [t₀, t₁]:

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

We work globally on [t₀, t₁] (rather than on a local domain W ⊂ ℝⁿ) to avoid local-extension boilerplate.

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‖ ≤ ε

Theorem 3.5 (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.

axiom scalar_ode_exists_interval (g : ℝ → ℝ → ℝ) (L : ℝ) (hL : 0 < L) (hg_cont : Continuous (Function.uncurry g)) (hg_lip : ∀ (t : ℝ), LipschitzWith ⟨L, ⋯⟩ (g t)) {t₀ t₁ x₀ : ℝ} (ht : t₀ ≤ t₁) : ∃ (z : ℝ → ℝ), IsIntegralSolution t₀ t₁ z x₀ g ∧ ContinuousOn z (Set.Icc t₀ t₁) ∧ ∀ s ∈ Set.Ico t₀ t₁, HasDerivWithinAt z (g s (z s)) (Set.Ici s) s

Picard-Lindelöf for scalar ODEs on compact intervals.

For a jointly continuous right-hand side g : ℝ → ℝ → ℝ that is globally Lipschitz in the state variable (uniformly in time), for any compact interval [t₀, t₁] and initial value x₀ : ℝ, there exists an integral solution z that is continuous and has right derivatives matching g on [t₀, t₁).

This is the scalar, compact-interval instance of the Picard-Lindelöf theorem, which holds because globally Lipschitz continuity prevents finite-time blowup.