Sturm separation theorem

sturm_separation — a formalization challenge from the lean-eval benchmark.

Notes

Between consecutive zeros of one solution of a second-order linear homogeneous ODE, any linearly independent solution has exactly one zero.

Formal statement

/-- **Sturm separation theorem.** Suppose `y₁, y₂ : ℝ → ℝ` are `C²` solutions on an open
interval `J` containing `[a, b]` of the linear homogeneous ODE `y'' + p y' + q y = 0`
with `p, q` continuous on `J`, and their Wronskian is nonzero at some point of `J`. If
`a < b ∈ J` are consecutive zeros of `y₁` (i.e. `y₁ a = y₁ b = 0` and `y₁ x ≠ 0` on
`(a, b)`), then `y₂` has exactly one zero in `(a, b)`. -/
theorem 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 := by
  sorry

Informal solution sketch

On (a, b), y_1 has constant sign and never vanishes. The Wronskian W = y_1 y_2' - y_2 y_1' satisfies W' = -p W (Liouville), so W has constant sign on J. Hence (y_2 / y_1)' = -W / y_1^2 has constant sign and y_2 / y_1 is strictly monotone on (a, b). The Wronskian also forces y_2(a), y_2(b) ≠ 0 (else W(a) or W(b) would vanish, contradicting nonvanishing of W). If y_2 had no zero in (a, b), continuity gives sign(y_2(a)) = sign(y_2(b)); then y_2 / y_1 tends to the same infinite sign at both endpoints, contradicting strict monotonicity. Thus y_2 has a zero in (a, b). Uniqueness follows because a strictly monotone function can cross 0 at most once.

Source

C. Sturm, Mémoire sur les équations différentielles linéaires du second ordre, 1836.

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: sturm_separation
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.