ODEs.ComparisonLemma

The comparison lemma for scalar ODEs: if u is an exact solution of u̇ = f(t, u) with u(t₀) = u₀, and v is continuous with upper Dini derivative satisfying D⁺v(t) ≤ f(t, v(t)) and v(t₀) ≤ u₀, then v(t) ≤ u(t) for all t ∈ [t₀, t₁].

Proof strategy (Khalil, Appendix C.2)

• Claim 1 (comparison_claim_1): For any perturbed solution z of ż = f(t, z) + λ with λ > 0, we have v(t) ≤ z(t) on [t₀, t₁]. Proved by contradiction: assuming the set S = {s | v(s) = z(s)} has a supremum a < t_bad (where v(t_bad) > z(t_bad)), the Dini derivative inequality at a forces f(a, z(a)) + λ ≤ f(a, v(a)), contradicting v(a) = z(a) and λ > 0.

• Claim 2 (comparison_lemma): v(t) ≤ u(t) follows by sending λ → 0. For each λ > 0, v(t) ≤ z_λ(t) by Claim 1, and z_λ(t) ≤ u(t) + ε/2 by the continuous-dependence estimate (Khalil, Theorem 3.5). Since ε > 0 is arbitrary, v(t) ≤ u(t).

Main declarations

• isIntegralSolution_of_hasDerivAt — converts a pointwise derivative condition into an integral solution.
• comparison_lemma — the full comparison inequality v ≤ u.

comparison_claim_1 is a private step of the latter's proof.

Integral solution helper

theorem isIntegralSolution_of_hasDerivAt {f : ℝ → ℝ → ℝ} {u : ℝ → ℝ} {t₀ t₁ u₀ : ℝ} (ht : t₀ ≤ t₁) (hu_deriv : ∀ t ∈ Set.Ioo t₀ t₁, HasDerivAt u (f t (u t)) t) (hu_cont : ContinuousOn u (Set.Icc t₀ t₁)) (hf_cont : Continuous fun (p : ℝ × ℝ) => f p.1 p.2) (hu₀ : u t₀ = u₀) : IsIntegralSolution t₀ t₁ u u₀ f

Converts a classical (pointwise) ODE solution into an integral solution.

If u has derivative f(t, u(t)) at every interior point of [t₀, t₁], is continuous on [t₀, t₁], and satisfies u(t₀) = u₀, then u is an integral solution in the sense of IsIntegralSolution.

The comparison lemma

theorem comparison_lemma {f : ℝ → ℝ → ℝ} {u v : ℝ → ℝ} {t₀ t₁ u₀ L : ℝ} (ht : t₀ < t₁) (hL : 0 < L) (hf_cont : Continuous fun (p : ℝ × ℝ) => f p.1 p.2) (hLip : ∀ t ∈ Set.Icc t₀ t₁, LipschitzWith ⟨L, ⋯⟩ (f t)) (hu_deriv : ∀ t ∈ Set.Ioo t₀ t₁, HasDerivAt u (f t (u t)) t) (hu_cont : ContinuousOn u (Set.Icc t₀ t₁)) (hu₀ : u t₀ = u₀) (hv_cont : ContinuousOn v (Set.Icc t₀ t₁)) (hDv : ∀ t ∈ Set.Ico t₀ t₁, D⁺ v t ≤ f t (v t)) (hv_bdd : ∀ t ∈ Set.Ico t₀ t₁, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin 0 (Set.Ioi 0)) fun (h : ℝ) => (v (t + h) - v t) / h) (hv₀ : v t₀ ≤ u₀) (hz_exists : ∀ (lam : ℝ), 0 < lam → ∃ (z : ℝ → ℝ), (IsIntegralSolution t₀ t₁ z u₀ fun (s x : ℝ) => f s x + lam) ∧ ContinuousOn z (Set.Icc t₀ t₁) ∧ ∀ s ∈ Set.Ico t₀ t₁, HasDerivWithinAt z (f s (z s) + lam) (Set.Ici s) s) (t : ℝ) : t ∈ Set.Icc t₀ t₁ → v t ≤ u t

Comparison lemma. If u solves u̇ = f(t, u) with u(t₀) = u₀, and v is continuous with D⁺v(t) ≤ f(t, v(t)) and v(t₀) ≤ u₀, then v(t) ≤ u(t) on [t₀, t₁].

Hypotheses:

• f is jointly continuous and globally Lipschitz in the state variable on [t₀, t₁].
• u solves the ODE classically (pointwise derivative).
• v satisfies the Dini subsolution inequality and has bounded difference quotients.
• For each λ > 0, a perturbed solution z_λ of ż = f(t, z) + λ exists on [t₀, t₁] (the existence hypothesis hz_exists, kept for generality; it is always discharged by exists_isIntegralSolution_Icc_of_lipschitz).

The proof uses comparison_claim_1 to get v ≤ z_λ, then continuous_dependence_parameters (Khalil, Theorem 3.5) to bound ‖u - z_λ‖ ≤ ε/2, and concludes v(t) < u(t) + ε for all ε > 0.

Reference: Khalil, Nonlinear Systems (3rd ed.), Lemma 3.4. Note this is Khalil's Lemma 3.4; his Theorem 3.4 is the continuous-dependence result continuous_dependence_ODE.