Ordinary differential equations

Existence and uniqueness (Cauchy–Peano, Picard, maximal solutions), linear systems and fundamental matrices, stability and Lyapunov's indirect method, Sturm–Liouville and boundary value problems with their Green's operators and eigenfunctions, oscillation and comparison theorems.

TheoremCauchy–Peano existence theorem#✓fully proved

Let \(E\) be a finite-dimensional real normed space and let \(f : \mathbb{R} \times E \to E\) be continuous. Then for every \(t_0 \in \mathbb{R}\) and \(x_0 \in E\) there are \(\varepsilon > 0\) and a function \(x : \mathbb{R} \to E\) with \(x(t_0) = x_0\) such that, for every \(t \in (t_0 - \varepsilon, t_0 + \varepsilon)\), \(x\) is differentiable at \(t\) with \(x'(t) = f(t, x(t))\).

theorem cauchy_peano_exists
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    (f : ℝ × E → E) (hf : Continuous f) (t₀ : ℝ) (x₀ : E) :
    ∃ ε > 0, ∃ x : ℝ → E, x t₀ = x₀ ∧
      ∀ t ∈ Set.Ioo (t₀ - ε) (t₀ + ε), HasDerivAt x (f (t, x t)) t
Sources
  • G. Peano, Math. Ann. 37 (1890), 182-228, DOI 10.1007/BF01200235.

TheoremComparison principle for the Dirichlet problem on \((0, 1)\)#●ready to prove

Let \(J \subseteq \mathbb{R}\) be an open set containing \([0, 1]\), and let \(u, v : \mathbb{R} \to \mathbb{R}\) be functions that are differentiable at every point of \(J\) and whose derivatives \(u'\) and \(v'\) are differentiable at every point of \(J\). If \(-u''(x) \le -v''(x)\) for every \(x \in (0, 1)\), \(u(0) \le v(0)\) and \(u(1) \le v(1)\), then \(u(x) \le v(x)\) for every \(x \in [0, 1]\).

public theorem_wanted bvp_comparison
    (J : Set ℝ) (hJ_open : IsOpen J) (hJ_sub : Set.Icc (0 : ℝ) 1 ⊆ J)
    (u v : ℝ → ℝ)
    (hu : ∀ x ∈ J, HasDerivAt u (deriv u x) x)
    (hu' : ∀ x ∈ J, HasDerivAt (deriv u) (deriv (deriv u) x) x)
    (hv : ∀ x ∈ J, HasDerivAt v (deriv v x) x)
    (hv' : ∀ x ∈ J, HasDerivAt (deriv v) (deriv (deriv v) x) x)
    (hineq : ∀ x ∈ Set.Ioo (0 : ℝ) 1, -deriv (deriv u) x ≤ -deriv (deriv v) x)
    (hu0 : u 0 ≤ v 0) (hu1 : u 1 ≤ v 1) :
    ∀ x ∈ Set.Icc (0 : ℝ) 1, u x ≤ v x
Sources
  • Standard maximum-principle argument; Protter-Weinberger. Problem bvp_comparison of the lean-eval benchmark.

TheoremDecay rate of solutions of \(y' = -y^3\)#●ready to prove

Let \(y : \mathbb{R} \to \mathbb{R}\) be differentiable at every \(t > 0\) with \(y'(t) = -y(t)^3\), continuous at \(0\) within \([0, \infty)\), and such that \(y(0) = 1\). Then \(y(t) \sqrt{t} \to 1/\sqrt{2}\) as \(t \to \infty\).

public theorem_wanted cubic_decay_asymptotic
    (y : ℝ → ℝ) (hy_diff : ∀ t : ℝ, 0 < t → HasDerivAt y (-(y t) ^ 3) t)
    (hy_cont : ContinuousWithinAt y (Set.Ici 0) 0)
    (hy0 : y 0 = 1) :
    Tendsto (fun t : ℝ => y t * Real.sqrt t) atTop (𝓝 (1 / Real.sqrt 2))
Sources
  • Standard ODE textbook exercise. Problem cubic_decay_asymptotic of the lean-eval benchmark.

TheoremDirichlet eigenvalues of \(-y'' = \lambda y\) on \((0, \pi)\)#●ready to prove

For every real number \(\lambda\), the following are equivalent: (i) there are a function \(y : \mathbb{R} \to \mathbb{R}\) and an open set \(J \subseteq \mathbb{R}\) containing \([0, \pi]\) such that \(y\) is differentiable at every point of \(J\), its derivative \(y'\) is differentiable at every \(x \in J\) with \(y''(x) = -\lambda y(x)\), \(y(0) = y(\pi) = 0\), and \(y(x) \ne 0\) for some \(x \in (0, \pi)\); (ii) \(\lambda = n^2\) for some positive integer \(n\).

public theorem_wanted dirichlet_eigenvalues_eq_nat_sq (lam : ℝ) :
    (∃ (y : ℝ → ℝ) (J : Set ℝ),
        IsOpen J ∧ Set.Icc (0 : ℝ) Real.pi ⊆ J ∧
        (∀ x ∈ J, HasDerivAt y (deriv y x) x) ∧
        (∀ x ∈ J, HasDerivAt (deriv y) (-(lam * y x)) x) ∧
        y 0 = 0 ∧ y Real.pi = 0 ∧
        ∃ x ∈ Set.Ioo (0 : ℝ) Real.pi, y x ≠ 0) ↔
      ∃ n : ℕ, 0 < n ∧ lam = (n : ℝ) ^ 2
Sources
  • Classical Sturm-Liouville theory. Problem dirichlet_eigenvalues_eq_nat_sq of the lean-eval benchmark.

TheoremDuhamel's formula (variation of constants)#✓fully proved

Let \(E\) be a real Banach space, let \(A : E \to E\) be a bounded linear operator, let \(b : \mathbb{R} \to E\) be continuous, and let \(t_0 \in \mathbb{R}\) and \(x_0 \in E\). Write \(e^{sA}\) for the operator exponential and define \(x : \mathbb{R} \to E\) by \(x(t) = e^{(t - t_0)A} x_0 + \int_{t_0}^{t} e^{(t - s)A} b(s)\, ds\). Then \(x(t_0) = x_0\) and \(x\) is differentiable with \(x'(t) = A x(t) + b(t)\) for every \(t \in \mathbb{R}\). Moreover \(x\) is the only such solution: every \(y : \mathbb{R} \to E\) with \(y(t_0) = x_0\) and \(y'(t) = A y(t) + b(t)\) for every \(t \in \mathbb{R}\) equals \(x\).

Proof: Factor the propagator by the commuting exponential group law, differentiate the integrating-factor primitive, and apply global Lipschitz uniqueness. This follows Teschl, Sections 3.2 and 3.4, formula (3.48) and Theorem 3.12 / (3.97).

theorem duhamel_variation_of_constants
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
    (A : E →L[ℝ] E) (b : ℝ → E) (t₀ : ℝ) (x₀ : E)
    (hb : Continuous b) :
    ∃ x : ℝ → E, x t₀ = x₀ ∧
      (∀ t, x t = (NormedSpace.exp ((t - t₀) • A)) x₀ +
        ∫ s in t₀..t, (NormedSpace.exp ((t - s) • A)) (b s)) ∧
      (∀ t, HasDerivAt x (A (x t) + b t) t) ∧
      ∀ y : ℝ → E, y t₀ = x₀ → (∀ t, HasDerivAt y (A (y t) + b t) t) → y = x
Sources
  • G. Teschl, Ordinary Differential Equations and Dynamical Systems, Section 3.2; stable ref https://en.wikipedia.org/wiki/Duhamel%27s_principle.

TheoremNonresonant forced oscillator#●ready to prove

Let \(\omega > 0\) be a real number that is not an integer, and let \(g : \mathbb{R} \to \mathbb{R}\) be continuous and \(2\pi\)-periodic. Then the equation \(u'' + \omega^2 u = g\) has exactly one twice continuously differentiable solution \(u : \mathbb{R} \to \mathbb{R}\) that is \(2\pi\)-periodic, and every twice continuously differentiable solution \(u : \mathbb{R} \to \mathbb{R}\) of this equation is bounded.

public theorem_wanted existsUnique_periodic_solution_and_isBounded_of_ne_natCast
  (ω : ℝ) (hωpos : 0 < ω) (hω_nonint : ∀ n : ℕ, ω ≠ n)
  (g : ℝ → ℝ) (hg_cont : Continuous g)
  (hper : Function.Periodic g (2 * Real.pi)) :
  (∃! u : ℝ → ℝ, ContDiff ℝ 2 u ∧
  (∀ x : ℝ, deriv (deriv u) x + ω ^ 2 * u x = g x) ∧
  Function.Periodic u (2 * Real.pi)) ∧
  (∀ u : ℝ → ℝ, ContDiff ℝ 2 u →
  (∀ x : ℝ, deriv (deriv u) x + ω ^ 2 * u x = g x) →
  Bornology.IsBounded (Set.range u))
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Operator theory; Ordinary differential operators), problem ma_proofbench_l2_39.

TheoremSolutions of \(xu''+2u'+u=0\) have infinitely many zeros#●ready to prove

Let \(u : \mathbb{R} \to \mathbb{R}\) be twice continuously differentiable on \((0,\infty)\) and satisfy

\[ x\,u''(x)+2u'(x)+u(x)=0 \quad \text{for all } x>0. \]

If \(u(x) \ne 0\) for some \(x>0\), then \(u\) has infinitely many zeros in \((1,\infty)\).

public theorem_wanted setInfinite_zero_of_mul_iteratedDeriv_two_add_two_deriv_add_eq_zero
  (u : ℝ → ℝ)
  (hu_diff : ContDiffOn ℝ 2 u (Set.Ioi 0))
  (hu : ∀ x > 0, x * iteratedDeriv 2 u x + 2 * deriv u x + u x = 0)
  (hnontrivial : ∃ x > 0, u x ≠ 0) :
  Set.Infinite {x : ℝ | x > 1 ∧ u x = 0}
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Operator theory; Ordinary differential operators), problem ma_proofbench_l2_83.

TheoremSturm separation theorem#●ready to prove

Let \(p, q, y_1, y_2 : \mathbb{R} \to \mathbb{R}\) and \(a < b\), and let \(J \subseteq \mathbb{R}\) be an open connected set (an open interval, possibly unbounded) containing \([a, b]\). Suppose that \(p\) and \(q\) are continuous on \(J\), and that \(y_1\) and \(y_2\) are twice differentiable at every point of \(J\) and solve \(y'' + p(x)\, y' + q(x)\, y = 0\) at every \(x \in J\). Suppose further that the Wronskian \(y_1 y_2' - y_2 y_1'\) is nonzero at some point of \(J\). If \(y_1(a) = y_1(b) = 0\) and \(y_1(x) \ne 0\) for every \(x \in (a, b)\), then \(y_2\) has exactly one zero in the open interval \((a, b)\).

public theorem_wanted sturm_separation
    (p q y₁ y₂ : ℝ → ℝ) (a b : ℝ) (hab : a < b)
    (J : Set ℝ) (hJ_open : IsOpen J) (hJ_conn : IsPreconnected J)
    (hJ_sub : Set.Icc a b ⊆ J)
    (hp : ContinuousOn p J) (hq : ContinuousOn q J)
    (hy₁ : ∀ x ∈ J, HasDerivAt y₁ (deriv y₁ x) x)
    (hy₁' : ∀ x ∈ J, HasDerivAt (deriv y₁) (-(p x * deriv y₁ x + q x * y₁ x)) x)
    (hy₂ : ∀ x ∈ J, HasDerivAt y₂ (deriv y₂ x) x)
    (hy₂' : ∀ x ∈ J, HasDerivAt (deriv y₂) (-(p x * deriv y₂ x + q x * y₂ x)) x)
    (hW : ∃ x₀ ∈ J, y₁ x₀ * deriv y₂ x₀ - y₂ x₀ * deriv y₁ x₀ ≠ 0)
    (hza : y₁ a = 0) (hzb : y₁ b = 0)
    (hne : ∀ x ∈ Set.Ioo a b, y₁ x ≠ 0) :
    ∃! c, c ∈ Set.Ioo a b ∧ y₂ c = 0
Sources
  • C. Sturm, Mémoire sur les équations différentielles linéaires du second ordre, 1836. Problem sturm_separation of the lean-eval benchmark.
2 fully proved6 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.