Dirichlet eigenvalues of -y'' = lambda y on [0,pi] are n^2

Problem statement

Notes: Characterises the spectrum of the Dirichlet Laplacian on [0,pi]: lambda is an eigenvalue iff lambda = n^2 for some positive natural n.

Source: Classical Sturm-Liouville theory.

Informal solution: Case-split on the sign of lambda. For lambda <= 0 only the zero solution satisfies both boundary conditions. For lambda > 0 the general solution is A sin(sqrt lambda x) + B cos(sqrt lambda x); the boundary conditions force B = 0 and sqrt lambda in N_{>0}. Conversely, for lambda = n^2 with n in N_{>0}, the function sin(n x) is a nontrivial Dirichlet eigenfunction.

theorem declaration uses `sorry`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 := bylam:ℝ⊢ (∃ y J,
    IsOpen J ∧
      Set.Icc 0 π ⊆ J ∧
        (∀ x ∈ J, HasDerivAt y (deriv y x) x) ∧
          (∀ x ∈ J, HasDerivAt (deriv y) (-(lam * y x)) x) ∧ y 0 = 0 ∧ y π = 0 ∧ ∃ x ∈ Set.Ioo 0 π, y x ≠ 0) ↔
  ∃ n, 0 < n ∧ lam = ↑n ^ 2
  sorryAll goals completed! 🐙