dirichlet_eigenvalues_eq_nat_sq.toml

id = "dirichlet_eigenvalues_eq_nat_sq"
title = "Dirichlet eigenvalues of -y'' = lambda y on [0,pi] are n^2"
test = false
module = "LeanEval.Analysis.ODE.DirichletEigenvalues"
holes = ["dirichlet_eigenvalues_eq_nat_sq"]
submitter = "Kim Morrison"
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."