Sturm separation theorem | Lean AI formalization leaderboard

Problem statement

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

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

Informal solution: 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.

theorem declaration uses `sorry`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 := byp:ℝ → ℝq:ℝ → ℝy₁:ℝ → ℝy₂:ℝ → ℝa:ℝb:ℝhab:a < bJ:Set ℝhJ_open:IsOpen JhJ_conn:IsPreconnected JhJ_sub:Set.Icc a b ⊆ Jhp:ContinuousOn p Jhq:ContinuousOn q Jhy₁:∀ x ∈ J, HasDerivAt y₁ (deriv y₁ x) xhy₁':∀ x ∈ J, HasDerivAt (deriv y₁) (-(p x * deriv y₁ x + q x * y₁ x)) xhy₂:∀ x ∈ J, HasDerivAt y₂ (deriv y₂ x) xhy₂':∀ x ∈ J, HasDerivAt (deriv y₂) (-(p x * deriv y₂ x + q x * y₂ x)) xhW:∃ x₀ ∈ J, y₁ x₀ * deriv y₂ x₀ - y₂ x₀ * deriv y₁ x₀ ≠ 0hza:y₁ a = 0hzb:y₁ b = 0hne:∀ x ∈ Set.Ioo a b, y₁ x ≠ 0⊢ ∃! c, c ∈ Set.Ioo a b ∧ y₂ c = 0
  sorryAll goals completed! 🐙