Sturm–Liouville Dirichlet problem

TheoremExistence for the Sturm–Liouville Dirichlet problem on the closed unit interval#✓fully proved

Let \(V\) and \(f\) be continuous real functions on \([0, 1]\) with \(V \ge 0\). Then there is a function \(u \colon \mathbb{R} \to \mathbb{R}\) that is \(C^2\) on \([0, 1]\), satisfies \(-u''(x) + V(x)\,u(x) = f(x)\) for every \(x \in [0, 1]\), with the second derivative taken within \([0, 1]\), and has \(u(0) = u(1) = 0\).

The proof is by the shooting method: let \(u_0\) solve the equation with \(u_0(0) = u_0'(0) = 0\), and let \(w\) solve the homogeneous equation \(-w'' + V w = 0\) with \(w(0) = 0\) and \(w'(0) = 1\). An energy argument using \(V \ge 0\) shows \(w(1) \ne 0\), and \(u = u_0 + a w\) with \(a = -u_0(1)/w(1)\) is the required solution.

theorem sturm_liouville_existence
    (V : C(Set.Icc (0 : ℝ) 1, ℝ)) (hV : ∀ x : Set.Icc (0 : ℝ) 1, 0 ≤ V x)
    (f : C(Set.Icc (0 : ℝ) 1, ℝ)) :
    ∃ u : ℝ → ℝ,
      ContDiffOn ℝ 2 u (Set.Icc 0 1) ∧
      (∀ x : ℝ, ∀ hx : x ∈ Set.Icc (0 : ℝ) 1, -(iteratedDerivWithin 2 u (Set.Icc 0 1) x) +
        V ⟨x, hx⟩ * u x = f ⟨x, hx⟩) ∧
      u 0 = 0 ∧ u 1 = 0

Sources

• SpectralTheory.sturm_liouville_existence in the v1 formalization, whose formalization is left unproved there; the proof here is original.

Uses 1

Proof usesGlobal existence and uniqueness for globally Lipschitz ODEs

TheoremUniqueness for the Sturm–Liouville Dirichlet problem on the closed unit interval#✓fully proved

Let \(V\) and \(f\) be continuous real functions on \([0, 1]\) with \(V \ge 0\), and let \(u_1, u_2 \colon \mathbb{R} \to \mathbb{R}\) be \(C^2\) on \([0, 1]\). Suppose that for \(i = 1, 2\), \(-u_i''(x) + V(x)\,u_i(x) = f(x)\) for every \(x \in [0, 1]\), with the second derivative taken within \([0, 1]\), and \(u_i(0) = u_i(1) = 0\). Then \(u_1\) and \(u_2\) agree on \([0, 1]\).

theorem sturm_liouville_uniqueness
    (V : C(Set.Icc (0 : ℝ) 1, ℝ)) (hV : ∀ x : Set.Icc (0 : ℝ) 1, 0 ≤ V x)
    (f : C(Set.Icc (0 : ℝ) 1, ℝ))
    (u₁ u₂ : ℝ → ℝ)
    (h₁ : ContDiffOn ℝ 2 u₁ (Set.Icc 0 1) ∧
      (∀ x : ℝ, ∀ hx : x ∈ Set.Icc (0 : ℝ) 1, -(iteratedDerivWithin 2 u₁ (Set.Icc 0 1) x) +
        V ⟨x, hx⟩ * u₁ x = f ⟨x, hx⟩) ∧
      u₁ 0 = 0 ∧ u₁ 1 = 0)
    (h₂ : ContDiffOn ℝ 2 u₂ (Set.Icc 0 1) ∧
      (∀ x : ℝ, ∀ hx : x ∈ Set.Icc (0 : ℝ) 1, -(iteratedDerivWithin 2 u₂ (Set.Icc 0 1) x) +
        V ⟨x, hx⟩ * u₂ x = f ⟨x, hx⟩) ∧
      u₂ 0 = 0 ∧ u₂ 1 = 0) :
    Set.EqOn u₁ u₂ (Set.Icc 0 1)

TheoremExistence for the one-dimensional Dirichlet problem#●ready to prove

Let \(f : \mathbb{R} \to \mathbb{R}\) be continuous on \([0, 1]\). Then there is a twice continuously differentiable function \(u : \mathbb{R} \to \mathbb{R}\) with \(u(0) = u(1) = 0\) and \(u''(x) = f(x)\) for every \(x \in (0, 1)\).

public theorem_wanted dirichlet_1d_exists {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc 0 1)) :
    ∃ u : ℝ → ℝ, ContDiff ℝ 2 u ∧ u 0 = 0 ∧ u 1 = 0 ∧
      ∀ x ∈ Set.Ioo 0 1, deriv (deriv u) x = f x

Sources

• L. Evans, Partial Differential Equations, Ch. 6.

TheoremUniqueness for the one-dimensional Dirichlet problem#●ready to prove

Let \(f : \mathbb{R} \to \mathbb{R}\) be any function, and let \(u_1, u_2 : \mathbb{R} \to \mathbb{R}\) be twice continuously differentiable functions such that, for \(i = 1, 2\), \(u_i(0) = u_i(1) = 0\) and \(u_i''(x) = f(x)\) for every \(x \in (0, 1)\). Then \(u_1(x) = u_2(x)\) for every \(x \in [0, 1]\).

public theorem_wanted dirichlet_1d_unique {f : ℝ → ℝ} {u₁ u₂ : ℝ → ℝ}
    (h₁ : ContDiff ℝ 2 u₁ ∧ u₁ 0 = 0 ∧ u₁ 1 = 0 ∧
      ∀ x ∈ Set.Ioo 0 1, deriv (deriv u₁) x = f x)
    (h₂ : ContDiff ℝ 2 u₂ ∧ u₂ 0 = 0 ∧ u₂ 1 = 0 ∧
      ∀ x ∈ Set.Ioo 0 1, deriv (deriv u₂) x = f x) :
    ∀ x ∈ Set.Icc 0 1, u₁ x = u₂ x

Sources

• L. Evans, Partial Differential Equations, Ch. 6.

2 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.